instSFinite — Mathlib

English

Under appropriate hypotheses, a measure on a product space is determined by its values on rectangles generated by a Pi-system.

Русский

При подходящих предположениях мера на произведении пространства задаётся её значениями на прямоугольниках, образованных Pi-системой.

LaTeX

$$prod_eq_generateFrom$$

Lean4

instance instSFinite {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α} [SFinite μ] {_ : MeasurableSpace β}
    {ν : Measure β} [SFinite ν] : SFinite (μ.prod ν) :=
  by
  have : μ.prod ν = Measure.sum (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)) :=
    by
    conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
    apply prod_sum
  rw [this]
  infer_instance

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