English
Let {𝓧_i} be a family of measurable spaces indexed by ι, and for each i a probability measure μ_i on 𝓧_i. Then there exists a probability space (Ω, 𝓕, P) and a family of random variables X_i : Ω → 𝓧_i such that each X_i has law μ_i, every X_i is measurable, the collection X_i is independent, and P is a probability measure.
Русский
Пусть имеется множество индексов ι и для каждого i∈ι задано измеримое пространство 𝓧_i и вероятность μ_i на 𝓧_i. Тогда существует вероятность пространство (Ω, 𝓕, P) и семейство случайных величин X_i : Ω → 𝓧_i так, что для каждого i векторная величина X_i имеет распределение μ_i, все X_i измеримы, семейство X_i независимы и P — вероятностное распределение.
LaTeX
$$$\exists Ω,\ \mathcal{F},\ P,\ X : (i : ι) \to Ω \to (\mathcal{X}_i),\ (∀ i,\ Measurable (X_i)) \land (∀ i, HasLaw (X_i) (μ_i) P) \land iIndepFun X P \land IsProbabilityMeasure P$$$
Lean4
theorem exists_hasLaw_indepFun {ι : Type v} (𝓧 : ι → Type u) {m𝓧 : ∀ i, MeasurableSpace (𝓧 i)}
(μ : (i : ι) → Measure (𝓧 i)) [hμ : ∀ i, IsProbabilityMeasure (μ i)] :
∃ Ω : Type (max u v),
∃ _ : MeasurableSpace Ω,
∃ P : Measure Ω,
∃ X : (i : ι) → Ω → (𝓧 i),
(∀ i, Measurable (X i)) ∧ (∀ i, HasLaw (X i) (μ i) P) ∧ iIndepFun X P ∧ IsProbabilityMeasure P :=
by
use Π i, (𝓧 i), .pi, infinitePi μ, fun i ↦ Function.eval i
refine ⟨by fun_prop, fun i ↦ MeasurePreserving.hasLaw (measurePreserving_eval_infinitePi _ _), ?_, by infer_instance⟩
rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), map_id']
congr
funext i
exact ((measurePreserving_eval_infinitePi μ i).map_eq).symm
