pi_caratheodory — Mathlib

English

The product measure π is Carathéodory-measurable with respect to the product of Carathéodory measures from the coordinates.

Русский

Произведение меры π является каратейодорной по отношению к произведению мер координат.

LaTeX

$$pi m ≤ caratheodory$$

Lean4

theorem pi_caratheodory : MeasurableSpace.pi ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory :=
  by
  refine iSup_le ?_
  intro i s hs
  rw [MeasurableSpace.comap] at hs
  rcases hs with ⟨s, hs, rfl⟩
  apply boundedBy_caratheodory
  intro t
  simp_rw [piPremeasure]
  refine Finset.prod_add_prod_le' (Finset.mem_univ i) ?_ ?_ ?_
  · simp [image_inter_preimage, image_diff_preimage, measure_inter_add_diff _ hs, le_refl]
  · rintro j - _; gcongr; apply inter_subset_left
  · rintro j - _; gcongr; apply diff_subset

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