Theorems · Theorem · real analysis

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} [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}
  [MeasureTheory.SigmaFinite μ] {f f' : E × ℝ → F} {g g' : E × ℝ → G} {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) (μ.prod MeasureTheory.volume) →
    MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) (μ.prod MeasureTheory.volume) →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) (μ.prod MeasureTheory.volume) →
        (∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)) →
          (∀ x ∈ tsupport f, 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

Defined in

Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceMeasurableSpaceMeasureTheory.SigmaFinite