English
For integrable u,v and their derivatives on Iic a, the integral of u' v + u v' over Iic a equals a' − b' minus the integral of u v' across the left endpoint.
Русский
Для интегрируемых u,v и их производных на Iic a интеграл u' v + u v' по Iic a равен a' − b' минус интеграл uv' по левой границе.
LaTeX
$$$$ \int_{x \in Iic a} (u' x \cdot v x + u x \cdot v' x) \, dx = a' - b'. $$$$
Lean4
/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`. -/
theorem integral_Iic_deriv_mul_eq_sub (hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x)
(hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x) (huv : IntegrableOn (u' * v + u * v') (Iic a))
(h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')) (h_infty : Tendsto (u * v) atBot (𝓝 b')) :
∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b' :=
by
rw [← Iic_diff_right] at h_zero
let f := Function.update (u * v) a a'
have hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x :=
by
intro x hx
apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
filter_upwards [Iio_mem_nhds hx] with x (hx : x < a)
exact Function.update_of_ne (ne_of_lt hx) a' (u * v)
have htendsto : Tendsto f atBot (𝓝 b') := by
apply h_infty.congr'
filter_upwards [Iio_mem_atBot a] with x (hx : x < a)
exact (Function.update_of_ne (ne_of_lt hx) a' (u * v)).symm
simpa using integral_Iic_of_hasDerivAt_of_tendsto (continuousWithinAt_update_same.mpr h_zero) hderiv huv htendsto
