English
For a fixed n and a, almost every x (with respect to the first marginal fst κ a) satisfies densityProcess κ (fst κ) n a x univ = 1.
Русский
Пусть для заданных n и a существует почти всюм x относительно fst κ a, для которых densityProcess κ (fst κ) n a x univ = 1.
LaTeX
$$$\\forall^{\\mathrm{ae}} x \\;\\partial(\\mathrm{fst}\\,κ\\,a),\\; \\densityProcess κ (fst κ) n a x univ = 1$$$
Lean4
theorem densityProcess_fst_univ [IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ) :
densityProcess κ (fst κ) n a x univ = if fst κ a (countablePartitionSet n x) = 0 then 0 else 1 :=
by
rw [densityProcess]
split_ifs with h
· simp only [h]
by_cases h' : κ a (countablePartitionSet n x ×ˢ univ) = 0
· simp [h']
· simp
· rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
have : countablePartitionSet n x ×ˢ univ = {p : γ × β | p.1 ∈ countablePartitionSet n x} :=
by
ext x
simp
rw [this, ENNReal.div_self]
· simp
· rwa [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h
· exact measure_ne_top _ _
