condExpL1CLM_indicatorConstLp — Mathlib

English

For a measurable s with finite μ(s), condExpL1CLM on indicatorConstLp equals condExpInd: condExpL1CLM F' hm μ ↑(indicatorConstLp 1 hs hμs x) = condExpInd F' hm μ s x.

Русский

Для измеримого s с конечной μ(s) condExpL1CLM на индикаторе константа равна condExpInd.

LaTeX

$$$ condExpL1CLM\; F'\; hm\; μ\; ↑(indicatorConstLp\; 1\; hs\; hμs\; x) = condExpInd\; F'\; hm\; μ\; s\; x,$$

Lean4

theorem condExpL1CLM_indicatorConstLp (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : F') :
    (condExpL1CLM F' hm μ) (indicatorConstLp 1 hs hμs x) = condExpInd F' hm μ s x :=
  L1.setToL1_indicatorConstLp (dominatedFinMeasAdditive_condExpInd F' hm μ) hs hμs x

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