condExpIndSMul_empty — Mathlib

English

The conditional expectation IndSMul on the empty set vanishes for any x.

Русский

Условное ожидание IndSMul на пустом множестве равно нулю.

LaTeX

$$$\operatorname{condExpIndSMul} hm MeasurableSet.empty ((measure_empty (\mu := μ)).le.trans_lt ENNReal.coe_lt_top).ne x = 0$$$

Lean4

theorem condExpIndSMul_empty {x : G} :
    condExpIndSMul hm MeasurableSet.empty ((measure_empty (μ := μ)).le.trans_lt ENNReal.coe_lt_top).ne x = 0 :=
  by
  rw [condExpIndSMul, indicatorConstLp_empty]
  simp only [Submodule.coe_zero, ContinuousLinearMap.map_zero]

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