Commit 2025-10-02 10:12 1f85fdff

View on Github →

feat(MeasureTheory): add absolutely continuous functions (#29504) Add absolutely continuous functions. Part of originally planned #29092.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean

added theorem AbsolutelyContinuousOnInterval.add

added theorem AbsolutelyContinuousOnInterval.boundedVariationOn

added theorem AbsolutelyContinuousOnInterval.const_mul

added theorem AbsolutelyContinuousOnInterval.const_smul

added theorem AbsolutelyContinuousOnInterval.continuousOn

added def AbsolutelyContinuousOnInterval.disjWithin

added theorem AbsolutelyContinuousOnInterval.disjWithin_comm

added theorem AbsolutelyContinuousOnInterval.disjWithin_mono

added theorem AbsolutelyContinuousOnInterval.exists_bound

added theorem AbsolutelyContinuousOnInterval.fun_add

added theorem AbsolutelyContinuousOnInterval.fun_mul

added theorem AbsolutelyContinuousOnInterval.fun_neg

added theorem AbsolutelyContinuousOnInterval.fun_smul

added theorem AbsolutelyContinuousOnInterval.fun_sub

added theorem AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter

added theorem AbsolutelyContinuousOnInterval.mono

added theorem AbsolutelyContinuousOnInterval.mul

added theorem AbsolutelyContinuousOnInterval.neg

added theorem AbsolutelyContinuousOnInterval.smul

added theorem AbsolutelyContinuousOnInterval.sub

added theorem AbsolutelyContinuousOnInterval.symm

added def AbsolutelyContinuousOnInterval.totalLengthFilter

added theorem AbsolutelyContinuousOnInterval.uniformity_eq_comap_totalLengthFilter

added theorem AbsolutelyContinuousOnInterval.uniformlyContinuousOn

added def AbsolutelyContinuousOnInterval

added theorem LipschitzOnWith.absolutelyContinuousOnInterval

added theorem absolutelyContinuousOnInterval_iff

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

added theorem eVariationOn.sum'

added theorem eVariationOn.sum