`BookProof.KernelBound.kernel_hs_sq_bound` (Ψ : ιy → ιx → 𝕜) (Φ : ιx → 𝕜) : ∑ y, ‖kernelOp Ψ Φ y‖ ^ 2 ≤ (∑ y, ∑ x, ‖Ψ y x‖ ^ 2) * (∑ x, ‖Φ x‖ ^ 2)
ProvedBookProof.KernelBound.kernel_hs_sq_boundtheoremstimepiece
Prove the following Lean 4 theorem from ChapterKernelBound.
BookProof.KernelBound.kernel_hs_sq_bound (Ψ : ιy → ιx → 𝕜) (Φ : ιx → 𝕜) : ∑ y, ‖kernelOp Ψ Φ y‖ ^ 2 ≤ (∑ y, ∑ x, ‖Ψ y x‖ ^ 2) * (∑ x, ‖Φ x‖ ^ 2)
Formalization note: Lean 4 identifier BookProof.KernelBound.kernel_hs_sq_bound.
Preamble
-- Generated from ChapterKernelBound.lean — theorem BookProof.KernelBound.kernel_hs_sq_bound
import Mathlib
import Definitions.Def_ChapterKernelBound
open BookProof.KernelBound
open Finset
variable {𝕜 : Type*} [RCLike 𝕜]
variable {ιx ιy : Type*} [Fintype ιx] [Fintype ιy]Formal statement
theorem BookProof.KernelBound.kernel_hs_sq_bound (Ψ : ιy → ιx → 𝕜) (Φ : ιx → 𝕜) :
∑ y, ‖kernelOp Ψ Φ y‖ ^ 2
≤ (∑ y, ∑ x, ‖Ψ y x‖ ^ 2) * (∑ x, ‖Φ x‖ ^ 2) := by sorry