fst_sum — Mathlib

English

The first marginal of a sum of measures equals the sum of the first marginals: (sum μ).fst = sum (μ n).fst.

Русский

Первая маргинальная сумма мера равна сумме их первых маргиналок.

LaTeX

$$$$ (\\mathrm{sum}\\,\\mu).fst = \\mathrm{sum}\\ (\\lambda n, (\\mu n).fst) $$$$

Lean4

theorem fst_sum {ι : Type*} (μ : ι → Measure (α × β)) : (sum μ).fst = sum (fun n ↦ (μ n).fst) :=
  Measure.map_sum measurable_fst.aemeasurable

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