English
If the sequence seq is monotone and its union is univ, then densityProcess κ (fst κ) n a x (seq m) tends to densityProcess κ (fst κ) n a x univ as m → ∞, for each x.
Русский
Если последовательность seq монотонна и её объединение равно всеобщему множеству, то densityProcess κ (fst κ) n a x (seq m) сходится к densityProcess κ (fst κ) n a x univ при m → ∞ для каждого x.
LaTeX
$$$\\operatorname{Tendsto}\\left(m \\mapsto \\densityProcess κ (fst κ) n a x (seq m)\\right)_{\\operatorname{atTop}} (\\mathcal{N}\\bigl(\\densityProcess κ (fst κ) n a x univ\\bigr))$$$
Lean4
theorem densityProcess_fst_univ_ae (κ : Kernel α (γ × β)) [IsFiniteKernel κ] (n : ℕ) (a : α) :
∀ᵐ x ∂(fst κ a), densityProcess κ (fst κ) n a x univ = 1 :=
by
rw [ae_iff]
have : {x | ¬densityProcess κ (fst κ) n a x univ = 1} ⊆ {x | fst κ a (countablePartitionSet n x) = 0} :=
by
intro x hx
simp only [mem_setOf_eq] at hx ⊢
rw [densityProcess_fst_univ] at hx
simpa using hx
refine measure_mono_null this ?_
have :
{x | fst κ a (countablePartitionSet n x) = 0} ⊆ ⋃ (u) (_ : u ∈ countablePartition γ n) (_ : fst κ a u = 0), u :=
by
intro t ht
simp only [mem_setOf_eq, mem_iUnion, exists_prop] at ht ⊢
exact ⟨countablePartitionSet n t, countablePartitionSet_mem _ _, ht, mem_countablePartitionSet _ _⟩
refine measure_mono_null this ?_
rw [measure_biUnion]
· simp
· exact (finite_countablePartition _ _).countable
· intro s hs t ht hst
simp only [disjoint_iUnion_right, disjoint_iUnion_left]
exact fun _ _ ↦ disjoint_countablePartition hs ht hst
· intro s hs
by_cases h : fst κ a s = 0
· simp [h, measurableSet_countablePartition n hs]
· simp [h]
