English
Let seq be monotone and its union be univ. Then almost surely in x (with respect to fst κ a), densityProcess κ (fst κ) n a x (seq m) tends to 1.
Русский
Пусть seq монотонна и объединение равно всеобщему множеству. Тогда почти наверняка по x выполняется, что densityProcess κ (fst κ) n a x (seq m) стремится к 1.
LaTeX
$$$\\text{ae}_{x\\sim (fst\\,κ\\,a)}\\; \\lim_{m\\to\\infty} densityProcess κ (fst κ) n a x (seq m) = 1$$$
Lean4
theorem tendsto_densityProcess_fst_atTop_univ_of_monotone (κ : Kernel α (γ × β)) (n : ℕ) (a : α) (x : γ)
(seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = univ) :
Tendsto (fun m ↦ densityProcess κ (fst κ) n a x (seq m)) atTop (𝓝 (densityProcess κ (fst κ) n a x univ)) :=
by
simp_rw [densityProcess]
refine (ENNReal.tendsto_toReal ?_).comp ?_
· rw [ne_eq, ENNReal.div_eq_top]
push_neg
simp_rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
constructor
· refine fun h h0 ↦ h (measure_mono_null (fun x ↦ ?_) h0)
simp only [mem_prod, mem_setOf_eq, and_imp]
exact fun h _ ↦ h
· refine fun h_top ↦ eq_top_mono (measure_mono (fun x ↦ ?_)) h_top
simp only [mem_prod, mem_setOf_eq, and_imp]
exact fun h _ ↦ h
by_cases h0 : fst κ a (countablePartitionSet n x) = 0
· rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0 ⊢
suffices ∀ m, κ a (countablePartitionSet n x ×ˢ seq m) = 0
by
simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]
suffices κ a (countablePartitionSet n x ×ˢ univ) = 0 by simp only [this, ENNReal.zero_div]
convert h0
ext x
simp only [mem_prod, mem_univ, and_true, mem_setOf_eq]
refine fun m ↦ measure_mono_null (fun x ↦ ?_) h0
simp only [mem_prod, mem_setOf_eq, and_imp]
exact fun h _ ↦ h
refine ENNReal.Tendsto.div_const ?_ ?_
· convert tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)
rw [← prod_iUnion, hseq_iUnion]
· exact Or.inr h0
