English
Integration by parts for a bilinear form L on E × F over the real line: if u, v have derivatives u', v' and the bilinear products are integrable, then the integral of L(u, v') + L(u', v) equals the difference n − m where m,n are the end limits of the bilinear term.
Русский
Интегрирование по частям для билинеарной формы L на E × F: если функции u,v дифференцируемы и соответствующие линейные комбинации интегрируемы, то интеграл L(u, v') + L(u', v) равен n − m, где m,n — пределы на бесконечности.
LaTeX
$$$$ \int_{\mathbb{R}} \bigl( L(u x, v' x) + L(u' x, v x) \bigr) \, dx = n - m, $$$$
Lean4
theorem integrableOn_Ioi_comp_mul_left_iff (f : ℝ → E) (c : ℝ) {a : ℝ} (ha : 0 < a) :
IntegrableOn (fun x => f (a * x)) (Ioi c) ↔ IntegrableOn f (Ioi <| a * c) :=
by
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi c)]
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi <| a * c)]
convert integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne' using 2
ext1 x
rw [← indicator_comp_right, preimage_const_mul_Ioi _ ha, mul_comm a c, mul_div_cancel_right₀ _ ha.ne',
Function.comp_def]
