English
If f is interval-integrable and locally well-behaved, then the Lebesgue version of integration-by-parts holds on the interval.
Русский
Если f интегрируема по интервалу и удовлетворяет условиям Лебега, то формула IBP действует на интервале.
LaTeX
$$$\\displaystyle \\text{ae}_{x} \\; x\\in uIcc(a,b) \\Rightarrow \\int_a^b f'(x)(g\\circ f)(x) \\,dx = \\int_{f(a)}^{f(b)} g(u) \\,du$$$
Lean4
/-- 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 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
