Differentiation of real functions

Absolutely continuous, Lipschitz and bounded-variation functions of a real variable, maximal functions and almost-everywhere properties of real functions.

• Absolutely continuous functions
• Hardy–Littlewood maximal function

TheoremJordan decomposition of a continuous function of bounded variation#●ready to prove

Let \(F : \mathbb{R} \to \mathbb{R}\) be continuous and of bounded variation on all of \(\mathbb{R}\). Then there are continuous non-decreasing functions \(F_1, F_2 : \mathbb{R} \to \mathbb{R}\) such that \(F = F_1 - F_2\).

public theorem_wanted exists_continuous_monotone_sub_of_boundedVariationOn
    {F : ℝ → ℝ} (hF_bv : BoundedVariationOn F (Set.univ : Set ℝ))
    (hF_cont : Continuous F) :
    ∃ F₁ F₂ : ℝ → ℝ, Monotone F₁ ∧ Continuous F₁ ∧ Monotone F₂ ∧ Continuous F₂ ∧ F = F₁ - F₂

Sources

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

TheoremNo continuous function agrees a.e. with the indicator of \((0,1)\)#●ready to prove

Let \(\chi_{[0,1]}\) be the characteristic function of \([0,1]\). There is no continuous function \(f : \mathbb{R} \to \mathbb{R}\) such that \(f(x) = \chi_{[0,1]}(x)\) for almost every \(x \in \mathbb{R}\) with respect to Lebesgue measure.

public theorem_wanted not_exists_continuous_ae_eq_indicator_Icc : ¬ ∃ f : ℝ → ℝ, Continuous f ∧
  (∀ᵐ x ∂(MeasureTheory.volume), f x = Set.indicator (Set.Icc (0 : ℝ) 1) (fun _ => (1 : ℝ)) x)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Measure and integration; Classical measure theory), problem ma_proofbench_l1_28.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.