`BookProof.NavierStokesFlow.Carleman.tridiagOp_not_bounded` (c : ℕ → ℂ) (hc : ∀ C : ℝ, ∃ n, C < ‖c n‖) : ¬ ∃ C : ℝ, ∀ f : lpFiniteModes ℕ, ‖tridiagOp c f‖ ≤ C * ‖f‖

Initializing...

`BookProof.NavierStokesFlow.Carleman.tridiagOp_not_bounded` (c : ℕ → ℂ) (hc : ∀ C : ℝ, ∃ n, C < ‖c n‖) : ¬ ∃ C : ℝ, ∀ f : lpFiniteModes ℕ, ‖tridiagOp c f‖ ≤ C * ‖f‖ · Prove2Me