English
The main integration-by-parts identity for line derivatives: under integrability assumptions for hf'g, hfg', hfg and HasLineDerivAt for f, g, the equality holds.
Русский
Главное тождество интегрирования по частям для линейных производных: при выполнении условий интегрируемости для hf'g, hfg', hfg и HasLineDerivAt для f, g равенство верно.
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 two scalar functions: `∫ 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_mul_fderiv_eq_neg_fderiv_mul_of_integrable {f : E → 𝕜} {g : E → 𝕜} {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.mul ℝ 𝕜) hf'g hfg' hfg hf hg
