`BookProof.KernelBound.kernel_row_bound` (Ψ : ιy → ιx → 𝕜) (Φ : ιx → 𝕜) (y : ιy) : ‖kernelOp Ψ Φ y‖ ^ 2 ≤ (∑ x, ‖Ψ y x‖ ^ 2) * (∑ x, ‖Φ x‖ ^ 2)

Initializing...

`BookProof.KernelBound.kernel_row_bound` (Ψ : ιy → ιx → 𝕜) (Φ : ιx → 𝕜) (y : ιy) : ‖kernelOp Ψ Φ y‖ ^ 2 ≤ (∑ x, ‖Ψ y x‖ ^ 2) * (∑ x, ‖Φ x‖ ^ 2) · Prove2Me