English
Let ι be any index type and 𝓧 a measurable space with a probability measure μ. Then there exists a probability space and a family of random variables X_i : Ω → 𝓧 such that each X_i has law μ and the collection X_i is independent.
Русский
Пусть ι — произвольное множество индексов и 𝓧 — измеримое пространство с вероятностным распределением μ. Тогда существует вероятность пространство и семейство случайных величин X_i : Ω → 𝓧 так, что каждое X_i имеет закон μ, а множество X_i независимы.
LaTeX
$$$\exists Ω,\ ∃_\mathcal{F} \ P,\ X : ι \to Ω \to 𝓧,\ (∀ i, Measurable (X i)) ∧ (∀ i, HasLaw (X i) μ P) ∧ iIndepFun X P ∧ IsProbabilityMeasure P$$$
Lean4
theorem exists_iid (ι : Type v) {𝓧 : Type u} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) [IsProbabilityMeasure μ] :
∃ Ω : Type (max u v),
∃ _ : MeasurableSpace Ω,
∃ P : Measure Ω,
∃ X : ι → Ω → 𝓧, (∀ i, Measurable (X i)) ∧ (∀ i, HasLaw (X i) μ P) ∧ iIndepFun X P ∧ IsProbabilityMeasure P :=
exists_hasLaw_indepFun (fun _ ↦ 𝓧) (fun _ ↦ μ)
