(L : List (SignedHop ι sym)) (hsym : ∀ β, 1 ≤ sym β) : ∃ cst : ℝ, 0 ≤ cst ∧ ∀ x : maxDom sym, |commForm (listH L) (diagMax sym) x| ≤ cst * quadForm (diagMax sym) x

Initializing...

(L : List (SignedHop ι sym)) (hsym : ∀ β, 1 ≤ sym β) : ∃ cst : ℝ, 0 ≤ cst ∧ ∀ x : maxDom sym, |commForm (listH L) (diagMax sym) x| ≤ cst * quadForm (diagMax sym) x · Prove2Me