English
If f is locally integrable, then for almost every x in the interval, the derivative of the integral of f from c to x with respect to x equals f(x).
Русский
Если f локально интегрируема, то почти во всех точках x внутри интервала производная интеграла от c до x по x равна f(x).
LaTeX
$$$\\displaystyle \\text{ae}_{x} \\; \\forall c,\\; \\frac{d}{dx}\\Big|_{x} \\int_c^x f(t) \\,dt = f(x)$$$
Lean4
/-- 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 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]
