Gadget Decompose zmod l2Norm Sq le

theorem gadgetDecompose_zmod_l2NormSq_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)    (hbq : b - 1 ≤ q / 2) (x : PolyVec (Rq Φ) rows)    (j : Fin (rows * digits)) :    ‖gadgetDecompose Φ (zmodDigitDecomposition b digits hb hq) x j‖₂² ≤      Φ.φ.natDegree * (b - 1) ^ 2 := by  unfold Rq.l2NormSq  calc ∑ k ∈ Finset.range Φ.φ.natDegree,        ((gadgetDecompose Φ (zmodDigitDecomposition b digits hb hq) x j).1.coeff k).valMinAbs.natAbs          ^ 2      ≤ ∑ _k ∈ Finset.range Φ.φ.natDegree, (b - 1) ^ 2 := by        refine Finset.sum_le_sum (fun k hk => ?_)        rw [gadgetDecompose_coeff Φ _ x j (Finset.mem_range.mp hk)]        exact Nat.pow_le_pow_left (zmodDigit_natAbs_le hb hq hbq _ _) 2    _ = Φ.φ.natDegree * (b - 1) ^ 2 := by        rw [Finset.sum_const, Finset.card_range, smul_eq_mul]