condExpL1CLM_indicatorConst — Mathlib

English

For measurable set s and finite μ(s), condExpL1CLM on indicatorConstLp equals condExpInd.

Русский

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

LaTeX

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

Lean4

theorem condExpL1CLM_indicatorConst (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : F') :
    (condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs hμs x) = condExpInd F' hm μ s x := by
  rw [Lp.simpleFunc.coe_indicatorConst]; exact condExpL1CLM_indicatorConstLp hs hμs x

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