Theorems · Definition · measure theory

MeasureTheory.L1.integralCLM

{α : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : NormedSpace ℝ E] → [CompleteSpace E] → ↥(MeasureTheory.Lp E 1 μ) →L[ℝ] E

The Bochner integral in L1 space as a continuous linear map over ℝ.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.L1

Cited by

16 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace