Theorems · Definition · probability

StrongDual.toLp

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {mE : MeasurableSpace E} →
      {𝕜 : Type u_2} →
        [inst_1 : RCLike 𝕜] →
          [inst_2 : NormedSpace 𝕜 E] →
            [OpensMeasurableSpace E] →
              (μ : MeasureTheory.Measure E) →
                (p : ENNReal) → [inst_4 : Fact (1 ≤ p)] → StrongDual 𝕜 E →L[𝕜] ↥(MeasureTheory.Lp 𝕜 p μ)

Continuous linear map from the dual to Lp equal to MemLp.toLp if MemLp id p μ and to 0 otherwise.

Defined in

Mathlib.Probability.Moments.CovarianceBilinDual

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeNormedSpaceOpensMeasurableSpaceFact