English
Let μ: α → M(β) with each μ(a) finite, and suppose the β-measurable space is generated by a Pi-system S. If μ(a)(s) is measurable in a for all s ∈ S and μ(a)(univ) is measurable, then μ is measurable.
Русский
Пусть μ: α → M(β) такая, что каждая μ(a) конечна, а пространство β измеримо порождено Pi-системой S. Если a ↦ μ(a)(s) измерима для всех s ∈ S и a ↦ μ(a)(univ) измерима, то μ измеримо.
LaTeX
$$$Eq\\ m_β (MeasureSpace(genFrom(S))) \\to IsPiSystem(S) \\to (\\forall s\\in S, Measurable(\\lambda a. μ(a)(s))) \\to Measurable(\\lambda a. μ(a)(univ)) \\to Measurable μ.$$$
Lean4
theorem _root_.Measurable.measure_of_isPiSystem {μ : α → Measure β} [∀ a, IsFiniteMeasure (μ a)] {S : Set (Set β)}
(hgen : ‹MeasurableSpace β› = .generateFrom S) (hpi : IsPiSystem S) (h_basic : ∀ s ∈ S, Measurable fun a ↦ μ a s)
(h_univ : Measurable fun a ↦ μ a univ) : Measurable μ :=
by
rw [measurable_measure]
intro s hs
induction s, hs using MeasurableSpace.induction_on_inter hgen hpi with
| empty => simp
| basic s hs => exact h_basic s hs
| compl s hsm ihs =>
simp only [measure_compl hsm (measure_ne_top _ _)]
exact h_univ.sub ihs
| iUnion f hfd hfm ihf => simpa only [measure_iUnion hfd hfm] using .ennreal_tsum ihf
