Gadget Mul zmod vec L2Norm Sq le

theorem gadgetMul_zmod_vecL2NormSq_le {b rows digits : ℕ} (hd : 0 < digits)    (h1 : 1 ≤ Φ.φ.natDegree) {γ : ℕ} (v : PolyVec (Rq Φ) (rows * digits))    (hv : vecLInftyNorm Φ v ≤ γ) :    ‖gadgetMul Φ (b : ZMod q) v‖₂²      ≤ zRecomposeL2SqBound γ b digits Φ.φ.natDegree rows := by  calc vecL2NormSq Φ (gadgetMul Φ (b : ZMod q) v)      ≤ rows * (Φ.φ.natDegree * (vecLInftyNorm Φ (gadgetMul Φ (b : ZMod q) v)) ^ 2) :=        vecL2NormSq_le_card_mul_lInftyNorm_sq Φ _    _ ≤ rows * (Φ.φ.natDegree * ((∑ u ∈ Finset.range digits, b ^ u) * γ) ^ 2) :=        Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left          (gadgetMul_zmod_vecLInftyNorm_le Φ hd h1 v hv) 2))    _ = zRecomposeL2SqBound γ b digits Φ.φ.natDegree rows := rfl