Theorems · Theorem · measure theory

MeasureTheory.condExpL2_comp_continuousLinearMap

∀ {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [inst_4 : NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {E'' : Type u_8} (𝕜' : Type u_9) [inst_5 : RCLike 𝕜'] [inst_6 : NormedAddCommGroup E'']
  [inst_7 : InnerProductSpace 𝕜' E''] [inst_8 : CompleteSpace E''] [inst_9 : NormedSpace ℝ E''] (hm : m ≤ m0)
  (T : E' →L[ℝ] E'') (f : ↥(MeasureTheory.Lp E' 2 μ)),
  ↑↑↑((MeasureTheory.condExpL2 E'' 𝕜' hm) (T.compLp f)) =ᵐ[μ] ↑↑(T.compLp ↑((MeasureTheory.condExpL2 E' 𝕜 hm) f))

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpaceNormedSpaceRCLikeNormedAddCommGroupInnerProductSpaceCompleteSpaceNormedSpace