compProd_preimage_fst — Mathlib

English

For measurable s ⊆ β, (κ ⊗ₖ η) x (fst^{-1}(s)) = κ x s.

Русский

Для измеримого s ⊆ β выполняется (κ ⊗ₖ η) x (fst^{-1}(s)) = κ x s.

LaTeX

$$$$ (\kappa \otimes_k \eta)(x)(\operatorname{fst}^{-1}(s)) = \kappa(x)(s). $$$$

Lean4

theorem compProd_preimage_fst {s : Set β} (hs : MeasurableSet s) (κ : Kernel α β) (η : Kernel (α × β) γ)
    [IsSFiniteKernel κ] [IsMarkovKernel η] (x : α) : (κ ⊗ₖ η) x (Prod.fst ⁻¹' s) = κ x s := by
  classical
  simp_rw [compProd_apply (measurable_fst hs), ← Set.preimage_comp, Prod.fst_comp_mk, Set.preimage,
    Function.const_apply]
  have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b :=
    by
    intro b
    by_cases hb : b ∈ s <;> simp [hb]
  simp_rw [this]
  rw [lintegral_indicator_const hs, one_mul]

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