condExpInd — Mathlib

English

For measurable s with finite μ(s) and any x, condExpInd on s equals condExpIndSMul almost everywhere on α (i.e., they agree μ-almost everywhere).

Русский

Для измеримого s с конечной μ(s) и любого x_condExpInd на s совпадает с condExpIndSMul почти наверняка на α.

LaTeX

$$$ condExpInd\; hm\; \mu\; s\; x =_a.e. condExpIndSMul\; hm\; hs\; hμs\; x,$$

Lean4

/-- Conditional expectation of the indicator of a set, as a linear map from `G` to L1. -/
def condExpInd {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (s : Set α) :
    G →L[ℝ] α →₁[μ] G where
  toFun := condExpIndL1 hm μ s
  map_add' := condExpIndL1_add
  map_smul' := condExpIndL1_smul
  cont := continuous_condExpIndL1

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