English
Integration by parts for scalar multiplication: ∫ f · fderiv g · v = − ∫ fderiv f · g · v under suitable integrability and differentiability hypotheses.
Русский
Интегрирование по частям для скалярного умножения: при условии интегрируемости и дифференцируемости выполняется тождество.
LaTeX
$$$$ \int x\; f x \cdot fderiv 𝕜 g x v \, dμ = - \int x\; f x \cdot fderiv 𝕜 f x v \, dμ $$$$
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 the derivatives
of `f` and `g` in a given direction `v`, then `∫ B f g' = - ∫ B f' g`. -/
theorem integral_bilinear_fderiv_right_eq_neg_left_of_integrable {f : E → F} {g : E → G} {v : E} {B : F →L[ℝ] G →L[ℝ] W}
(hf'g : Integrable (fun x ↦ B (fderiv ℝ f x v) (g x)) μ) (hfg' : Integrable (fun x ↦ B (f x) (fderiv ℝ g x v)) μ)
(hfg : Integrable (fun x ↦ B (f x) (g x)) μ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
∫ x, B (f x) (fderiv ℝ g x v) ∂μ = -∫ x, B (fderiv ℝ f x v) (g x) ∂μ :=
integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable hf'g hfg' hfg (fun x ↦ (hf x).hasFDerivAt)
(fun x ↦ (hg x).hasFDerivAt)
