deterministic_prod_apply' — Mathlib

English

For a measurable f: α → β and κ: Kernel α γ with IsSFiniteKernel κ, for any a ∈ α and any measurable set s ⊆ β × γ, the product at a assigns κ a-measure to the preimage of s under the map b ↦ (f(a), b).

Русский

Для измеримого f: α → β и κ: Kernel α γ, для любого a ∈ α и измеримого множества s ⊆ β × γ верно: ((deterministic f hf) ×ₖ κ) a (s) = κ a ( { (f(a), b) ∈ s } ) = κ a ( Prod.mk (f a) ⁻¹' s ).

LaTeX

$$$\\displaystyle ((\\mathrm{deterministic} f hf) \\times_K \\kappa) a (s) = \\kappa a (\\mathrm{Prod.mk}(f a)^{-1} s)$$$

Lean4

theorem deterministic_prod_apply' {f : α → β} (mf : Measurable f) (κ : Kernel α γ) [IsSFiniteKernel κ] (a : α)
    {s : Set (β × γ)} (hs : MeasurableSet s) : ((Kernel.deterministic f mf) ×ₖ κ) a s = κ a (Prod.mk (f a) ⁻¹' s) :=
  by
  rw [prod_apply' _ _ _ hs, lintegral_deterministic']
  exact measurable_measure_prodMk_left hs

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