isFiniteMeasureOnCompacts — Mathlib

English

If each component μ_i has finite measure on compact sets, then the product measure on the product space has finite measure on compacts.

Русский

Если каждая мерa μ_i конечна на компактах, тогда произведение μ на произведении пространств имеет конечную меру на компактах.

LaTeX

$$$\bigl(\forall i, IsFiniteMeasureOnCompacts(\mu_i)\bigr) \Rightarrow IsFiniteMeasureOnCompacts(\pi\mu)$$$

Lean4

instance isFiniteMeasureOnCompacts [∀ i, TopologicalSpace (α i)] [∀ i, IsFiniteMeasureOnCompacts (μ i)] :
    IsFiniteMeasureOnCompacts (MeasureTheory.Measure.pi μ) :=
  by
  constructor
  intro K hK
  suffices Measure.pi μ (Set.univ.pi fun j => Function.eval j '' K) < ⊤ by
    exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this
  rw [Measure.pi_pi]
  refine WithTop.prod_lt_top ?_
  exact fun i _ => IsCompact.measure_lt_top (IsCompact.image hK (continuous_apply i))

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