Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

Indexing Newton sums

Finite indexing and coefficient identities for the Newton-sum recurrence associated with Carlitz (1969).

theorem KloostermanWeil.Carlitz.prod_heq_of_heq {α α' β β' : Type} {a : α} {a' : α'} {b : β} {b' : β'} (ha : a ≍ a') (hb : b ≍ b') : (a, b) ≍ (a', b')

theorem KloostermanWeil.Carlitz.nested_sigma_heq {α : Type} {γ : α → Type} {δ : (a : α) → γ a → Type} {a a' : α} (ha : a = a') {q : γ a} {q' : γ a'} (hq : q ≍ q') {k : δ a q} {k' : δ a' q'} (hk : k ≍ k') : ⟨q, k⟩ ≍ ⟨q', k'⟩

@[instance_reducible]

noncomputable instance KloostermanWeil.Carlitz.factorDataFintype (p n : ℕ) [Fact (Nat.Prime p)] : Fintype (FactorData p n)

Equations

• KloostermanWeil.Carlitz.factorDataFintype p n = Fintype.ofEquiv (Fin n → ZMod p) (KloostermanWeil.Carlitz.coeffFactorEquiv p n)

@[instance_reducible]

noncomputable instance KloostermanWeil.Carlitz.relevantIrredFintype (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] : Fintype (RelevantIrred p n)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev KloostermanWeil.Carlitz.PointedFactorData (p n : ℕ) [Fact (Nat.Prime p)] : Type

Factor data with a chosen irreducible factor and one occurrence of that factor.

Equations

• KloostermanWeil.Carlitz.PointedFactorData p n = ((s : KloostermanWeil.Carlitz.FactorData p n) × (q : ↥(↑s).toFinset) × Fin (Multiset.count ↑q ↑s))

@[reducible, inline]

abbrev KloostermanWeil.Carlitz.PrimePowerDecomp (p n : ℕ) [Fact (Nat.Prime p)] : Type

An irreducible prime-power contribution together with complementary factor data.

Equations

• KloostermanWeil.Carlitz.PrimePowerDecomp p n = ((j : Fin n) × KloostermanWeil.Carlitz.RelevantIrred p (↑j + 1) × KloostermanWeil.Carlitz.FactorData p (n - (↑j + 1)))

noncomputable def KloostermanWeil.Carlitz.primePowerToPointed (p n : ℕ) [Fact (Nat.Prime p)] : PrimePowerDecomp p n → PointedFactorData p n

Insert the indicated irreducible power and mark its final occurrence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KloostermanWeil.Carlitz.pointedToPrimePower (p n : ℕ) [Fact (Nat.Prime p)] : PointedFactorData p n → PrimePowerDecomp p n

Remove the irreducible power ending at the marked occurrence.

Equations

• One or more equations did not get rendered due to their size.

theorem KloostermanWeil.Carlitz.pointed_primePower_left (p n : ℕ) [Fact (Nat.Prime p)] (z : PrimePowerDecomp p n) : pointedToPrimePower p n (primePowerToPointed p n z) = z

theorem KloostermanWeil.Carlitz.primePower_pointed_left (p n : ℕ) [Fact (Nat.Prime p)] (z : PointedFactorData p n) : primePowerToPointed p n (pointedToPrimePower p n z) = z

noncomputable def KloostermanWeil.Carlitz.primePowerPointedEquiv (p n : ℕ) [Fact (Nat.Prime p)] : PrimePowerDecomp p n ≃ PointedFactorData p n

Reindex prime-power contributions as factor multisets with a marked occurrence.

Equations

• One or more equations did not get rendered due to their size.