English
Under the same hypotheses as trajContent_tendsto_zero, a stronger version asserts the existence of a function l such that lmarginalPartialTraj converges to l, and ultimately trajContent tends to 0 when combined with indicator arguments.
Русский
При тех же предположениях trajContent_tendsto_zero даёт существование функции l, к которой сходится lmarginalPartialTraj, и в итоге trajContent стремится к 0 при учёте индикаторов.
LaTeX
$$$\\exists l,\\ Tendsto(\\lambda n. \\ lmarginalPartialTraj\\ κ\\ p\\ (a n) (\\chi n) (updateFinset x ...))_{atTop} (\\mathcal{N} 0)$$$
Lean4
/-- This is an auxiliary result for `trajContent_tendsto_zero`. Consider `f` a sequence of bounded
measurable functions such that `f n` depends only on the first coordinates up to `a n`.
Assume that when integrating `f n` against `partialTraj (k + 1) (a n)`, one gets a non-increasing
sequence of functions which converges to `l`.
Assume then that there exists `ε` and `y : Π i : Iic k, X i` such that
when integrating `f n` against `partialTraj k (a n) y`, you get something at least
`ε` for all `n`. Then there exists `z` such that this remains true when integrating
`f` against `partialTraj (k + 1) (a n) (update y (k + 1) z)`. -/
theorem le_lmarginalPartialTraj_succ {f : ℕ → (Π n, X n) → ℝ≥0∞} {a : ℕ → ℕ} (hcte : ∀ n, DependsOn (f n) (Iic (a n)))
(mf : ∀ n, Measurable (f n)) {bound : ℝ≥0∞} (fin_bound : bound ≠ ∞) (le_bound : ∀ n x, f n x ≤ bound) {k : ℕ}
(anti : ∀ x, Antitone (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x)) {l : (Π n, X n) → ℝ≥0∞}
(htendsto : ∀ x, Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))) (ε : ℝ≥0∞)
(y : Π i : Iic k, X i) (hpos : ∀ x n, ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)) :
∃ z, ∀ x n, ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (f n) (update (updateFinset x (Iic k) y) (k + 1) z) :=
by
have _ n : Nonempty (X n) := by
induction n using Nat.case_strong_induction_on with
| hz => exact ⟨y ⟨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⟩
-- `Fₙ` is the integral of `fₙ` from time `k + 1` to `aₙ`.
let F n : (Π n, X n) → ℝ≥0∞ :=
lmarginalPartialTraj κ (k + 1) (a n)
(f n)
-- `Fₙ` converges to `l` by hypothesis.
have tendstoF x : Tendsto (F · x) atTop (𝓝 (l x)) := htendsto x
have f_eq x n : lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x :=
by
simp_rw [F]
obtain h | h | h := lt_trichotomy (k + 1) (a n)
· rw [← lmarginalPartialTraj_self k.le_succ h.le (mf n)]
· rw [← h, lmarginalPartialTraj_le _ le_rfl (mf n)]
· rw [lmarginalPartialTraj_le _ _ (mf n), (hcte n).lmarginalPartialTraj_of_le _ (mf n),
(hcte n).lmarginalPartialTraj_of_le _ (mf n)]
all_goals
cutsat
-- `F` is also a bounded sequence.
have F_le n x : F n x ≤ bound := by
simpa [F, lmarginalPartialTraj] using
lintegral_le_const
(ae_of_all _ fun z ↦ le_bound _ _)
-- By dominated convergence, the integral of `fₙ` between time `k` and time `a n` converges
-- to the integral of `l` between time `k` and time `k + 1`.
have tendsto_int x :
Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop (𝓝 (lmarginalPartialTraj κ k (k + 1) l x)) :=
by
simp_rw [f_eq, lmarginalPartialTraj]
exact
tendsto_lintegral_of_dominated_convergence (fun _ ↦ bound)
(fun n ↦ (measurable_lmarginalPartialTraj _ _ (mf n)).comp measurable_updateFinset)
(fun n ↦ Eventually.of_forall <| fun y ↦ F_le n _) (by simp [fin_bound])
(Eventually.of_forall (fun _ ↦ tendstoF _))
-- By hypothesis, we have `ε ≤ lmarginalPartialTraj κ k (k + 1) (F n) (updateFinset x _ y)`,
-- so this is also true for `l`.
have ε_le_lint x : ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x _ y) :=
ge_of_tendsto (tendsto_int _) (by simp [hpos])
let x_ : Π n, X n := Classical.ofNonempty
obtain ⟨x, hx⟩ : ∃ x, ε ≤ l (update (updateFinset x_ _ y) (k + 1) x) :=
by
have : ∫⁻ x, l (update (updateFinset x_ _ y) (k + 1) x) ∂(κ k y) ≠ ∞ :=
ne_top_of_le_ne_top fin_bound <|
lintegral_le_const <| ae_of_all _ fun y ↦ le_of_tendsto' (tendstoF _) <| fun _ ↦ F_le _ _
obtain ⟨x, hx⟩ := exists_lintegral_le this
refine ⟨x, (ε_le_lint x_).trans ?_⟩
rwa [lmarginalPartialTraj_succ, frestrictLe_updateFinset]
exact ENNReal.measurable_of_tendsto (by fun_prop) (tendsto_pi_nhds.2 htendsto)
refine
⟨x, fun x' n ↦ ?_⟩
-- As `F` is a non-increasing sequence, we have `ε ≤ Fₙ(y, x)` for any `n`.
have :=
le_trans hx
((anti _).le_of_tendsto (tendstoF _) n)
-- This part below is just to say that this is true for any `x : (i : ι) → X i`,
-- as `Fₙ` technically depends on all the variables, but really depends only on the first `k + 1`.
convert this using 1
refine (hcte n).dependsOn_lmarginalPartialTraj _ (mf n) fun i hi ↦ ?_
simp only [update, updateFinset, mem_Iic]
split_ifs with h1 h2 <;> try rfl
rw [mem_coe, mem_Iic] at hi
cutsat
