condExpIndL1Fin_ae_eq_condExpIndSMul

English

If s is measurable and μ(s) ≠ ∞, condExpIndL1 hm μ s x equals condExpIndL1Fin hm hs hμs x.

Русский

Если s измеримо и μ(s) ≠ ∞, то condExpIndL1 hm μ s x=condExpIndL1Fin hm hs hμs x.

LaTeX

$$$condExpIndL1_of_measurableSet_of_measure_ne_top hm μ s x = condExpIndL1Fin hm hs hμs x$$$

Lean4

theorem condExpIndL1Fin_ae_eq_condExpIndSMul (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (x : G) : condExpIndL1Fin hm hs hμs x =ᵐ[μ] condExpIndSMul hm hs hμs x :=
  (integrable_condExpIndSMul hm hs hμs x).coeFn_toL1

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