AbsolutelyContinuous

📁 Source: Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean

Statistics

Metric	Count
Definitions `AbsolutelyContinuousOnInterval`, `disjWithin`, `totalLengthFilter`	3
Theorems `add`, `ae_differentiableAt`, `biUnion_uIoc_subset_of_mem_disjWithin`, `boundedVariationOn`, `const_mul`, `const_smul`, `continuousOn`, `disjWithin_comm`, `disjWithin_mono`, `exists_bound`, `fun_add`, `fun_mul`, `fun_neg`, `fun_smul`, `fun_sub`, `hasBasis_totalLengthFilter`, `mono`, `mul`, `neg`, `smul`, `sub`, `tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero`, `tendsto_volume_totalLengthFilter_nhds_zero`, `uIoc_subset_of_mem_disjWithin`, `uniformContinuousOn`, `uniformity_eq_comap_totalLengthFilter`, `uniformlyContinuousOn`, `absolutelyContinuousOnInterval_intervalIntegral`, `absolutelyContinuousOnInterval`, `absolutelyContinuousOnInterval_iff`	30
Total	33

AbsolutelyContinuousOnInterval

Definitions

Name	Category	Theorems
`disjWithin` 📖	CompOp	3 math math: `disjWithin_comm`, `disjWithin_mono`, `tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero`
`totalLengthFilter` 📖	CompOp	4 math math: `tendsto_volume_totalLengthFilter_nhds_zero`, `tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero`, `uniformity_eq_comap_totalLengthFilter`, `hasBasis_totalLengthFilter`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.instAdd` `Real` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`squeeze_zero` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `Finset.sum_add_distrib` `Finset.sum_le_sum` `dist_add_add_le` `add_zero` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`ae_differentiableAt` 📖	mathematical	`AbsolutelyContinuousOnInterval` `Real` `Real.pseudoMetricSpace`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume`	—	`BoundedVariationOn.ae_differentiableAt_of_mem_uIcc` `FiniteDimensional.rclike_to_real` `boundedVariationOn`
`biUnion_uIoc_subset_of_mem_disjWithin` 📖	mathematical	`Set` `Set.instMembership` `disjWithin`	`Real` `Set.instHasSubset` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.range` `Set.uIoc` `Real.linearOrder`	—	`Set.iUnion_congr_Prop` `uIoc_subset_of_mem_disjWithin`
`boundedVariationOn` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`BoundedVariationOn` `Real` `Real.linearOrder` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.uIcc` `Real.lattice`	—	`Set.uIcc_of_le` `LE.le.eq_or_lt` `Set.Icc_self` `eVariationOn.subsingleton` `absolutelyContinuousOnInterval_iff` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `exists_nat_one_div_lt` `Real.instArchimedean` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Monotone.const_add` `Monotone.mul_const` `IsOrderedRing.toMulPosMono` `Nat.mono_cast` `div_nonneg` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.natCast_nonneg` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.zero_mul` `add_zero` `Nat.cast_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Finset.sum_congr` `eVariationOn.sum'` `Set.Icc_subset_Icc` `Set.PairwiseDisjoint.eq_1` `Set.uIoc_of_le` `Nat.succ_eq_succ` `Pairwise.set_pairwise` `Monotone.pairwise_disjoint_on_Ioc_succ` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Set.mem_Icc` `Finset.sum_range_sub` `dist_comm` `Real.dist_eq` `abs_eq_self` `ENNReal.toReal_sum` `ENNReal.ofReal_toReal` `ENNReal.ofReal_one` `ENNReal.ofReal_le_ofReal` `LT.lt.le` `add_mul` `Distrib.rightDistribClass` `add_assoc` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Set.uIcc_comm` `symm`
`const_mul` 📖	mathematical	`AbsolutelyContinuousOnInterval` `Real` `Real.pseudoMetricSpace`	`Real.instMul`	—	`const_smul` `NormedSpace.toNormSMulClass`
`const_smul` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`squeeze_zero` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `Finset.sum_congr` `dist_smul₀` `Finset.mul_sum` `MulZeroClass.mul_zero` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`continuousOn` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.uIcc` `Real.lattice`	—	`UniformContinuousOn.continuousOn` `uniformContinuousOn`
`disjWithin_comm` 📖	mathematical	—	`disjWithin`	—	`disjWithin.eq_1` `Set.uIcc_comm`
`disjWithin_mono` 📖	mathematical	`Set` `Real` `Set.instHasSubset` `Set.uIcc` `Real.lattice`	`disjWithin`	—	—
`exists_bound` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`IsCompact.exists_bound_of_continuousOn` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `continuousOn`
`fun_add` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`add`
`fun_mul` 📖	mathematical	`AbsolutelyContinuousOnInterval` `Real` `Real.pseudoMetricSpace`	`Real.instMul`	—	`mul`
`fun_neg` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`neg`
`fun_smul` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedRing.toPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`smul`
`fun_sub` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`sub`
`hasBasis_totalLengthFilter` 📖	mathematical	—	`Filter.HasBasis` `Real` `totalLengthFilter` `Real.instLT` `Real.instZero` `setOf` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Set.ext` `zero_sub` `zero_add` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `Filter.HasBasis.comap` `nhds_basis_Ioo_pos` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`mono` 📖	—	`AbsolutelyContinuousOnInterval` `Set` `Real` `Set.instHasSubset` `Set.uIcc` `Real.lattice`	—	—	`le_trans` `Filter.map_mono` `inf_le_inf` `le_refl` `disjWithin_mono`
`mul` 📖	mathematical	`AbsolutelyContinuousOnInterval` `Real` `Real.pseudoMetricSpace`	`Pi.instMul` `Real.instMul`	—	`smul` `NormedSpace.toNormSMulClass`
`neg` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.instNeg` `Real` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`squeeze_zero` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `Finset.sum_congr` `dist_neg_neg` `NormedAddGroup.to_isIsometricVAdd_left` `NormedAddGroup.to_isIsometricVAdd_right`
`smul` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedRing.toPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.smul'` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`exists_bound` `squeeze_zero'` `Filter.Eventually.of_forall` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `Filter.eventually_inf_principal` `Filter.univ_mem'` `Finset.sum_congr` `Finset.mul_sum` `Finset.sum_le_sum` `dist_triangle` `add_le_add` `covariant_swap_add_of_covariant_add` `dist_smul₀` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_comm` `le_imp_le_of_le_of_le` `dist_pair_smul` `NormSMulClass.toIsBoundedSMul` `le_refl` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `dist_zero_right` `MulZeroClass.mul_zero` `add_zero` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul`
`sub` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.instSub` `Real` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.uIoc` `Real.linearOrder` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.range` `Filter` `Filter.instInf` `totalLengthFilter` `Real.pseudoMetricSpace` `Filter.principal` `disjWithin` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `Filter.Tendsto.mono_left` `tendsto_volume_totalLengthFilter_nhds_zero` `Set.iUnion_congr_Prop` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.Measure.restrict_le_self`
`tendsto_volume_totalLengthFilter_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.range` `Set.uIoc` `Real.linearOrder` `totalLengthFilter` `Real.pseudoMetricSpace` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `ENNReal.ofReal_zero` `ENNReal.tendsto_ofReal` `Filter.tendsto_comap` `Set.iUnion_congr_Prop` `ENNReal.instCanonicallyOrderedAdd` `le_imp_le_of_le_of_le` `MeasureTheory.measure_biUnion_finset_le` `MeasureTheory.Measure.instOuterMeasureClass` `le_refl` `ENNReal.ofReal_sum_of_nonneg` `dist_nonneg` `Eq.le` `Finset.sum_congr` `Real.volume_Ioc` `max_sub_min_eq_abs'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`uIoc_subset_of_mem_disjWithin` 📖	mathematical	`Set` `Set.instMembership` `disjWithin`	`Real` `Set.instHasSubset` `Set.uIoc` `Real.linearOrder`	—	`Set.Ioc_subset_Ioc`
`uniformContinuousOn` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`UniformContinuousOn` `Real` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.uIcc` `Real.lattice`	—	`uniformity_eq_comap_totalLengthFilter` `Filter.comap_inf` `Filter.comap_principal` `Set.ext` `Finset.coe_singleton` `Filter.comap_comap` `Finset.sum_congr` `Finset.sum_const` `Finset.card_singleton` `one_smul` `Filter.comap_mono`
`uniformity_eq_comap_totalLengthFilter` 📖	mathematical	—	`uniformity` `PseudoMetricSpace.toUniformSpace` `Filter.comap` `totalLengthFilter`	—	`Filter.HasBasis.eq_of_same_basis` `Metric.uniformity_basis_dist` `Finset.sum_congr` `Finset.sum_const` `Finset.card_singleton` `one_smul` `Filter.HasBasis.comap` `hasBasis_totalLengthFilter`
`uniformlyContinuousOn` 📖	mathematical	`AbsolutelyContinuousOnInterval` `SeminormedAddCommGroup.toPseudoMetricSpace`	`UniformContinuousOn` `Real` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.uIcc` `Real.lattice`	—	`uniformContinuousOn`

IntervalIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuousOnInterval_intervalIntegral` 📖	mathematical	`IntervalIntegrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Set` `Set.instMembership` `Set.uIcc` `Real.lattice`	`AbsolutelyContinuousOnInterval` `intervalIntegral` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.tendsto_setLIntegral_zero` `ne_of_lt` `MeasureTheory.Integrable.hasFiniteIntegral` `intervalIntegrable_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero` `Filter.Tendsto.comp` `ContinuousAt.tendsto` `ENNReal.continuousAt_toReal` `ENNReal.toReal_zero` `squeeze_zero'` `Filter.univ_mem'` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `Finset.sum_congr` `Filter.eventually_inf_principal` `Filter.mp_mem` `Set.mem_setOf_eq` `Set.iUnion_congr_Prop` `MeasureTheory.integral_norm_eq_lintegral_enorm` `MeasureTheory.AEStronglyMeasurable.restrict` `aestronglyMeasurable_restrict_uIoc` `MeasureTheory.integral_biUnion_finset` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin` `Finset.mem_range` `MeasureTheory.Measure.restrict_restrict_of_subset` `MeasureTheory.IntegrableOn.integrable` `MeasureTheory.IntegrableOn.mono_set` `MeasureTheory.Integrable.norm` `def'` `Finset.sum_le_sum` `Real.dist_eq` `intervalIntegral.integral_interval_sub_left` `mono_set'` `intervalIntegral.integral_symm` `abs_neg` `intervalIntegral.abs_intervalIntegral_eq` `MeasureTheory.abs_integral_le_integral_abs`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuousOnInterval` 📖	mathematical	`LipschitzOnWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.uIcc` `Real.lattice`	`AbsolutelyContinuousOnInterval`	—	`absolutelyContinuousOnInterval_iff` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NNReal.coe_nonneg` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Finset.sum_le_sum` `dist_edist` `ENNReal.toReal_mul` `ENNReal.toReal_mono` `instLawfulBCmpCompare_mathlib` `Finset.mul_sum` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_lt` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.neg_add` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `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.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`

(root)

Definitions

Name	Category	Theorems
`AbsolutelyContinuousOnInterval` 📖	MathDef	3 math math: `IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral`, `LipschitzOnWith.absolutelyContinuousOnInterval`, `absolutelyContinuousOnInterval_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuousOnInterval_iff` 📖	mathematical	—	`AbsolutelyContinuousOnInterval` `Real` `Real.instLT` `Real.instZero` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_zero_right` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.sum_nonneg` `dist_nonneg` `Filter.HasBasis.eventually_iff` `Filter.HasBasis.inf_principal` `AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter` `Finset.sum_congr`

---

← Back to Index