Absolutely continuous functions

TheoremAbsolutely continuous functions have the Lusin N property#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be absolutely continuous on every closed bounded interval \([a, b]\). Then \(f\) maps Lebesgue null sets to null sets: for every set \(s \subseteq \mathbb{R}\) of Lebesgue outer measure zero, the image \(f(s)\) has Lebesgue outer measure zero.

public theorem_wanted volume_image_eq_zero_of_absolutelyContinuous
    (f : ℝ → ℝ) (hf : ∀ a b : ℝ, AbsolutelyContinuousOnInterval f a b) :
    ∀ s : Set ℝ, MeasureTheory.volume s = 0 → MeasureTheory.volume (f '' s) = 0

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_75.

TheoremLipschitz functions are the absolutely continuous functions with bounded derivative#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) and let \(M \ge 0\) be a real number. Then \(|f(x) - f(y)| \le M|x - y|\) for all \(x, y \in \mathbb{R}\) if and only if \(f\) is absolutely continuous on every closed bounded interval and \(|f'(x)| \le M\) for almost every \(x \in \mathbb{R}\) (with respect to Lebesgue measure), where \(f'(x)\) is taken to be \(0\) at points where \(f\) is not differentiable.

public theorem_wanted lipschitzWith_iff_absolutelyContinuous_and_ae_norm_deriv_le
    (f : ℝ → ℝ) (M : NNReal) : (LipschitzWith M f) ↔
  ((∀ a b : ℝ, AbsolutelyContinuousOnInterval f a b) ∧ (∀ᵐ x, ‖deriv f x‖ ≤ (M : ℝ)))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_62.

TheoremA \(1\)-Lipschitz function on \((a,b)\) is absolutely continuous with essentially bounded derivative#●ready to prove

A \(1\)-Lipschitz function on \([a,b]\) is absolutely continuous with essentially bounded derivative. Let \(a \le b\) be real numbers and let \(f : \mathbb{R} \to \mathbb{R}\) satisfy \(|f(x) - f(y)| \le |x - y|\) for all \(x, y \in [a, b]\). Then \(f\) is absolutely continuous on \([a, b]\), and its derivative \(f'\), taken to be \(0\) at points where \(f\) is not differentiable, has finite norm \(\|f'\|_{L^\infty[a,b]}\), the essential supremum with respect to Lebesgue measure on \([a, b]\).

public theorem_wanted absolutelyContinuousOnInterval_and_eLpNorm_deriv_lt_top_of_lipschitzOnWith
    {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b)
    (hf : LipschitzOnWith 1 f (Set.Icc a b)) :
    AbsolutelyContinuousOnInterval f a b ∧
      eLpNorm (fun x => deriv f x) ⊤ (volume.restrict (Set.Icc a b)) < ⊤

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_34.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.