apply_of_ne_zero — Mathlib

English

If κ is a kernel α → β × Ω and κCond a CondKernel for ρ, then κ.fst ⊗ₖ κCond = κ.

Русский

Если κ — ядро α → β × Ω, а κCond — CondKernel для ρ, то κ.fst ⊗ₖ κCond = κ.

LaTeX

$$$\\kappa_{\\mathrm{fst}} \\otimes_k \\kappa_{\\mathrm{Cond}} = \\kappa.$$$

Lean4

/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`,
`ρCond x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` . -/
theorem apply_of_ne_zero [MeasurableSingletonClass α] {x : α} (hx : ρ.fst { x } ≠ 0) (s : Set Ω) :
    ρCond x s = (ρ.fst { x })⁻¹ * ρ ({ x } ×ˢ s) :=
  by
  have : ρCond x s = ((ρ.fst { x })⁻¹ • ρ).comap (fun (y : Ω) ↦ (x, y)) s :=
    by
    congr 2 with s hs
    simp [IsCondKernel.apply_of_ne_zero_of_measurableSet _ _ hx hs, (measurableEmbedding_prodMk_left x).comap_apply,
      Set.singleton_prod]
  simp [this, (measurableEmbedding_prodMk_left x).comap_apply, Set.singleton_prod]

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