comp_snd_map_prod_id — Mathlib

English

The conditional expectation kernel condExpKernel equals the condDistrib kernel comapped along the identity, i.e., condExpKernel μ m equals condDistrib id id μ comap id.

Русский

Условное ожидание ядра совпадает с ядром CondDistrib через идентити-мэппинг: condExpKernel μ m = condDistrib id id μ comap id.

LaTeX

$$$$ \\operatorname{condExpKernel}(μ, m) = (\\operatorname{condDistrib}(id, id, μ)).comap(identity). $$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id [TopologicalSpace F] (hm : m ≤ mΩ)
    (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable[m.prod mΩ] (fun x : Ω × Ω => f x.2)
      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω => (id ω, id ω)) μ) :=
  by
  rw [← aestronglyMeasurable_comp_snd_map_prodMk_iff (measurable_id'' hm)] at hf
  simp_rw [id] at hf ⊢
  exact hf

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