pi_Ioi_ae_eq_pi_Ici — Mathlib

English

Similarly, the product of Ioi(f_i) across I is a.e. equal to the product of Ici(f_i) under the product measure when underlying assumptions hold.

Русский

Аналогично, произведение Ioi(f_i) по I равно почти наверняка Ici(f_i) под произведением мер при сохранности условий.

LaTeX

$$$(\\mathrm{pi}\\; s\\; (\\lambda i.\\; \\mathrm{Ioi}(f_i))) =_{a.e.}^{\\mathrm{Measure.pi}\\; \\mu} (\\mathrm{pi}\\; s\\; (\\lambda i.\\; \\mathrm{Ici}(f_i)))$$$

Lean4

theorem pi_Ioi_ae_eq_pi_Ici {s : Set ι} {f : ∀ i, α i} :
    (pi s fun i => Ioi (f i)) =ᵐ[Measure.pi μ] pi s fun i => Ici (f i) :=
  ae_eq_set_pi fun _ _ => Ioi_ae_eq_Ici

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