English
For bilinear operator L on E × F with u,v differentiable, the improper integral across the real line of L(u x, v′ x) + L(u' x, v x) equals n − m when the total integrand is integrable and the boundary bilinear term tends to m and n at ±∞ respectively.
Русский
Для билинейной формы L на E × F и функций u,v дифференцируемых, интеграл
∫ L(u x, v′ x) + L(u' x, v x) dx по ℝ равен n − m при условии интегрируемости и пределов bilinear в ±∞.
LaTeX
$$$$ \int_{-\infty}^{\infty} \bigl( L(u x, v' x) + L(u' x, v x) \bigr) \, dx = n - m, $$$$
Lean4
theorem integral_bilinear_hasDerivAt_eq_sub [CompleteSpace G] (hu : ∀ x, HasDerivAt u (u' x) x)
(hv : ∀ x, HasDerivAt v (v' x) x) (huv : Integrable (fun x ↦ L (u x) (v' x) + L (u' x) (v x)))
(h_bot : Tendsto (fun x ↦ L (u x) (v x)) atBot (𝓝 m)) (h_top : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 n)) :
∫ (x : ℝ), L (u x) (v' x) + L (u' x) (v x) = n - m :=
integral_of_hasDerivAt_of_tendsto (fun x ↦ L.hasDerivAt_of_bilinear (hu x) (hv x)) huv h_bot h_top
