condExpL2 — Mathlib

English

If f is AEStronglyMeasurable, then condExpL2 E 𝕜 hm f is AEStronglyMeasurable.

Русский

Если f AEStronglyMeasurable, то condExpL2 E 𝕜 hm f является AEStronglyMeasurable.

LaTeX

$$AEStronglyMeasurable [m] (condExpL2 E 𝕜 hm f)$$

Lean4

/-- Conditional expectation of a function in L2 with respect to a sigma-algebra -/
noncomputable def condExpL2 (hm : m ≤ m0) : (α →₂[μ] E) →L[𝕜] lpMeas E 𝕜 m 2 μ :=
  haveI : Fact (m ≤ m0) := ⟨hm⟩
  (lpMeas E 𝕜 m 2 μ).orthogonalProjection

Похожие утверждения