English
Integration by parts for Fréchet derivatives: if hf'g, hfg', hfg are integrable and f, g are differentiable, then ∫ B(f) (g' v) = − ∫ B(f' v) (g).
Русский
Интегрирование по Частям для Фрéче-деривативов: если hf'g, hfg', hfg интегрируемы и f, g дифференцируемы, то ∫ B(f) (g' v) = − ∫ B(f' v) (g).
LaTeX
$$$$ \int x\, B(f x) \bigl(g' x\bigr) v \, d\mu = - \int x\, B(f' x) \bigl(g x\bigr) \, d\mu $$$$
Lean4
/-- **Integration by parts for Fréchet derivatives**
Version with a general bilinear form `B`.
If `B f g` is integrable, as well as `B f' g` and `B f g'` where `f'` and `g'` are derivatives
of `f` and `g` in a given direction `v`, then `∫ B f g' = - ∫ B f' g`. -/
theorem integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable {f : E → F} {f' : E → (E →L[ℝ] F)} {g : E → G}
{g' : E → (E →L[ℝ] G)} {v : E} {B : F →L[ℝ] G →L[ℝ] W} (hf'g : Integrable (fun x ↦ B (f' x v) (g x)) μ)
(hfg' : Integrable (fun x ↦ B (f x) (g' x v)) μ) (hfg : Integrable (fun x ↦ B (f x) (g x)) μ)
(hf : ∀ x, HasFDerivAt f (f' x) x) (hg : ∀ x, HasFDerivAt g (g' x) x) :
∫ x, B (f x) (g' x v) ∂μ = -∫ x, B (f' x v) (g x) ∂μ :=
integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable hf'g hfg' hfg (fun x ↦ (hf x).hasLineDerivAt v)
(fun x ↦ (hg x).hasLineDerivAt v)
