English
If s is measurable, then the densityProcess is measurable with respect to the product of the base and the n-th countable filtration.
Русский
Если s измеримо, то densityProcess относительно произведения сигма-алгебр и n-го счетного разбиения измеримо.
LaTeX
$$$\mathsf{Measurable}_{m_\alpha . \mathrm{prod}}\left( p \mapsto \dfrac{\kappa p.1(\text{countablePartitionSet }n p.2 \times^s s)}{\nu p.1(\text{countablePartitionSet }n p.2)} \right)$$$
Lean4
theorem measurable_densityProcess_countableFiltration_aux (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) {s : Set β}
(hs : MeasurableSet s) :
Measurable[mα.prod (countableFiltration γ n)]
(fun (p : α × γ) ↦ κ p.1 (countablePartitionSet n p.2 ×ˢ s) / ν p.1 (countablePartitionSet n p.2)) :=
by
change
Measurable[mα.prod (countableFiltration γ n)]
((fun (p : α × countablePartition γ n) ↦ κ p.1 (↑p.2 ×ˢ s) / ν p.1 p.2) ∘
(fun (p : α × γ) ↦ (p.1, ⟨countablePartitionSet n p.2, countablePartitionSet_mem n p.2⟩)))
have h1 : @Measurable _ _ (mα.prod ⊤) _ (fun p : α × countablePartition γ n ↦ κ p.1 (↑p.2 ×ˢ s) / ν p.1 p.2) :=
by
refine Measurable.div ?_ ?_
· refine measurable_from_prod_countable_left (fun t ↦ ?_)
exact Kernel.measurable_coe _ ((measurableSet_countablePartition _ t.prop).prod hs)
· refine measurable_from_prod_countable_left ?_
rintro ⟨t, ht⟩
exact Kernel.measurable_coe _ (measurableSet_countablePartition _ ht)
refine h1.comp (measurable_fst.prodMk ?_)
change
@Measurable (α × γ) (countablePartition γ n) (mα.prod (countableFiltration γ n)) ⊤
((fun c ↦ ⟨countablePartitionSet n c, countablePartitionSet_mem n c⟩) ∘ (fun p : α × γ ↦ p.2))
exact (measurable_countablePartitionSet_subtype n ⊤).comp measurable_snd
