condExpInd_of_measurable — Mathlib

English

If s is measurable and μ(s) is finite, then condExpInd on s equals the indicator-based simple expression: condExpInd G hm μ s x = indicatorConstLp 1 (hm s hs) hμs x.

Русский

Если s измеримо и μ(s) конечна, то условное ожидание на s равно индикаторной константе: condExpInd = indicatorConstLp 1 … x.

LaTeX

$$$ condExpInd\; G\; hm\; \mu\; s\; x = indicatorConstLp\; 1\; (hm s hs)\; hμs\; x,$$

Lean4

theorem condExpInd_of_measurable (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) (c : G) :
    condExpInd G hm μ s c = indicatorConstLp 1 (hm s hs) hμs c :=
  by
  ext1
  grw [indicatorConstLp_coeFn, condExpInd_ae_eq_condExpIndSMul, condExpIndSMul_ae_eq_smul]
  rw [condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)]
  filter_upwards [@indicatorConstLp_coeFn α _ _ 2 μ _ s (hm s hs) hμs (1 : ℝ)] with x hx
  rw [hx]
  by_cases hx_mem : x ∈ s <;> simp [hx_mem]

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