instIsFiniteKernelProdParallelComp

English

If κ and η are s-finite, then κ ∥ₖ η is s-finite.

Русский

Если κ и η s-конечные, то κ ∥ₖ η також s-конечное.

LaTeX

$$$$[\\text{IsSFiniteKernel } κ] \\; [\\text{IsSFiniteKernel } η] \\Rightarrow [\\text{IsSFiniteKernel } (κ \\parallelₖ η)].$$$$

Lean4

instance [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ ∥ₖ η) :=
  by
  refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩
  calc
    (κ ∥ₖ η) a Set.univ
    _ = κ a.1 Set.univ * η a.2 Set.univ := parallelComp_apply_univ
    _ ≤ κ.bound * η.bound := by
      gcongr
      · exact measure_le_bound κ a.1 Set.univ
      · exact measure_le_bound η a.2 Set.univ

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