instIsSFiniteKernelProdParallelComp

English

For s ⊆ β and t ⊆ γ, the product kernel applied to a equals the product of the marginals on s and t.

Русский

Для s ⊆ β и t ⊆ γ применение произведения ядра к a равно произведению масс на s и t.

LaTeX

$$$$ (κ ×ₖ η) a (s ×ˢ t) = (κ a s) \\cdot (η a t). $$$$

Lean4

instance : IsSFiniteKernel (κ ∥ₖ η) := by
  by_cases h : IsSFiniteKernel κ
  swap
  · simp only [h, not_false_eq_true, parallelComp_of_not_isSFiniteKernel_left]
    infer_instance
  by_cases h : IsSFiniteKernel η
  swap
  · simp only [h, not_false_eq_true, parallelComp_of_not_isSFiniteKernel_right]
    infer_instance
  simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, parallelComp_sum_left, parallelComp_sum_right]
  infer_instance

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