apply_eq_measure_condKernel_of_compProd_eq

English

In the real-valued kernel setting, the a.e. equality of condKernel with the sliced kernel holds when ρ = ρ.fst.compProd κ.

Русский

В настройке с Real ядер condKernel совпадает почти наверху с срезанным ядром, если ρ = ρ.fst.compProd κ.

LaTeX

$$$\\forall x, (κ x) = ρ.condKernel x$ a.e.$$

Lean4

theorem apply_eq_measure_condKernel_of_compProd_eq {ρ : Kernel α (β × Ω)} [IsFiniteKernel ρ] {κ : Kernel (α × β) Ω}
    [IsFiniteKernel κ] (hκ : Kernel.fst ρ ⊗ₖ κ = ρ) (a : α) : (fun b ↦ κ (a, b)) =ᵐ[Kernel.fst ρ a] (ρ a).condKernel :=
  by
  have : ρ a = (ρ a).fst ⊗ₘ Kernel.comap κ (fun b ↦ (a, b)) measurable_prodMk_left :=
    by
    ext s hs
    conv_lhs => rw [← hκ]
    rw [Measure.compProd_apply hs, Kernel.compProd_apply hs]
    rfl
  have h := eq_condKernel_of_measure_eq_compProd _ this
  rw [Kernel.fst_apply]
  filter_upwards [h] with b hb
  rw [← hb, Kernel.comap_apply]

Похожие утверждения