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 : ℝ → 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 : ℝ → 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 LocallyIntegrable.ae_hasDerivAt_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) => ∫ (t : ℝ) in c..x, f t) (f x) x

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 IntervalIntegrable.ae_hasDerivAt_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) : ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → ∀ c ∈ Set.uIcc a b, HasDerivAt (fun (x : ℝ) => ∫ (t : ℝ) in c..x, f t) (f x) x

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.