inducedFamily — Mathlib

English

If each μ_n is S-finite, then the induced family on any finite index I is also S-finite. This ensures the finite-dimensional marginals are well-behaved.

Русский

Если каждый μ_n является S-конечной, то и индуцированное семейство на любом конечном индексе I тоже S-конечное. Это обеспечивает корректность конечномерных маргиналов.

LaTeX

$$$ [∀ n, SFinite (μ n)] (I : Finset ℕ) : SFinite (inducedFamily μ I)$$$

Lean4

/-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, we can define a family
of measures indexed by `Finset ℕ` by projecting the measures. -/
noncomputable def inducedFamily (S : Finset ℕ) : Measure ((k : S) → X k) :=
  (μ (S.sup id)).map (restrict₂ S.subset_Iic_sup_id)

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