condKernel_apply_of_ne_zero — Mathlib

English

A lemma about condKernel for prod maps: the fst component of a mapped κ equals the mapped κ after conditioning.

Русский

Лемма о condKernel для отображённых произведений: проекция fst сопоставленного κ равна отображённому κ после условного распределения.

LaTeX

$$$fst (map κ (Prod.map (id) e)) ⊗ η = map κ (Prod.map (id) e) \\Rightarrow fst κ ⊗ borelMarkovFromReal Ω η = κ$$$

Lean4

/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`,
`ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` . -/
theorem _root_.MeasureTheory.Measure.condKernel_apply_of_ne_zero [MeasurableSingletonClass α] {x : α}
    (hx : ρ.fst { x } ≠ 0) (s : Set Ω) : ρ.condKernel x s = (ρ.fst { x })⁻¹ * ρ ({ x } ×ˢ s) :=
  Measure.IsCondKernel.apply_of_ne_zero _ _ hx _

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