English
Let seq be an antitone sequence of subsets of β with empty intersection and each seq m measurable. Then densityProcess κ ν n a x (seq m) converges to densityProcess κ ν n a x ∅ as m → ∞.
Русский
Пусть seq — антитонная последовательность подмножеств β с пересечением равным пустому множеству и все seq m измеримы. Тогда densityProcess κ ν n a x (seq m) сходится к densityProcess κ ν n a x ∅ при m → ∞.
LaTeX
$$$\displaystyle \lim_{m\to\infty} \densityProcess κ ν n a x (seq m) = \densityProcess κ ν n a x \emptyset$$$
Lean4
theorem tendsto_densityProcess_atTop_empty_of_antitone (κ : Kernel α (γ × β)) (ν : Kernel α γ) [IsFiniteKernel κ]
(n : ℕ) (a : α) (x : γ) (seq : ℕ → Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅)
(hseq_meas : ∀ m, MeasurableSet (seq m)) :
Tendsto (fun m ↦ densityProcess κ ν n a x (seq m)) atTop (𝓝 (densityProcess κ ν n a x ∅)) :=
by
simp_rw [densityProcess]
by_cases h0 : ν a (countablePartitionSet n x) = 0
· simp_rw [h0, ENNReal.toReal_div]
simp
refine (ENNReal.tendsto_toReal ?_).comp ?_
· rw [ne_eq, ENNReal.div_eq_top]
push_neg
simp
refine ENNReal.Tendsto.div_const ?_ (.inr h0)
have :
Tendsto (fun m ↦ κ a (countablePartitionSet n x ×ˢ seq m)) atTop
(𝓝 ((κ a) (⋂ n_1, countablePartitionSet n x ×ˢ seq n_1))) :=
by
apply tendsto_measure_iInter_atTop
· measurability
· exact fun _ _ h ↦ prod_mono_right <| hseq h
· exact ⟨0, measure_ne_top _ _⟩
simpa only [← prod_iInter, hseq_iInter] using this
