feat(MeasureTheory): add Lebesgue differentiation theorem for intervals (leanprover-community#29503)

Add the Lebesgue differentiation theorem for intervals. Part of originally planned leanprover-community#29092.

Author: zhuyizheng

Mathlib.lean

@@ -4608,6 +4608,7 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
+import Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
 import Mathlib.MeasureTheory.Integral.Layercake
 import Mathlib.MeasureTheory.Integral.Lebesgue

Mathlib/Analysis/Calculus/Deriv/Slope.lean

@@ -69,6 +69,10 @@ theorem hasDerivWithinAt_iff_tendsto_slope' (hs : x ∉ s) :
 theorem hasDerivAt_iff_tendsto_slope : HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[≠] x) (𝓝 f') :=
   hasDerivAtFilter_iff_tendsto_slope
 
+theorem hasDerivAt_iff_tendsto_slope_left_right [LinearOrder 𝕜] : HasDerivAt f f' x ↔
+    Tendsto (slope f x) (𝓝[<] x) (𝓝 f') ∧ Tendsto (slope f x) (𝓝[>] x) (𝓝 f') := by
+  simp [hasDerivAt_iff_tendsto_slope, ← Iio_union_Ioi, nhdsWithin_union]
+
 theorem hasDerivAt_iff_tendsto_slope_zero :
     HasDerivAt f f' x ↔ Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f') := by
   have : 𝓝[≠] x = Filter.map (fun t ↦ x + t) (𝓝[≠] 0) := by

Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2025 Yizheng Zhu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yizheng Zhu
+-/
+import Mathlib.Analysis.Calculus.Deriv.Slope
+import Mathlib.MeasureTheory.Covering.OneDim
+import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
+
+/-!
+# Lebesgue Differentiation Theorem (Interval Version)
+
+This file proves the interval version of the Lebesgue Differentiation Theorem. There are two
+versions in this file.
+
+* `LocallyIntegrable.ae_hasDerivAt_integral` is the global version. It states that if `f : ℝ → ℝ`
+is locally integrable, then for almost every `x`, for any `c : ℝ`, the derivative of
+`∫ (t : ℝ) in c..x, f t` at `x` is equal to `f x`.
+
+* `IntervalIntegrable.ae_hasDerivAt_integral` is the local version. It states that if `f : ℝ → ℝ`
+is interval integrable on `a..b`, then for almost every `x ∈ uIcc a b`, for any `c ∈ uIcc a b`, the
+derivative of `∫ (t : ℝ) in c..x, f t` at `x` is equal to `f x`.
+-/
+
+open MeasureTheory Set Filter Function IsUnifLocDoublingMeasure
+
+open scoped Topology
+
+/-- The (global) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → ℝ` is
+locally integrable, then for almost every `x`, for any `c : ℝ`, the derivative of
+`∫ (t : ℝ) in c..x, f t` at `x` is equal to `f x`. -/
+theorem LocallyIntegrable.ae_hasDerivAt_integral {f : ℝ → ℝ} (hf : LocallyIntegrable f volume) :
+    ∀ᵐ x, ∀ c, HasDerivAt (fun x => ∫ (t : ℝ) in c..x, f t) (f x) x := by
+  have hg (x y : ℝ) : IntervalIntegrable f volume x y :=
+    intervalIntegrable_iff.mpr <|
+      (hf.integrableOn_isCompact isCompact_uIcc).mono_set uIoc_subset_uIcc
+  have LDT := (vitaliFamily volume 1).ae_tendsto_average hf
+  have {a b : ℝ} : ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t :=
+    integral_Icc_eq_integral_Ioc (x := a) (y := b) (X := ℝ) |>.symm
+  filter_upwards [LDT] with x hx
+  intro c
+  rw [hasDerivAt_iff_tendsto_slope_left_right]
+  constructor
+  · refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left)
+    filter_upwards [self_mem_nhdsWithin] with y hy
+    replace hy : y ≤ x := by grind
+    simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
+        intervalIntegral.integral_of_ge, hy, this]
+    grind
+  · refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_right)
+    filter_upwards [self_mem_nhdsWithin] with y hy
+    replace hy : x ≤ y := by grind
+    simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
+        intervalIntegral.integral_of_le, hy, this]
+
+/-- The (local) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → ℝ` is
+interval integrable on `a..b`, then for almost every `x ∈ uIcc a b`, for any `c ∈ uIcc a b`, the
+derivative of `∫ (t : ℝ) in c..x, f t` at `x` is equal to `f x`. -/
+theorem IntervalIntegrable.ae_hasDerivAt_integral {f : ℝ → ℝ} {a b : ℝ}
+    (hf : IntervalIntegrable f volume a b) :
+    ∀ᵐ x, x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun x => ∫ (t : ℝ) in c..x, f t) (f x) x := by
+  wlog hab : a ≤ b
+  · exact uIcc_comm b a ▸ @this f b a hf.symm (by linarith)
+  rw [uIcc_of_le hab]
+  have h₁ : ∀ᵐ x, x ≠ a := by simp [ae_iff, measure_singleton]
+  have h₂ : ∀ᵐ x, x ≠ b := by simp [ae_iff, measure_singleton]
+  let g (x : ℝ) := if x ∈ Ioc a b then f x else 0
+  have hg : LocallyIntegrable g volume :=
+    integrableOn_congr_fun (by grind [EqOn]) (by simp) |>.mpr hf.left
+      |>.integrable_of_forall_notMem_eq_zero (by grind) |>.locallyIntegrable
+  filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hg, h₁, h₂] with x hx _ _ _
+  intro c hc
+  refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <| Ioo_mem_nhds (by grind) (by grind)
+  rw [show f x = g x by grind]
+  refine (hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_
+  all_goals apply intervalIntegral.integral_congr_ae' <;> filter_upwards <;> grind