(d : ℕ) (p q : Fin d → ℕ → ℝ) (hunb : ∀ C : ℝ, ∃ k, C < |(∑ i, p i k ^ 2) + (∑ i, q i k ^ 2) + 1|) : ¬ ∃ C : ℝ, ∀ f : lpFiniteModes ℕ, ‖(diagComparisonData d p q).comparison f‖ ≤ C * ‖f‖

Initializing...

(d : ℕ) (p q : Fin d → ℕ → ℝ) (hunb : ∀ C : ℝ, ∃ k, C < |(∑ i, p i k ^ 2) + (∑ i, q i k ^ 2) + 1|) : ¬ ∃ C : ℝ, ∀ f : lpFiniteModes ℕ, ‖(diagComparisonData d p q).comparison f‖ ≤ C * ‖f‖ · Prove2Me