Documentation Verification Report

DerivIntegrable

📁 Source: Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean

Statistics

Metric	Count
Definitions	0
Theorems `intervalIntegrable_deriv`, `intervalIntegrable_deriv`, `exists_tendsto_deriv_liminf_lintegral_enorm_le`, `intervalIntegrable_deriv`, `intervalIntegral_deriv_mem_uIcc`	5
Total	5

AbsolutelyContinuousOnInterval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intervalIntegrable_deriv` 📖	mathematical	`AbsolutelyContinuousOnInterval` `Real` `Real.pseudoMetricSpace`	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`BoundedVariationOn.intervalIntegrable_deriv` `boundedVariationOn`

BoundedVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intervalIntegrable_deriv` 📖	mathematical	`BoundedVariationOn` `Real` `Real.linearOrder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set.uIcc` `Real.lattice`	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn` `locallyBoundedVariationOn` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.NoAtoms.measure_singleton` `Real.noAtoms_volume` `IntervalIntegrable.congr_ae` `PseudoEMetricSpace.pseudoMetrizableSpace` `IntervalIntegrable.sub` `MonotoneOn.intervalIntegrable_deriv` `Filter.EventuallyEq.eq_1` `MeasureTheory.ae_restrict_iff'` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.mp_mem` `MonotoneOn.ae_differentiableWithinAt_of_mem` `Filter.univ_mem'` `Set.Ioc_subset_Icc_self` `Icc_mem_nhds` `Set.mem_Ioc` `Set.uIoc.eq_1` `lt_of_le_of_ne` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `DifferentiableAt.hasDerivAt` `DifferentiableWithinAt.differentiableAt` `HasDerivAt.deriv` `HasDerivAt.sub`

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_tendsto_deriv_liminf_lintegral_enorm_le` 📖	mathematical	`Real` `Real.instLE` `MonotoneOn` `Real.instPreorder` `Set.Icc`	`Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.AEStronglyMeasurable` `Real.measurableSpace` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `MeasureTheory.lintegral` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofReal` `Real.instSub`	—	`monotoneOn_univ` `comp` `Set.EqOn.deriv` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.NoAtoms.measure_singleton` `Real.noAtoms_volume` `intervalIntegrable_slope` `Monotone.monotoneOn` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `intervalIntegrable_iff_integrableOn_Icc_of_le` `PseudoEMetricSpace.pseudoMetrizableSpace` `enorm_ne_top` `MeasureTheory.ae_restrict_iff'` `BorelSpace.opensMeasurable` `Real.borelSpace` `Filter.mp_mem` `Monotone.ae_differentiableAt` `Filter.univ_mem'` `Filter.Tendsto.comp` `HasDerivAt.tendsto_slope` `DifferentiableAt.hasDerivAt` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `add_zero` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_const_nhds` `tendsto_inv_atTop_nhds_zero_nat` `RCLike.charZero_rclike` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `MeasureTheory.Integrable.aestronglyMeasurable` `Filter.liminf_congr` `MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm` `abs_eq_self` `slope_nonneg` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Filter.liminf_le_of_frequently_le'` `Filter.Frequently.of_forall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ENNReal.ofReal_le_ofReal` `MeasureTheory.integral_Icc_eq_integral_Ioc` `intervalIntegral.integral_of_le` `min_self` `inf_of_le_right` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `intervalIntegral_slope_le`
`intervalIntegrable_deriv` 📖	mathematical	`MonotoneOn` `Real` `Real.instPreorder` `Set.uIcc` `Real.lattice`	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`MeasureTheory.Measure.instOuterMeasureClass` `exists_tendsto_deriv_liminf_lintegral_enorm_le` `Set.uIcc_of_le` `LT.lt.ne_top` `lt_of_le_of_lt` `ENNReal.ofReal_lt_top` `MeasureTheory.integrable_of_tendsto` `intervalIntegrable_iff_integrableOn_Icc_of_le` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.noAtoms_volume` `enorm_ne_top` `IntervalIntegrable.symm` `Set.uIcc_comm` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `lt_of_not_ge`
`intervalIntegral_deriv_mem_uIcc` 📖	mathematical	`MonotoneOn` `Real` `Real.instPreorder` `Set.uIcc` `Real.lattice`	`Set` `Set.instMembership` `Real.instZero` `Real.instSub` `intervalIntegral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`MeasureTheory.Measure.instOuterMeasureClass` `exists_tendsto_deriv_liminf_lintegral_enorm_le` `Set.uIcc_of_le` `MeasureTheory.NoAtoms.measure_singleton` `Real.noAtoms_volume` `LT.lt.ne_top` `lt_of_le_of_lt` `ENNReal.ofReal_lt_top` `MeasureTheory.integrable_of_tendsto` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Set.mem_Icc` `derivWithin_of_mem_nhds` `Icc_mem_nhds` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `derivWithin_nonneg` `instOrderTopologyReal` `intervalIntegral.integral_nonneg_of_ae_restrict` `Filter.EventuallyLE.eq_1` `MeasureTheory.ae_restrict_iff'` `BorelSpace.opensMeasurable` `Real.borelSpace` `Filter.mp_mem` `Filter.univ_mem'` `MeasureTheory.lintegral_enorm_le_liminf_of_tendsto` `AEMeasurable.enorm` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `intervalIntegral.integral_congr_ae` `Set.uIoc_of_le` `abs_eq_self` `intervalIntegral.integral_of_le` `MeasureTheory.integral_Icc_eq_integral_Ioc` `ENNReal.ofReal_le_ofReal_iff` `MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm` `le_imp_le_of_le_of_le` `le_refl` `Mathlib.Tactic.Linarith.add_neg` `lt_of_not_ge` `intervalIntegral.integral_symm` `Set.uIcc_of_ge` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Set.neg_mem_Icc_iff` `neg_zero` `neg_sub` `Set.uIcc_comm`

---

← Back to Index