English
The long, technical lemma (trajContent_tendsto_zero) provides a method to prove the existence of traj and its sigma-additivity by showing the decrease to zero of cylinder contents and controlling lmarginalPartialTraj through dominated convergence and indicator arguments.
Русский
Длинная техническая лемма trajContent_tendsto_zero обеспечивает существование traj и его σ-аддитивность через убывание содержимого цилиндров и управление lmarginalPartialTraj через домогодную схождение и индикаторные аргументы.
LaTeX
$$$\\text{trajContent\\_tendsto\\_zero}$$$
Lean4
/-- This is the key theorem to prove the existence of the `traj`:
the `trajContent` of a decreasing sequence of cylinders with empty intersection
converges to `0`.
This implies the `σ`-additivity of `trajContent`
(see `addContent_iUnion_eq_sum_of_tendsto_zero`),
which allows to extend it to the `σ`-algebra by Carathéodory's theorem. -/
theorem trajContent_tendsto_zero {A : ℕ → Set (Π n, X n)} (A_mem : ∀ n, A n ∈ measurableCylinders X)
(A_anti : Antitone A) (A_inter : ⋂ n, A n = ∅) {p : ℕ} (x₀ : Π i : Iic p, X i) :
Tendsto (fun n ↦ trajContent κ x₀ (A n)) atTop (𝓝 0) :=
by
have _ n : Nonempty (X n) := by
induction n using Nat.case_strong_induction_on with
| hz => exact ⟨x₀ ⟨0, mem_Iic.2 (zero_le _)⟩⟩
| hi m
hm =>
have : Nonempty (Π i : Iic m, X i) := ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
exact
ProbabilityMeasure.nonempty
⟨κ m Classical.ofNonempty, inferInstance⟩
-- `Aₙ` is a cylinder, it can be written as `cylinder (Iic (a n)) Sₙ`.
have A_cyl n : ∃ a S, MeasurableSet S ∧ A n = cylinder (Iic a) S := by simpa [measurableCylinders_nat] using A_mem n
choose a S mS A_eq using A_cyl
let χ n :=
(A n).indicator
(1 : (Π n, X n) → ℝ≥0∞)
-- `χₙ` is measurable.
have mχ n : Measurable (χ n) := by
simp_rw [χ, A_eq]
exact (measurable_indicator_const_iff 1).2 <| (mS n).cylinder
have χ_dep n : DependsOn (χ n) (Iic (a n)) := by
simp_rw [χ, A_eq]
exact
dependsOn_cylinder_indicator_const ..
-- Therefore its integral against `partialTraj κ k (a n)` is constant.
have lma_const x y n :
lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x _ x₀) =
lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y _ x₀) :=
by
refine (χ_dep n).dependsOn_lmarginalPartialTraj p (mχ n) fun i hi ↦ ?_
rw [mem_coe, mem_Iic] at hi
simp [updateFinset, hi]
-- As `(Aₙ)` is non-increasing, so is `(χₙ)`.
have χ_anti : Antitone χ := fun m n hmn y ↦
by
apply Set.indicator_le fun a ha ↦ ?_
simp [χ, A_anti hmn ha]
-- Integrating `χₙ` further than the last coordinate it depends on does nothing.
-- This is used to then show that the integral of `χₙ` from time `k` is non-increasing.
have lma_inv k M n (h : a n ≤ M) : lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n) :=
(χ_dep n).lmarginalPartialTraj_const_right (mχ n) h le_rfl
have anti_lma k x : Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x :=
by
intro m n hmn
simp only
rw [← lma_inv k ((a n).max (a m)) n (le_max_left _ _), ← lma_inv k ((a n).max (a m)) m (le_max_right _ _)]
exact
lmarginalPartialTraj_mono _ _ (χ_anti hmn)
_
-- Therefore it converges to some function `lₖ`.
have this k x : ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l) :=
by
obtain h | h := tendsto_of_antitone (anti_lma k x)
· rw [OrderBot.atBot_eq] at h
exact ⟨0, h.mono_right <| pure_le_nhds 0⟩
· exact h
choose l hl using this
have l_const x y : l p (updateFinset x _ x₀) = l p (updateFinset y _ x₀) :=
by
have := hl p (updateFinset x _ x₀)
simp_rw [lma_const x y] at this
exact tendsto_nhds_unique this (hl p _)
obtain ⟨ε, hε⟩ : ∃ ε, ∀ x, l p (updateFinset x _ x₀) = ε :=
⟨l p (updateFinset Classical.ofNonempty _ x₀), fun x ↦ l_const _ _⟩
-- As the sequence is decreasing, `ε ≤ ∫ χₙ`.
have hpos x n : ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x _ x₀) :=
hε x ▸ ((anti_lma p _).le_of_tendsto (hl p _)) n
have χ_le n x : χ n x ≤ 1 := by
apply Set.indicator_le
simp
-- We have all the conditions to apply `le_lmarginalPartialTraj_succ`.
-- This allows us to recursively build a sequence `z` with the following property:
-- for any `k ≥ p` and `n`, integrating `χ n` from time `k` to time `a n`
-- with the trajectory up to `k` being equal to `z` gives something greater than `ε`.
choose! ind hind using fun k y h ↦
le_lmarginalPartialTraj_succ χ_dep mχ (by simp : (1 : ℝ≥0∞) ≠ ∞) χ_le (anti_lma (k + 1)) (hl (k + 1)) ε y h
let z := iterateInduction x₀ ind
have main k (hk : p ≤ k) : ∀ x n, ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x _ (frestrictLe k z)) := by
induction k, hk using Nat.le_induction with
| base => exact fun x n ↦ by simpa [z, frestrictLe_iterateInduction] using hpos x n
| succ k hn h =>
intro x n
convert hind k (fun i ↦ z i.1) h x n
ext i
simp only [updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite, update, z]
split_ifs with h1 h2 h3 h4 h5
any_goals cutsat
cases h2
rw [iterateInduction, dif_neg (by cutsat)]
-- We now want to prove that the integral of `χₙ`, which is equal to the `trajContent`
-- of `Aₙ`, converges to `0`.
have aux x n : trajContent κ x₀ (A n) = lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x _ x₀) :=
by
simp_rw [χ, A_eq]
nth_rw 1 [← frestrictLe_updateFinset x x₀]
exact trajContent_eq_lmarginalPartialTraj (mS n) ..
simp_rw [aux z]
convert hl p _
rw [hε]
-- Which means that we want to prove that `ε = 0`. But if `ε > 0`, then for any `n`,
-- choosing `k > aₙ` we get `ε ≤ χₙ(z₀, ..., z_{aₙ})` and therefore `z ∈ Aₙ`.
-- This contradicts the fact that `(Aₙ)` has an empty intersection.
by_contra!
have mem n : z ∈ A n :=
by
have : 0 < χ n z :=
by
rw [← lmarginalPartialTraj_le κ (le_max_right p (a n)) (mχ n), ← updateFinset_frestrictLe (a := a n) z]
simpa using lt_of_lt_of_le this.symm.bot_lt (main _ (le_max_left _ _) z n)
exact Set.mem_of_indicator_ne_zero (ne_of_lt this).symm
exact (A_inter ▸ Set.mem_iInter.2 mem).elim
