English
For hm with m ≤ mΩ, the composed measure (μ.trim hm) ⊗ₘ condExpKernel μ m equals the push-forward of μ by the map ω ↦ (ω, ω).
Русский
Для hm с m ≤ mΩ композиция (μ.trim hm) ⊗ₘ condExpKernel μ m равна отображению меры μ через отображение ω ↦ (ω, ω).
LaTeX
$$$(μ.trim hm)\\otimes_{m} condExpKernel(μ,m)\\;=\\; Measure.map\\bigl(\\omega\\mapsto(\\text{id}(\\omega),\\text{id}(\\omega))\\bigr)\\mu$$$
Lean4
theorem compProd_trim_condExpKernel (hm : m ≤ mΩ) :
(μ.trim hm) ⊗ₘ condExpKernel μ m = @Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ :=
by
rcases isEmpty_or_nonempty Ω with h | h
· simp [Measure.eq_zero_of_isEmpty μ]
rw [condExpKernel_eq]
have : m ⊓ mΩ = m := inf_of_le_left hm
have h := compProd_map_condDistrib (mβ := m) (μ := μ) (X := id) measurable_id.aemeasurable
rw [← h, trim_eq_map hm]
congr 1
ext a s hs
simp only [Kernel.coe_comap, Function.comp_apply, id_eq]
congr
