instIsFiniteMeasureOnCompacts — Mathlib

English

If μ and ν are probability measures, then their product is a probability measure on α × β.

Русский

Если μ и ν являются вероятностьными мерами, то их произведение является вероятностной мерой на α × β.

LaTeX

$$$\text{IsProbabilityMeasure}(μ \mathrm{.prod} ν)$$$

Lean4

instance instIsFiniteMeasureOnCompacts {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {mα : MeasurableSpace α}
    {mβ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) [IsFiniteMeasureOnCompacts μ]
    [IsFiniteMeasureOnCompacts ν] : IsFiniteMeasureOnCompacts (μ.prod ν) where
  lt_top_of_isCompact K
    hK :=
    calc
      μ.prod ν K ≤ μ.prod ν ((Prod.fst '' K) ×ˢ (Prod.snd '' K)) := measure_mono subset_prod
      _ ≤ μ (Prod.fst '' K) * ν (Prod.snd '' K) := (prod_prod_le _ _)
      _ < ∞ := mul_lt_top (hK.image continuous_fst).measure_lt_top (hK.image continuous_snd).measure_lt_top

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