Hasse differentiation in Stepanov's construction

The divisibility, linear operator, and degree estimates below formalize Lemma 10 of Gergely Harcos, Weil's bound for Kloosterman sums, printed page 10 (harcos-weil.pdf).

The operator is polynomial division of hasseDeriv k (g * f ^ n) by f ^ (n - k). Its factorization is proved, not assumed. No monicity or characteristic restriction is needed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_pow_dvd_hasseDeriv_mul_pow {R : Type u_1} [CommRing R] (f g : Polynomial R) (n k : ℕ) : f ^ (n - k) ∣ (Polynomial.hasseDeriv k) (g * f ^ n)

The power forced by Leibniz's rule divides the Hasse derivative. The truncated exponent also makes the statement valid when n < k.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n k : ℕ) : Polynomial F →ₗ[F] Polynomial F

Harcos's g ↦ g⁽ᵏ⁾ as an actual linear map, for every nonzero f. It is defined for all k; the degree estimate below uses k ≤ n.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator f hf n k = { toFun := fun (g : Polynomial F) => (Polynomial.hasseDeriv k) (g * f ^ n) / f ^ (n - k), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator_apply {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n k : ℕ) (g : Polynomial F) : (stepanovHasseOperator f hf n k) g = (Polynomial.hasseDeriv k) (g * f ^ n) / f ^ (n - k)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator_spec {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n k : ℕ) (g : Polynomial F) : (Polynomial.hasseDeriv k) (g * f ^ n) = (stepanovHasseOperator f hf n k) g * f ^ (n - k)

The factorization in Harcos Lemma 10, including the endpoint k = n.

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator_zero {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n : ℕ) (g : Polynomial F) : (stepanovHasseOperator f hf n 0) g = g

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator_self {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n : ℕ) (g : Polynomial F) : (stepanovHasseOperator f hf n n) g = (Polynomial.hasseDeriv n) (g * f ^ n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator_natDegree_le {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n k : ℕ) (hkn : k ≤ n) (hm : 1 ≤ f.natDegree) (g : Polynomial F) : ((stepanovHasseOperator f hf n k) g).natDegree ≤ g.natDegree + k * (f.natDegree - 1)

The natural-degree form of Harcos's estimate; valid also for g = 0.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovHasseOperator_degree_lt {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) (n k B : ℕ) (hkn : k ≤ n) (hm : 1 ≤ f.natDegree) (g : Polynomial F) (hg : g.degree < ↑B) : ((stepanovHasseOperator f hf n k) g).degree < ↑(B + k * (f.natDegree - 1))

The strict degree bound used to size Stepanov's coefficient system. Unlike a natDegree < B hypothesis, degree < B handles g = 0, even when B = 0.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_hasse_vanishing_iff_pow_dvd {R : Type u_2} [CommRing R] (h : Polynomial R) (x : R) (ell : ℕ) : (∀ k < ell, Polynomial.eval x ((Polynomial.hasseDeriv k) h) = 0) ↔ (Polynomial.X - Polynomial.C x) ^ ell ∣ h

Harcos Lemma 8: vanishing of the first Hasse derivatives is exactly divisibility by the corresponding power of the linear factor.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_sum_rootMultiplicity_le {F : Type u_1} [Field F] (h : Polynomial F) (s : Finset F) : ∑ x ∈ s, Polynomial.rootMultiplicity x h ≤ h.natDegree

The sum of root multiplicities over any finite set is at most the degree.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_sum_hasse_orders_le {F : Type u_1} [Field F] (h : Polynomial F) (hh : h ≠ 0) (s : Finset F) (orders : F → ℕ) (hv : ∀ x ∈ s, ∀ k < orders x, Polynomial.eval x ((Polynomial.hasseDeriv k) h) = 0) : ∑ x ∈ s, orders x ≤ h.natDegree

Finite-root degree bound with a possibly different vanishing order at each point. The nonzero hypothesis is essential here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_card_mul_hasse_order_le {F : Type u_1} [Field F] (h : Polynomial F) (hh : h ≠ 0) (s : Finset F) (ell : ℕ) (hv : ∀ x ∈ s, ∀ k < ell, Polynomial.eval x ((Polynomial.hasseDeriv k) h) = 0) : s.card * ell ≤ h.natDegree

If a nonzero polynomial vanishes to Hasse order at least ell at every point of a finite set, then ell times the number of points is at most its degree.