From c42cd4c65ce697014b61eba15f3ea2b67fe6e9f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20=C4=8Cert=C3=ADk?= Date: Tue, 23 Jun 2026 14:49:10 -0600 Subject: [PATCH 1/3] feat: generalize ae_hasDerivAt_integral to Banach MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalize both interval-version Lebesgue differentiation theorems `LocallyIntegrable.ae_hasDerivAt_integral` and `IntervalIntegrable.ae_hasDerivAt_integral` from real-valued functions `f : ℝ → ℝ` to functions `f : ℝ → E` valued in a Banach space `E`. The existing proof already goes through the vector-valued averaging theorem `VitaliFamily.ae_tendsto_average`, so the only change is replacing scalar multiplication `*` by `•` in the slope computation. --- .../LebesgueDifferentiationThm.lean | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean index 2654b47e2e7e3b..490b6e652c333e 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean @@ -15,11 +15,11 @@ public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic 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`. +* `LocallyIntegrable.ae_hasDerivAt_integral` is the global version. It states that if `f : ℝ → E` + is locally integrable (`E` a Banach space), 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 : ℝ → ℝ` +* `IntervalIntegrable.ae_hasDerivAt_integral` is the local version. It states that if `f : ℝ → E` 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`. -/ @@ -30,10 +30,11 @@ open MeasureTheory Set Filter Function IsUnifLocDoublingMeasure open scoped Topology -/-- The (global) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → ℝ` is +/-- The (global) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → E` 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) : +theorem LocallyIntegrable.ae_hasDerivAt_integral {E : Type*} [NormedAddCommGroup E] + [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (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 <| @@ -48,24 +49,25 @@ theorem LocallyIntegrable.ae_hasDerivAt_integral {f : ℝ → ℝ} (hf : Locally · refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left) filter_upwards [self_mem_nhdsWithin] with y hy replace hy : y ≤ x := hy.le - suffices -((y - x)⁻¹ * ∫ (t : ℝ) in Icc y x, f t) = (x - y)⁻¹ * ∫ (t : ℝ) in Icc y x, f t by + suffices -((y - x)⁻¹ • ∫ (t : ℝ) in Icc y x, f t) = (x - y)⁻¹ • ∫ (t : ℝ) in Icc y x, f t by simpa [slope, average, intervalIntegral.integral_interval_sub_left, hg, intervalIntegral.integral_of_ge, hy, h] - rw [← neg_mul, neg_inv, neg_sub] + rw [← neg_smul, neg_inv, neg_sub] · refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_right) filter_upwards [self_mem_nhdsWithin] with y hy replace hy : x ≤ y := hy.le simp [slope, average, intervalIntegral.integral_interval_sub_left, hg, intervalIntegral.integral_of_le, hy, h] -/-- The (local) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → ℝ` is +/-- The (local) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → E` 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 : ℝ} +theorem IntervalIntegrable.ae_hasDerivAt_integral {E : Type*} [NormedAddCommGroup E] + [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {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) + · exact uIcc_comm b a ▸ @this E _ _ _ 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] From 8c1bb5b5f11a80c235cc8662ea81c189d2ab8d2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20=C4=8Cert=C3=ADk?= Date: Tue, 23 Jun 2026 16:45:24 -0600 Subject: [PATCH 2/3] Update Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean Co-authored-by: Eric Wieser --- .../Integral/IntervalIntegral/LebesgueDifferentiationThm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean index 490b6e652c333e..4c4f162280c8ee 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean @@ -67,7 +67,7 @@ theorem IntervalIntegrable.ae_hasDerivAt_integral {E : Type*} [NormedAddCommGrou (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 E _ _ _ f b a hf.symm (by linarith) + · exact uIcc_comm b a ▸ this 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] From b459ac2de99de4dbe7fbdba3886da3bf8a9c06bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20=C4=8Cert=C3=ADk?= Date: Wed, 24 Jun 2026 16:55:18 -0600 Subject: [PATCH 3/3] chore: move shared assumptions into a variable line --- .../IntervalIntegral/LebesgueDifferentiationThm.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean index 4c4f162280c8ee..23dad80410b6b8 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean @@ -30,11 +30,12 @@ open MeasureTheory Set Filter Function IsUnifLocDoublingMeasure open scoped Topology +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] + /-- The (global) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → E` 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 {E : Type*} [NormedAddCommGroup E] - [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : LocallyIntegrable f volume) : +theorem LocallyIntegrable.ae_hasDerivAt_integral {f : ℝ → E} (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 <| @@ -62,8 +63,7 @@ theorem LocallyIntegrable.ae_hasDerivAt_integral {E : Type*} [NormedAddCommGroup /-- The (local) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → E` 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 {E : Type*} [NormedAddCommGroup E] - [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ} +theorem IntervalIntegrable.ae_hasDerivAt_integral {f : ℝ → E} {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