English
The infinite product measure is the projective limit of its finite marginals: infinitePi μ is the projective limit of the system I ↦ π (μ_i) indexed by finite sets I.
Русский
Бесконечное произведение меры является проективным пределом своих конечных маргиналов: infinitePi μ — проективный предел системы I ↦ π_i μ_i.
LaTeX
$$$$\text{IsProjectiveLimit}\bigl(\mathrm{infinitePi}\,\mu,\;I\mapsto \mathrm{Measure.pi}(\mu|_I)\bigr).$$$$
Lean4
/-- This is the key theorem to build the product of an arbitrary family of probability measures:
the `piContent` of a decreasing sequence of cylinders with empty intersection converges to `0`.
This implies the `σ`-additivity of `piContent` (see `addContent_iUnion_eq_sum_of_tendsto_zero`),
which allows to extend it to the `σ`-algebra by Carathéodory's theorem. -/
theorem piContent_tendsto_zero {A : ℕ → Set (Π i, X i)} (A_mem : ∀ n, A n ∈ measurableCylinders X) (A_anti : Antitone A)
(A_inter : ⋂ n, A n = ∅) : Tendsto (fun n ↦ piContent μ (A n)) atTop (𝓝 0) :=
by
have : ∀ i, Nonempty (X i) := fun i ↦ ProbabilityMeasure.nonempty ⟨μ i, hμ i⟩
have A_cyl n : ∃ s S, MeasurableSet S ∧ A n = cylinder s S := (mem_measurableCylinders _).1 (A_mem n)
choose s S mS A_eq using A_cyl
let u := ⋃ n, (s n).toSet
let t n : Finset u := (s n).preimage Subtype.val Subtype.val_injective.injOn
classical
-- The map `f` allows to pull back `Aₙ`
let f : (Π i : u, X i) → Π i, X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
let aux n : t n ≃ s n :=
{ toFun := fun i ↦ ⟨i.1.1, mem_preimage.1 i.2⟩
invFun := fun i ↦ ⟨⟨i.1, Set.mem_iUnion.2 ⟨n, i.2⟩⟩, mem_preimage.2 i.2⟩
left_inv := fun i ↦ by simp
right_inv := fun i ↦ by simp }
-- Finally `gₙ` is the equivalence between the product indexed by `tₙ` and the one indexed by `sₙ`
let g n :=
(aux n).piCongrLeft
(fun i : s n ↦ X i)
-- Mapping from the product indexed by `u` by `f` and then restricting to `sₙ` is the same as
-- first restricting to `tₙ` and then mapping by `gₙ`
have r_comp_f n : (s n).restrict ∘ f = (g n) ∘ (fun (x : Π i : u, X i) i ↦ x i) :=
by
ext x i
simp only [Function.comp_apply, Finset.restrict, Equiv.piCongrLeft_apply, Equiv.coe_fn_symm_mk, f, aux, g, t]
rw [dif_pos (Set.mem_iUnion.2 ⟨n, i.2⟩)]
-- `Bₙ` is the same as `Aₙ` but in the product indexed by `u`
let B n :=
f ⁻¹'
(A n)
-- `Tₙ` is the same as `Sₙ` but in the product indexed by `u`
let T n :=
(g n) ⁻¹'
(S n)
-- We now transfer the properties of `Aₙ` and `Sₙ` to `Bₙ` and `Tₙ`
have B_eq n : B n = cylinder (t n) (T n) := by simp_rw [B, A_eq, cylinder, ← Set.preimage_comp, r_comp_f]; rfl
have mT n : MeasurableSet (T n) := (mS n).preimage (by fun_prop)
have B_mem n : B n ∈ measurableCylinders (fun i : u ↦ X i) :=
(mem_measurableCylinders (B n)).2 ⟨t n, T n, mT n, B_eq n⟩
have mB n : MeasurableSet (B n) := .of_mem_measurableCylinders (B_mem n)
have B_anti : Antitone B := fun m n hmn ↦ Set.preimage_mono <| A_anti hmn
have B_inter : ⋂ n, B n = ∅ := by
simp_rw [B, ← Set.preimage_iInter, A_inter, Set.preimage_empty]
-- We now rewrite `piContent μ (A n)` as `piContent (fun i : u ↦ μ i) (B n)`. Then there are two
-- cases: either `u` is finite and we rewrite it to the finite product measure, either
-- it is countable and we rewrite it to the pushforward measure of `infinitePiNat`. In both cases
-- we have an actual measure and we can conclude with `tendsto_measure_iInter_atTop`.
conv =>
enter [1]; ext n
rw [A_eq, piContent_cylinder μ (mS n), ← pi_map_piCongrLeft (aux n), map_apply (by fun_prop) (mS n)]
change (Measure.pi (fun i : t n ↦ μ i)) (T n)
rw [← piContent_cylinder (fun i : u ↦ μ i) (mT n), ← B_eq n]
obtain u_fin | u_inf := finite_or_infinite u
· let _ := Fintype.ofFinite u
simp_rw [fun n ↦ piContent_eq_measure_pi (fun i : u ↦ μ i) (mB n)]
convert tendsto_measure_iInter_atTop (fun n ↦ (mB n).nullMeasurableSet) B_anti ⟨0, measure_ne_top _ _⟩
· rw [B_inter, measure_empty]
· infer_instance
· -- If `u` is infinite, then we have an equivalence with `ℕ` so we can apply `secondLemma`.
have count_u : Countable u := Set.countable_iUnion (fun n ↦ (s n).countable_toSet)
obtain ⟨φ, -⟩ := Classical.exists_true_of_nonempty (α := ℕ ≃ u) nonempty_equiv_of_countable
conv => enter [1]; ext n; rw [← infinitePiNat_map_piCongrLeft _ φ (B_mem n)]
convert tendsto_measure_iInter_atTop (fun n ↦ (mB n).nullMeasurableSet) B_anti ⟨0, measure_ne_top _ _⟩
· rw [B_inter, measure_empty]
· infer_instance
