English
The composition product with the identity kernel equals the pushforward by the diagonal map: μ ⊗ₘ Kernel.id = μ.map (a ↦ (a, a)).
Русский
Композиционное произведение с единичным ядром равно отображению через диагональ: μ ⊗ₘ Kernel.id = μ.map (a ↦ (a, a)).
LaTeX
$$$[\\mathrm{SFinite}\\; μ] \\Rightarrow μ ⊗_m \\mathrm{Kernel.id} = μ.map (\\lambda x \\to (x, x))$$$
Lean4
theorem compProd_id [SFinite μ] : μ ⊗ₘ Kernel.id = μ.map (fun x ↦ (x, x)) :=
by
ext s hs
rw [compProd_apply hs, map_apply (measurable_id.prod measurable_id) hs]
have h_meas a : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs
simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)]
calc
∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ
_ = ∫⁻ a, ((fun x ↦ (x, x)) ⁻¹' s).indicator 1 a ∂μ := rfl
_ = μ ((fun x ↦ (x, x)) ⁻¹' s) := by
rw [lintegral_indicator_one]
exact (measurable_id.prod measurable_id) hs
