measure_of_isPiSystem_of_isProbabilityMeasure

English

Let μ: α → M(β) be a family of probability measures and S generates the β-measurable space with IsPiSystem S. If μ(a)(s) is measurable for all s ∈ S, then μ is measurable.

Русский

Пусть μ: α → M(β) — последовательность распределений, вероятность каждой μ(a); β-σ-алгебра порождена S, IsPiSystem S. Если a ↦ μ(a)(s) измерима для всех s ∈ S, то μ измеримо.

LaTeX

$$$Eq\\ mβ (MeasureSpace(genFrom(S))) \\to IsPiSystem(S) \\to (\\forall s\\in S, Measurable(\\lambda a. μ(a)(s))) \\to Measurable μ.$$$

Lean4

theorem _root_.Measurable.measure_of_isPiSystem_of_isProbabilityMeasure {μ : α → Measure β}
    [∀ a, IsProbabilityMeasure (μ a)] {S : Set (Set β)} (hgen : ‹MeasurableSpace β› = .generateFrom S)
    (hpi : IsPiSystem S) (h_basic : ∀ s ∈ S, Measurable fun a ↦ μ a s) : Measurable μ :=
  .measure_of_isPiSystem hgen hpi h_basic <| by simp

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