Theorems · Theorem · real analysis

MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le

∀ {f : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    MonotoneOn f (Set.Icc a b) →
      ∃ G,
        (∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b),
            Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (deriv f x))) ∧
          (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) (MeasureTheory.volume.restrict (Set.Icc a b))) ∧
            Filter.liminf (fun n => ∫⁻ (x : ℝ) in Set.Icc a b, ‖G n x‖ₑ) Filter.atTop ≤ ENNReal.ofReal (f b - f a)

If f is monotone on [a, b], then f' is the limit of G n a.e. on [a, b], where each G n is AEStronglyMeasurable and the liminf of the lower Lebesgue integral of ‖G n ·‖ₑ is at most f b - f a.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Cited by

2 results in Mathlib

Foundations

Depth 265 from the axioms · uses propext, Classical.choice, Quot.sound