Scalar Vec Mul mul l2Norm Sq le

theorem scalarVecMul_mul_l2NormSq_le {cols : ℕ} (c d : Rq Φ) (v : PolyVec (Rq Φ) cols)    {κ βSq : ℕ} (hd : Rq.l1Norm Φ d ≤ κ)    (hv : vecL2NormSq Φ (scalarVecMul c v) ≤ βSq) :    vecL2NormSq Φ (scalarVecMul (c * d) v) ≤ scalarVecMulMulL2NormSqBound κ βSq := by  unfold vecL2NormSq scalarVecMulMulL2NormSqBound  have hcomm : ∀ i, scalarVecMul (c * d) v i = d * scalarVecMul c v i := by    intro i; simp only [scalarVecMul_apply]; ring  calc ∑ i, Rq.l2NormSq Φ (scalarVecMul (c * d) v i)      = ∑ i, Rq.l2NormSq Φ (d * scalarVecMul c v i) := by simp_rw [hcomm]    _ ≤ ∑ i, (Rq.l1Norm Φ d) ^ 2 * Rq.l2NormSq Φ (scalarVecMul c v i) :=        Finset.sum_le_sum fun i _ => Rq.l2NormSq_mul_le (α := α) d (scalarVecMul c v i)    _ = (Rq.l1Norm Φ d) ^ 2 * ∑ i, Rq.l2NormSq Φ (scalarVecMul c v i) := by rw [← Finset.mul_sum]    _ ≤ κ ^ 2 * βSq := Nat.mul_le_mul (Nat.pow_le_pow_left hd 2) hv