condExpL1CLM — Mathlib

English

Dominated FinMeasAdditive property holds for condExpInd with bound 1.

Русский

Свойство доминируемости FinMeasAdditive для condExpInd со значениею 1.

LaTeX

$$$ \text{DominatedFinMeasAdditive}\; μ\; (condExpInd\; G\; hm\; μ)\; 1,$$

Lean4

/-- Conditional expectation of a function as a linear map from `α →₁[μ] F'` to itself. -/
def condExpL1CLM (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] : (α →₁[μ] F') →L[ℝ] α →₁[μ] F' :=
  L1.setToL1 (dominatedFinMeasAdditive_condExpInd F' hm μ)

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