Rq l2Norm Sq mul le

theorem Rq.l2NormSq_mul_le (d w : Rq Φ) :    Rq.l2NormSq Φ (d * w) ≤ (Rq.l1Norm Φ d) ^ 2 * Rq.l2NormSq Φ w := by  have hAzero : ∀ i, 2 ^ α ≤ i → (d.1.coeff i).valMinAbs = 0 := by    intro i hi    have hc : d.1.coeff i = 0 := by      rw [CompPoly.CPolynomial.coeff_toPoly]      refine Polynomial.coeff_eq_zero_of_degree_lt        (lt_of_lt_of_le ((Φ).degree_toPoly_lt_of_reduced d.2) ?_)      rw [hachi_degree, hachi_natDegree]; exact_mod_cast hi    rw [hc, ZMod.valMinAbs_zero]  have hBzero : ∀ j, 2 ^ α ≤ j → (w.1.coeff j).valMinAbs = 0 := by    intro j hj    have hc : w.1.coeff j = 0 := by      rw [CompPoly.CPolynomial.coeff_toPoly]      refine Polynomial.coeff_eq_zero_of_degree_lt        (lt_of_lt_of_le ((Φ).degree_toPoly_lt_of_reduced w.2) ?_)      rw [hachi_degree, hachi_natDegree]; exact_mod_cast hj    rw [hc, ZMod.valMinAbs_zero]  have hc : ∀ k ∈ Finset.range (2 ^ α),      (((d * w).1.coeff k).valMinAbs.natAbs : ℤ)        ≤ ∑ i ∈ Finset.range (2 ^ α),            ((d.1.coeff i).valMinAbs.natAbs : ℤ)              * ((w.1.coeff ((k + 2 ^ α - i) % (2 ^ α))).valMinAbs.natAbs : ℤ) := by    intro k hk    have hkn : k < 2 ^ α := Finset.mem_range.mp hk    have hnat : ((d * w).1.coeff k).valMinAbs.natAbs        ≤ ∑ i ∈ Finset.range (2 ^ α),            ((d.1.coeff i).valMinAbs).natAbs              * ((w.1.coeff ((k + 2 ^ α - i) % (2 ^ α))).valMinAbs).natAbs := by      refine le_trans (valMinAbs_natAbs_le          ((∑ p ∈ Finset.antidiagonal k, (d.1.coeff p.1).valMinAbs * (w.1.coeff p.2).valMinAbs)            - ∑ p ∈ Finset.antidiagonal (2 ^ α + k),                (d.1.coeff p.1).valMinAbs * (w.1.coeff p.2).valMinAbs) ?_)        (natAbs_conv_le (by positivity) k hkn          (fun i => (d.1.coeff i).valMinAbs) (fun j => (w.1.coeff j).valMinAbs) hAzero hBzero)      rw [Int.cast_sub, cast_conv (α := α) d w k, cast_conv (α := α) d w (2 ^ α + k),          ← coeff_mul_rq_two_block (α := α) d w hkn]    exact_mod_cast hnat  have key := sum_conv_sq_le (n := 2 ^ α)      (fun i => ((d.1.coeff i).valMinAbs.natAbs : ℤ))      (fun j => ((w.1.coeff j).valMinAbs.natAbs : ℤ))      (fun k => (((d * w).1.coeff k).valMinAbs.natAbs : ℤ))      (fun i => by positivity) (fun j => by positivity) (fun k => by positivity) hc  have e1 : (Rq.l2NormSq Φ (d * w) : ℤ)      = ∑ k ∈ Finset.range (2 ^ α), (((d * w).1.coeff k).valMinAbs.natAbs : ℤ) ^ 2 := by    simp only [Rq.l2NormSq]; rw [hachi_natDegree]; push_cast; rfl  have e2 : (Rq.l1Norm Φ d : ℤ)      = ∑ i ∈ Finset.range (2 ^ α), ((d.1.coeff i).valMinAbs.natAbs : ℤ) := by    simp only [Rq.l1Norm]; rw [hachi_natDegree]; push_cast; rfl  have e3 : (Rq.l2NormSq Φ w : ℤ)      = ∑ j ∈ Finset.range (2 ^ α), ((w.1.coeff j).valMinAbs.natAbs : ℤ) ^ 2 := by    simp only [Rq.l2NormSq]; rw [hachi_natDegree]; push_cast; rfl  have hgoal : (Rq.l2NormSq Φ (d * w) : ℤ) ≤ ((Rq.l1Norm Φ d : ℤ)) ^ 2 * (Rq.l2NormSq Φ w : ℤ) := by    rw [e1, e2, e3]; exact key  exact_mod_cast hgoal