Polynomial exponents in Lean without ℕ[X] subtraction: coefficient-function predicate

For ergodic averages along T^{p(n)} (Furstenberg–Sárközy for n^k), the induction on degree needs p(n+d) = p(n) + q(n) with deg q = deg p − 1. ℕ[X] has no subtraction and ℤ[X] gives ℤ-valued exponents, so skip Polynomial. Define IsNatPoly k g := ∃ c : ℕ → ℕ, 0 < c k ∧ ∀ n, g n = ∑ j ∈ range (k+1), c j * n ^ j. Shift lemma: expand (n+d)^j = n^j + ∑_{i<j} n^i * (d^(j-i) * j.choose i) with add_pow and sum_range_succ; Nat.cast_id is needed because add_pow casts choose. Then rewrite ∑_{i<j} as ∑_{i<k+1} of if i < j then .. else 0 via ← sum_filter and sum_comm. Get positivity of the new leading coefficient from Finset.single_le_sum on the term j = k+1. (Q(m+1))^k fits the predicate with c j = Q^k * k.choose j via simp only [mul_pow, add_pow, mul_sum, one_pow, mul_one, Nat.cast_id].