Theorems · Theorem · measure theory

MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable

∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {L : E →L[ℝ] F →L[ℝ] G} {u : ℝ → E} {v : ℝ → F} {u' : ℝ → E} {v' : ℝ → F},
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (fun x => (L (u x)) (v' x)) MeasureTheory.volume →
        MeasureTheory.Integrable (fun x => (L (u' x)) (v x)) MeasureTheory.volume →
          MeasureTheory.Integrable (fun x => (L (u x)) (v x)) MeasureTheory.volume →
            ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Integration by parts on (-∞, ∞). With respect to a general bilinear form, assuming moreover that the total function is integrable.

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace