Integration by parts for line derivatives

Let f, g : E → ℝ be two differentiable functions on a real vector space endowed with a Haar measure. Then ∫ f * g' = - ∫ f' * g, where f' and g' denote the derivatives of f and g in a given direction v, provided that f * g, f' * g and f * g' are all integrable.

In this file, we prove this theorem as well as more general versions where the multiplication is replaced by a general continuous bilinear form, giving versions both for the line derivative and the Fréchet derivative. These results are derived from the one-dimensional version and a Fubini argument.

Main statements

• integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable: integration by parts in terms of line derivatives, with HasLineDerivAt assumptions and general bilinear form.
• integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable: integration by parts in terms of Fréchet derivatives, with HasFDerivAt assumptions and general bilinear form.
• integral_bilinear_fderiv_right_eq_neg_left_of_integrable: integration by parts in terms of Fréchet derivatives, written with fderiv assumptions and general bilinear form.
• integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable: integration by parts for scalar action, in terms of Fréchet derivatives, written with fderiv assumptions.
• integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable: integration by parts for scalar multiplication, in terms of Fréchet derivatives, written with fderiv assumptions.

Implementation notes

A standard set of assumptions for integration by parts in a finite-dimensional real vector space (without boundary term) is that the functions tend to zero at infinity and have integrable derivatives. In this file, we instead assume that the functions are integrable and have integrable derivatives. These sets of assumptions are not directly comparable (an integrable function with integrable derivative does not have to tend to zero at infinity). The one we use is geared towards applications to Fourier transforms.

TODO: prove similar theorems assuming that the functions tend to zero at infinity and have integrable derivatives.

theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1 {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] {f f' : E × ℝ → F} {g g' : E × ℝ → G} {B : F →L[ℝ] G →L[ℝ] W} (hf'g : MeasureTheory.Integrable (fun (x : E × ℝ) => (B (f' x)) (g x)) (μ.prod MeasureTheory.volume)) (hfg' : MeasureTheory.Integrable (fun (x : E × ℝ) => (B (f x)) (g' x)) (μ.prod MeasureTheory.volume)) (hfg : MeasureTheory.Integrable (fun (x : E × ℝ) => (B (f x)) (g x)) (μ.prod MeasureTheory.volume)) (hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)) (hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)) : ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ.prod MeasureTheory.volume = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.prod MeasureTheory.volume

theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2 {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure (E × ℝ)} [μ.IsAddHaarMeasure] {f f' : E × ℝ → F} {g g' : E × ℝ → G} {B : F →L[ℝ] G →L[ℝ] W} (hf'g : MeasureTheory.Integrable (fun (x : E × ℝ) => (B (f' x)) (g x)) μ) (hfg' : MeasureTheory.Integrable (fun (x : E × ℝ) => (B (f x)) (g' x)) μ) (hfg : MeasureTheory.Integrable (fun (x : E × ℝ) => (B (f x)) (g x)) μ) (hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)) (hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)) : ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ

theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {f f' : E → F} {g g' : E → G} {v : E} {B : F →L[ℝ] G →L[ℝ] W} (hf'g : MeasureTheory.Integrable (fun (x : E) => (B (f' x)) (g x)) μ) (hfg' : MeasureTheory.Integrable (fun (x : E) => (B (f x)) (g' x)) μ) (hfg : MeasureTheory.Integrable (fun (x : E) => (B (f x)) (g x)) μ) (hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v) (hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v) : ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ

Integration by parts for line 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 {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {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 : MeasureTheory.Integrable (fun (x : E) => (B ((f' x) v)) (g x)) μ) (hfg' : MeasureTheory.Integrable (fun (x : E) => (B (f x)) ((g' x) v)) μ) (hfg : MeasureTheory.Integrable (fun (x : E) => (B (f x)) (g x)) μ) (hf : ∀ (x : E), HasFDerivAt f (f' x) x) (hg : ∀ (x : E), HasFDerivAt g (g' x) x) : ∫ (x : E), (B (f x)) ((g' x) v) ∂μ = -∫ (x : E), (B ((f' x) v)) (g x) ∂μ

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_fderiv_right_eq_neg_left_of_integrable {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {f : E → F} {g : E → G} {v : E} {B : F →L[ℝ] G →L[ℝ] W} (hf'g : MeasureTheory.Integrable (fun (x : E) => (B ((fderiv ℝ f x) v)) (g x)) μ) (hfg' : MeasureTheory.Integrable (fun (x : E) => (B (f x)) ((fderiv ℝ g x) v)) μ) (hfg : MeasureTheory.Integrable (fun (x : E) => (B (f x)) (g x)) μ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : ∫ (x : E), (B (f x)) ((fderiv ℝ g x) v) ∂μ = -∫ (x : E), (B ((fderiv ℝ f x) v)) (g x) ∂μ

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_smul_fderiv_eq_neg_fderiv_smul_of_integrable {E : Type u_1} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {𝕜 : Type u_5} [NormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 G] {f : E → 𝕜} {g : E → G} {v : E} (hf'g : MeasureTheory.Integrable (fun (x : E) => (fderiv ℝ f x) v • g x) μ) (hfg' : MeasureTheory.Integrable (fun (x : E) => f x • (fderiv ℝ g x) v) μ) (hfg : MeasureTheory.Integrable (fun (x : E) => f x • g x) μ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : ∫ (x : E), f x • (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v • g x ∂μ

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_mul_fderiv_eq_neg_fderiv_mul_of_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {𝕜 : Type u_5} [NormedField 𝕜] [NormedAlgebra ℝ 𝕜] {f g : E → 𝕜} {v : E} (hf'g : MeasureTheory.Integrable (fun (x : E) => (fderiv ℝ f x) v * g x) μ) (hfg' : MeasureTheory.Integrable (fun (x : E) => f x * (fderiv ℝ g x) v) μ) (hfg : MeasureTheory.Integrable (fun (x : E) => f x * g x) μ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : ∫ (x : E), f x * (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v * g x ∂μ

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.