Theorems · Theorem · probability

StrongDual.toLp_apply

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal}
  {𝕜 : Type u_2} [inst_1 : RCLike 𝕜] [inst_2 : NormedSpace 𝕜 E] [inst_3 : OpensMeasurableSpace E]
  [inst_4 : Fact (1 ≤ p)] (h_Lp : MeasureTheory.MemLp id p μ) (L : StrongDual 𝕜 E),
  (StrongDual.toLp μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯

Defined in

Mathlib.Probability.Moments.CovarianceBilinDual

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeNormedSpaceOpensMeasurableSpaceFact