English
Given u,v with right derivatives on (a,b) and interval-integrable u', v', then ∫ (u' v) + (u v') equals boundary terms.
Русский
Если у функций есть правая производная на (a,b) и u', v' интегрируемы на интервале, то ∫ (u' v + u v') равен разности на концах.
LaTeX
$$$\\int_{a}^{b} (u'(x) v(x) + u(x) v'(x))\\,dx = u(b) v(b) - u(a) v(a) - \\int_{a}^{b} u(x) v'(x)\\,dx$$$
Lean4
/-- When the right derivative of a function is nonnegative, then it is automatically integrable. -/
theorem integrableOn_deriv_right_of_nonneg (hcont : ContinuousOn g (Icc a b))
(hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x) :
IntegrableOn g' (Ioc a b) := by
by_cases hab : a < b; swap
· simp [Ioc_eq_empty hab]
rw [integrableOn_Ioc_iff_integrableOn_Ioo]
have meas_g' : AEMeasurable g' (volume.restrict (Ioo a b)) :=
by
apply (aemeasurable_derivWithin_Ioi g _).congr
refine (ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_
exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _)
suffices H : (∫⁻ x in Ioo a b, ‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a) from
⟨meas_g'.aestronglyMeasurable, H.trans_lt ENNReal.ofReal_lt_top⟩
by_contra! H
obtain ⟨f, fle, fint, hf⟩ :
∃ f : SimpleFunc ℝ ℝ≥0,
(∀ x, f x ≤ ‖g' x‖₊) ∧ (∫⁻ x : ℝ in Ioo a b, f x) < ∞ ∧ ENNReal.ofReal (g b - g a) < ∫⁻ x : ℝ in Ioo a b, f x :=
exists_lt_lintegral_simpleFunc_of_lt_lintegral H
let F : ℝ → ℝ := (↑) ∘ f
have intF : IntegrableOn F (Ioo a b) :=
by
refine ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, ?_⟩
simpa only [F, hasFiniteIntegral_iff_enorm, comp_apply, NNReal.enorm_eq] using fint
have A : ∫⁻ x : ℝ in Ioo a b, f x = ENNReal.ofReal (∫ x in Ioo a b, F x) := lintegral_coe_eq_integral _ intF
rw [A] at hf
have B : (∫ x : ℝ in Ioo a b, F x) ≤ g b - g a :=
by
rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le hab.le]
refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_
· rwa [integrableOn_Icc_iff_integrableOn_Ioo]
· convert NNReal.coe_le_coe.2 (fle x)
simp only [Real.norm_of_nonneg (g'pos x hx), coe_nnnorm]
exact lt_irrefl _ (hf.trans_le (ENNReal.ofReal_le_ofReal B))
