setIntegral_condExpInd — Mathlib

English

For a scalar c ∈ 𝕜 with SMul-commuting property, condExpInd is linear in x with respect to c.

Русский

Для скаляра c ∈ 𝕜 с свойством SMul-commute condExpInd линейно по x.

LaTeX

$$$ condExpInd\; F\; hm\; \mu\; s\; (c \cdot x) = c \cdot condExpInd\; F\; hm\; \mu\; s\; x,$$

Lean4

theorem setIntegral_condExpInd (hs : MeasurableSet[m] s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞)
    (x : G') : ∫ a in s, condExpInd G' hm μ t x a ∂μ = μ.real (t ∩ s) • x :=
  calc
    ∫ a in s, condExpInd G' hm μ t x a ∂μ = ∫ a in s, condExpIndSMul hm ht hμt x a ∂μ :=
      setIntegral_congr_ae (hm s hs) ((condExpInd_ae_eq_condExpIndSMul hm ht hμt x).mono fun _ hx _ => hx)
    _ = μ.real (t ∩ s) • x := setIntegral_condExpIndSMul hs ht hμs hμt x

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