Theorems · Theorem · real analysis

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} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : 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},
  MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) μ →
    MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) μ →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ →
        (∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v) →
          (∀ x ∈ tsupport f, 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.

Defined in

Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Cited by

2 results in Mathlib

Foundations

Depth 285 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure