Gadget Mul zmod coeff nat Abs le

theorem gadgetMul_zmod_coeff_natAbs_le {b rows digits : ℕ} (hd : 0 < digits)    (h1 : 1 ≤ Φ.φ.natDegree) {γ : ℕ} (v : PolyVec (Rq Φ) (rows * digits))    (hv : vecLInftyNorm Φ v ≤ γ) (i : Fin rows) {k : ℕ} (hk : k < Φ.φ.natDegree) :    ((gadgetMul Φ (b : ZMod q) v i).1.coeff k).valMinAbs.natAbs      ≤ (∑ u ∈ Finset.range digits, b ^ u) * γ := by  -- the coefficient of the gadget product is the digit-weighted sum of block coefficients  have hcoeff : (gadgetMul Φ (b : ZMod q) v i).1.coeff k      = ∑ e : Fin digits, (b : ZMod q) ^ (e : ℕ) * (v (finProdFinEquiv (i, e))).1.coeff k := by    rw [gadgetMul_apply Φ (b : ZMod q) hd v i, ← Rq.coeffHom_apply Φ k, map_sum]    simp only [Rq.coeffHom_apply]    exact Finset.sum_congr rfl fun e _ => Rq.constRq_mul_coeff Φ h1 _ _ k  -- the explicit integer representative of that coefficient  have hrep : ((∑ e : Fin digits,        (b : ℤ) ^ (e : ℕ) * ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs : ℤ) : ZMod q)      = (gadgetMul Φ (b : ZMod q) v i).1.coeff k := by    rw [hcoeff, Int.cast_sum]    refine Finset.sum_congr rfl fun e _ => ?_    rw [Int.cast_mul, Int.cast_pow, Int.cast_natCast, ZMod.coe_valMinAbs]  -- entrywise range bound from the ℓ∞ hypothesis  have hentry : ∀ e : Fin digits,      ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs.natAbs ≤ γ := fun e =>    calc ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs.natAbs        ≤ Rq.lInftyNorm Φ (v (finProdFinEquiv (i, e))) :=          Finset.le_sup (f := fun k => ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs.natAbs)            (Finset.mem_range.mpr hk)      _ ≤ vecLInftyNorm Φ v :=          Finset.le_sup (f := fun j => Rq.lInftyNorm Φ (v j)) (Finset.mem_univ _)      _ ≤ γ := hv  -- minimality of the centered representative + triangle over the integer representative  calc ((gadgetMul Φ (b : ZMod q) v i).1.coeff k).valMinAbs.natAbs      ≤ (∑ e : Fin digits,          (b : ℤ) ^ (e : ℕ) * ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs).natAbs :=        valMinAbs_natAbs_le _ hrep    _ ≤ ∑ e : Fin digits,          ((b : ℤ) ^ (e : ℕ) * ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs).natAbs :=        Int.natAbs_sum_le _ _    _ = ∑ e : Fin digits,          b ^ (e : ℕ) * ((v (finProdFinEquiv (i, e))).1.coeff k).valMinAbs.natAbs := by        refine Finset.sum_congr rfl fun e _ => ?_        rw [Int.natAbs_mul, Int.natAbs_pow, Int.natAbs_natCast]    _ ≤ ∑ e : Fin digits, b ^ (e : ℕ) * γ :=        Finset.sum_le_sum fun e _ => Nat.mul_le_mul_left _ (hentry e)    _ = (∑ u ∈ Finset.range digits, b ^ u) * γ := by        rw [← Finset.sum_mul, Fin.sum_univ_eq_sum_range (fun u => b ^ u) digits]