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

Formal generating-series algebra

Formal power-series and coefficient identities underlying the Carlitz (1969) generating method. The particular identities are derived in Lean.

noncomputable def KloostermanWeil.Carlitz.KSeries (K : ℕ → ℂ) : PowerSeries ℂ

The formal series with positive-degree coefficients K n / n and constant term zero.

Equations

• KloostermanWeil.Carlitz.KSeries K = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else K n / ↑n

noncomputable def KloostermanWeil.Carlitz.quadraticL (K1 q : ℂ) : PowerSeries ℂ

The quadratic formal series 1 + K1 * X + q * X².

Equations

• KloostermanWeil.Carlitz.quadraticL K1 q = 1 + PowerSeries.C K1 * PowerSeries.X + PowerSeries.C q * PowerSeries.X ^ 2

@[simp]

theorem KloostermanWeil.Carlitz.constantCoeff_quadraticL (K1 q : ℂ) : PowerSeries.constantCoeff (quadraticL K1 q) = 1

theorem KloostermanWeil.Carlitz.derivative_logOf_mul_self {f : PowerSeries ℂ} (hf : PowerSeries.constantCoeff f = 1) : PowerSeries.derivative f.logOf * f = PowerSeries.derivative f

@[simp]

theorem KloostermanWeil.Carlitz.coeff_KSeries_succ (K : ℕ → ℂ) (n : ℕ) : (PowerSeries.coeff (n + 1)) (KSeries K) = K (n + 1) / ↑(n + 1)

theorem KloostermanWeil.Carlitz.coeff_derivative_KSeries (K : ℕ → ℂ) (n : ℕ) : (PowerSeries.coeff n) (PowerSeries.derivative (KSeries K)) = K (n + 1)

theorem KloostermanWeil.Carlitz.coeff_quadraticL_of_three_le (K1 q : ℂ) {n : ℕ} (hn : 3 ≤ n) : (PowerSeries.coeff n) (quadraticL K1 q) = 0

theorem KloostermanWeil.Carlitz.coeff_mul_quadraticL (D : PowerSeries ℂ) (K1 q : ℂ) (r : ℕ) : (PowerSeries.coeff (r + 2)) (D * quadraticL K1 q) = (PowerSeries.coeff (r + 2)) D + K1 * (PowerSeries.coeff (r + 1)) D + q * (PowerSeries.coeff r) D

theorem KloostermanWeil.Carlitz.recurrence_shifted_of_generating_identity (K : ℕ → ℂ) (q : ℂ) (hgen : KSeries K = (quadraticL (K 1) q).logOf) (r : ℕ) : K (r + 3) + K 1 * K (r + 2) + q * K (r + 1) = 0

theorem KloostermanWeil.Carlitz.recurrence_of_generating_identity (K : ℕ → ℂ) (q : ℂ) (hgen : KSeries K = (quadraticL (K 1) q).logOf) (n : ℕ) : 1 ≤ n → K (n + 2) + K 1 * K (n + 1) + q * K n = 0

theorem KloostermanWeil.Carlitz.coeff_one_mul_quadraticL (D : PowerSeries ℂ) (K1 q : ℂ) : (PowerSeries.coeff 1) (D * quadraticL K1 q) = (PowerSeries.coeff 1) D + K1 * (PowerSeries.coeff 0) D

theorem KloostermanWeil.Carlitz.K_two_eq_of_generating_identity (K : ℕ → ℂ) (q : ℂ) (hgen : KSeries K = (quadraticL (K 1) q).logOf) : K 2 = 2 * q - K 1 ^ 2

noncomputable def KloostermanWeil.Carlitz.spectralPoly (K1 q : ℂ) : Polynomial ℂ

The quadratic polynomial whose two roots encode the extension-sum recurrence.

Equations

• KloostermanWeil.Carlitz.spectralPoly K1 q = Polynomial.X ^ 2 + (Polynomial.C K1 * Polynomial.X + Polynomial.C q)

theorem KloostermanWeil.Carlitz.spectralPoly_degree (K1 q : ℂ) : (spectralPoly K1 q).degree = 2

theorem KloostermanWeil.Carlitz.exists_spectral_roots_of_generating_identity (K : ℕ → ℂ) (q : ℂ) (hgen : KSeries K = (quadraticL (K 1) q).logOf) : ∃ (α : ℂ) (β : ℂ), α + β = -K 1 ∧ α * β = q ∧ ∀ (n : ℕ), 1 ≤ n → K n = -(α ^ n + β ^ n)