Theorems · Theorem · probability

StrongDual.toLp_of_not_memLp

∀ {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)], ¬MeasureTheory.MemLp id p μ → ∀ (L : StrongDual 𝕜 E), (StrongDual.toLp μ p) L = 0

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