compProd_congr — Mathlib

English

For S-finite kernels κ, η, κ ⊗ₖ η = 0 if and only if for all a, η(a, b) is zero almost surely in b with respect to κ a.

Русский

Для S- конечных ядер κ, η, κ ⊗ₖ η = 0 тогда и только тогда, когда для каждого a верно, что η(a,b) = 0 почти surely по b относительно κ a.

LaTeX

$$$$ κ ⊗ₖ η = 0 \quad \Leftrightarrow \quad \forall a, η(a, b) = 0 \text{ a.e. in } b \text{ w.r.t. } κ a,$$$$

Lean4

theorem compProd_congr {κ : Kernel α β} {η η' : Kernel (α × β) γ} [IsSFiniteKernel η] [IsSFiniteKernel η']
    (h : ∀ a, ∀ᵐ b ∂(κ a), η (a, b) = η' (a, b)) : κ ⊗ₖ η = κ ⊗ₖ η' :=
  by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp_rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
  ext a s hs
  rw [compProd_apply hs, compProd_apply hs]
  refine lintegral_congr_ae ?_
  filter_upwards [h a] with b hb using by rw [hb]

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