English
A refined integration-by-parts identity for bilinear forms in a real finite-dimensional setting with a measure μ on E × ℝ.
Русский
Уточнённое тождество интегрирования по частям для билинейных форм в реалистичном конечномерном случае с мерой μ на E × ℝ.
LaTeX
$$$$ \int x\, B(f x) (g' x) \, dμ = - \int x\, B(f' x) (g x) \, dμ $$$$
Lean4
/-- **Integration by parts for Fréchet derivatives**
Version with a scalar function: `∫ f • g' = - ∫ f' • g` when `f • g'` and `f' • g` and `f • g`
are integrable, where `f'` and `g'` are the derivatives of `f` and `g` in a given direction `v`. -/
theorem integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable {f : E → 𝕜} {g : E → G} {v : E}
(hf'g : Integrable (fun x ↦ fderiv ℝ f x v • g x) μ) (hfg' : Integrable (fun x ↦ f x • fderiv ℝ g x v) μ)
(hfg : Integrable (fun x ↦ f x • g x) μ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
∫ x, f x • fderiv ℝ g x v ∂μ = -∫ x, fderiv ℝ f x v • g x ∂μ :=
integral_bilinear_fderiv_right_eq_neg_left_of_integrable (B := ContinuousLinearMap.lsmul ℝ 𝕜) hf'g hfg' hfg hf hg
