English
The average over [a,b] equals the average over [b,a] because the underlying Lebesgue measure is symmetric with respect to interval endpoints.
Русский
Среднее по [a,b] равно среднему по [b,a] за счет симметрии меры Лебега относительно концов интервала.
LaTeX
$$$$ \text{average}_{[a,b]} f = \text{average}_{[b,a]} f. $$$$
Lean4
/-- **Integration by parts on (∞, a].**
For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`. -/
theorem integral_Iic_mul_deriv_eq_deriv_mul (hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x)
(hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x) (huv' : IntegrableOn (u * v') (Iic a))
(hu'v : IntegrableOn (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 = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x :=
by
rw [Pi.mul_def] at huv' hu'v
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
simpa only [add_comm] using integral_Iic_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty
