Harcos's extension-field character sums

The coefficients belong to the fixed prime field, not to a varying extension. The trace is Algebra.trace; its Frobenius formula and additive-character orthogonality identify the sum over frequencies with the actual affine count.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] (a b m : ZMod p) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman p F a b m = ∑ t : Fˣ, ZMod.stdAddChar (m * (Algebra.trace (ZMod p) F) ((algebraMap (ZMod p) F) a * ↑t + (algebraMap (ZMod p) F) b * (↑t)⁻¹))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_eq_frobenius_sum (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (x : F) : (algebraMap (ZMod p) F) ((Algebra.trace (ZMod p) F) x) = ∑ i ∈ Finset.range (Module.finrank (ZMod p) F), x ^ p ^ i

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_eq_frobenius_sum_of_card (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (n : ℕ) (hcard : Fintype.card F = p ^ n) (x : F) : (algebraMap (ZMod p) F) ((Algebra.trace (ZMod p) F) x) = ∑ i ∈ Finset.range n, x ^ p ^ i

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_zero (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] (a b : ZMod p) : harcosTraceKloosterman p F a b 0 = ↑(Fintype.card Fˣ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_frequency_sum (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] (a b : ZMod p) : ∑ m : ZMod p, harcosTraceKloosterman p F a b m = ↑p * ↑{t : Fˣ | (Algebra.trace (ZMod p) F) ((algebraMap (ZMod p) F) a * ↑t + (algebraMap (ZMod p) F) b * (↑t)⁻¹) = 0}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_sum_eq_curve (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] [CharP F p] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : ∑ m : ZMod p, harcosTraceKloosterman p F a b m = ↑(harcosCurvePointCount p ((algebraMap (ZMod p) F) a) ((algebraMap (ZMod p) F) b))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_nonzero_sum_eq_curve (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] [CharP F p] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) : ∑ m ∈ Finset.univ.erase 0, harcosTraceKloosterman p F a b m = ↑(harcosCurvePointCount p ((algebraMap (ZMod p) F) a) ((algebraMap (ZMod p) F) b)) - ↑(Fintype.card F) + 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_algEquiv (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] (G : Type u_2) [Field G] [Fintype G] [DecidableEq G] [Algebra (ZMod p) G] (e : F ≃ₐ[ZMod p] G) (a b m : ZMod p) : harcosTraceKloosterman p F a b m = harcosTraceKloosterman p G a b m

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_primeField (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) : harcosTraceKloosterman p (ZMod p) a b m = completeKloosterman p (m * a) ↑(m * b).val

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_nonzero_sum_bound (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod p) F] [CharP F p] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) (n : ℕ) (hcard : Fintype.card F = p ^ n) (hn : 4 ≤ n) : ‖∑ m ∈ Finset.univ.erase 0, harcosTraceKloosterman p F a b m‖ ≤ 8 * ↑p * ↑⌈√(↑p ^ n)⌉₊ + 1

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) (n : ℕ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman p a b m n = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman p (GaloisField p n) a b m

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_one (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) : harcosExtensionKloosterman p a b m 1 = completeKloosterman p (m * a) ↑(m * b).val

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_nonzero_sum_bound (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) (n : ℕ) (hn : 4 ≤ n) : ‖∑ m ∈ Finset.univ.erase 0, harcosExtensionKloosterman p a b m n‖ ≤ 8 * ↑p * ↑⌈√(↑p ^ n)⌉₊ + 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_total_growth (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (a b : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) (n : ℕ) (hn : 4 ≤ n) : ‖∑ m ∈ Finset.univ.erase 0, harcosExtensionKloosterman p a b m n‖ ≤ (16 * ↑p + 1) * √↑p ^ n

A single constant for all extension degrees. This bounds the sum over nonzero frequencies, not any individual Kloosterman sum.