Documentation

LeanPool.KloostermanWeil.Weil.ChineseRemainderAndCompletion

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

CRT factorization and Fourier completion #

Exact Bézout/CRT factorization, reduced-modulus bounds, sharp centered Fourier completion and weighted partial summation. The underlying techniques are standard; see Iwaniec–Kowalski (2004), Ch. 12 §12.2, for completion methods. The declared hypotheses govern each estimate.

theorem KloostermanWeil.kloostermanSumPrime_le_two_sqrt_of_not_both_zero (hWeil : PrimeNondegenerateWeil) (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) (hnot : a ≠ 0 ∨ b ≠ 0) :

‖kloostermanSumPrime p a b‖ ≤ 2 * √↑p

CRT region: exact unit-sum splitting via the chosen Bézout coefficients; standard CRT, locally proved. No additional analytic hypothesis is hidden here.

def KloostermanWeil.crtLeftCoeff (m n : ℕ) :

The Bezout coefficient of n in the identity for the coprime pair m, n.

Equations

KloostermanWeil.crtLeftCoeff m n = n.gcdA m

Instances For

def KloostermanWeil.crtRightCoeff (m n : ℕ) :

The Bezout coefficient of m in the identity for the coprime pair m, n.

Equations

KloostermanWeil.crtRightCoeff m n = n.gcdB m

Instances For

theorem KloostermanWeil.crt_bezout {m n : ℕ} (hcop : m.Coprime n) :

↑n * crtLeftCoeff m n + ↑m * crtRightCoeff m n = 1

theorem KloostermanWeil.stdAddChar_mul_eq_crt {m n : ℕ} [NeZero m] [NeZero n] [NeZero (m * n)] (hcop : m.Coprime n) (t : ℤ) :

ZMod.stdAddChar ↑(crtLeftCoeff m n * t) * ZMod.stdAddChar ↑(crtRightCoeff m n * t) = ZMod.stdAddChar ↑t

noncomputable def KloostermanWeil.kloostermanUnitSum (N : ℕ) [NeZero N] (a b : ZMod N) :

The standard additive character of b*x + a/x, summed over residue-class units.

Equations

KloostermanWeil.kloostermanUnitSum N a b = ∑ x : (ZMod N)ˣ, ZMod.stdAddChar (b * ↑x + a * ↑x⁻¹)

Instances For

theorem KloostermanWeil.stdAddChar_mul_eq_crt_zmod {m n : ℕ} [NeZero m] [NeZero n] [NeZero (m * n)] (hcop : m.Coprime n) (z : ZMod (m * n)) :

ZMod.stdAddChar (↑(crtLeftCoeff m n) * ((ZMod.chineseRemainder hcop) z).1) * ZMod.stdAddChar (↑(crtRightCoeff m n) * ((ZMod.chineseRemainder hcop) z).2) = ZMod.stdAddChar z

noncomputable def KloostermanWeil.crtUnitsEquiv {m n : ℕ} (hcop : m.Coprime n) :

(ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ

The Chinese remainder equivalence on unit groups of coprime residue rings.

Equations

KloostermanWeil.crtUnitsEquiv hcop = (Units.mapEquiv (ZMod.chineseRemainder hcop).toMulEquiv).trans MulEquiv.prodUnits

Instances For

theorem KloostermanWeil.kloostermanUnitSum_crt {m n : ℕ} [NeZero m] [NeZero n] [NeZero (m * n)] (hcop : m.Coprime n) (a b : ZMod (m * n)) :

kloostermanUnitSum (m * n) a b = kloostermanUnitSum m (↑(crtLeftCoeff m n) * ((ZMod.chineseRemainder hcop) a).1) (↑(crtLeftCoeff m n) * ((ZMod.chineseRemainder hcop) b).1) * kloostermanUnitSum n (↑(crtRightCoeff m n) * ((ZMod.chineseRemainder hcop) a).2) (↑(crtRightCoeff m n) * ((ZMod.chineseRemainder hcop) b).2)

theorem KloostermanWeil.kloostermanUnitSum_prime_eq (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) :

kloostermanUnitSum p a b = kloostermanSumPrime p a b

theorem KloostermanWeil.norm_kloostermanUnitSum_crt {m n : ℕ} [NeZero m] [NeZero n] [NeZero (m * n)] (hcop : m.Coprime n) (a b : ZMod (m * n)) :

‖kloostermanUnitSum (m * n) a b‖ = ‖kloostermanUnitSum m (↑(crtLeftCoeff m n) * ((ZMod.chineseRemainder hcop) a).1) (↑(crtLeftCoeff m n) * ((ZMod.chineseRemainder hcop) b).1)‖ * ‖kloostermanUnitSum n (↑(crtRightCoeff m n) * ((ZMod.chineseRemainder hcop) a).2) (↑(crtRightCoeff m n) * ((ZMod.chineseRemainder hcop) b).2)‖

theorem KloostermanWeil.kloostermanUnitSum_prime_le_two_sqrt_of_not_both_zero (hWeil : PrimeNondegenerateWeil) (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) (hnot : a ≠ 0 ∨ b ≠ 0) :

‖kloostermanUnitSum p a b‖ ≤ 2 * √↑p

theorem KloostermanWeil.crtLeftCoeff_isUnit {m n : ℕ} [NeZero m] (hcop : m.Coprime n) :

IsUnit ↑(crtLeftCoeff m n)

theorem KloostermanWeil.crtRightCoeff_isUnit {m n : ℕ} [NeZero n] (hcop : m.Coprime n) :

IsUnit ↑(crtRightCoeff m n)

theorem KloostermanWeil.crt_local_left_isUnit {m n : ℕ} [NeZero m] (hcop : m.Coprime n) {a : ZMod (m * n)} (ha : IsUnit a) :

IsUnit (↑(crtLeftCoeff m n) * ((ZMod.chineseRemainder hcop) a).1)

theorem KloostermanWeil.crt_local_right_isUnit {m n : ℕ} [NeZero n] (hcop : m.Coprime n) {a : ZMod (m * n)} (ha : IsUnit a) :

IsUnit (↑(crtRightCoeff m n) * ((ZMod.chineseRemainder hcop) a).2)

theorem KloostermanWeil.kloostermanUnitSum_prod_primes_le (hWeil : PrimeNondegenerateWeil) (s : Finset ℕ) (Q : ℕ) :

Q = ∏ p ∈ s, p → ∀ (hQ0 : Q ≠ 0), (∀ p ∈ s, Nat.Prime p) → ∀ (a b : ZMod Q), IsUnit a → ‖kloostermanUnitSum Q a b‖ ≤ 2 ^ s.card * √↑Q

theorem KloostermanWeil.kloostermanUnitSum_squarefree_unit_le (hWeil : PrimeNondegenerateWeil) {q : ℕ} [NeZero q] (hsq : Squarefree q) (a b : ZMod q) (ha : IsUnit a) :

‖kloostermanUnitSum q a b‖ ≤ 2 ^ q.primeFactors.card * √↑q

Reduction region: bound for a source-defined reduced modulus/sum. No theorem here identifies that reduced sum with a full-modulus sum.

def KloostermanWeil.reducedDivisor (A q : ℕ) :

The common divisor removed from the numerator and modulus.

Equations

KloostermanWeil.reducedDivisor A q = A.gcd q

Instances For

def KloostermanWeil.reducedModulus (A q : ℕ) :

The modulus after division by gcd(A, q).

Equations

KloostermanWeil.reducedModulus A q = q / KloostermanWeil.reducedDivisor A q

Instances For

def KloostermanWeil.reducedNumerator (A q : ℕ) :

The numerator after division by gcd(A, q).

Equations

KloostermanWeil.reducedNumerator A q = A / KloostermanWeil.reducedDivisor A q

Instances For

theorem KloostermanWeil.reducedNumerator_coprime_reducedModulus {A q : ℕ} (hq : 0 < q) :

(reducedNumerator A q).Coprime (reducedModulus A q)

theorem KloostermanWeil.reducedModulus_dvd {A q : ℕ} :

reducedModulus A q ∣ q

theorem KloostermanWeil.reducedModulus_pos {A q : ℕ} (hq : 0 < q) :

0 < reducedModulus A q

theorem KloostermanWeil.reducedModulus_squarefree {A q : ℕ} (hsq : Squarefree q) :

Squarefree (reducedModulus A q)

theorem KloostermanWeil.reducedNumerator_isUnit {A q : ℕ} (hq : 0 < q) :

IsUnit ↑(reducedNumerator A q)

theorem KloostermanWeil.kloostermanUnitSum_reduced_le (hWeil : PrimeNondegenerateWeil) {A q : ℕ} (hq : 0 < q) (hsq : Squarefree q) (b : ZMod (reducedModulus A q)) :

‖kloostermanUnitSum (reducedModulus A q) (↑(reducedNumerator A q)) b‖ ≤ 2 ^ (reducedModulus A q).primeFactors.card * √↑(reducedModulus A q)

Completion region: character orthogonality, full finite DFT and sharp interval Fourier completion; method context [IwaniecKowalski2004].

def KloostermanWeil.zmodFrequencyDistance {N : ℕ} (h : ZMod N) :

The smaller distance of a residue's representative to zero or to the modulus.

Equations

KloostermanWeil.zmodFrequencyDistance h = min h.val (N - h.val)

Instances For

theorem KloostermanWeil.zmodFrequencyDistance_pos {N : ℕ} [NeZero N] {h : ZMod N} (hh : h ≠ 0) :

0 < zmodFrequencyDistance h

theorem KloostermanWeil.two_mul_zmodFrequencyDistance_le {N : ℕ} [NeZero N] (h : ZMod N) :

2 * zmodFrequencyDistance h ≤ N

theorem KloostermanWeil.stdAddChar_chord_lower {N : ℕ} [NeZero N] {h : ZMod N} (hh : h ≠ 0) :

4 * ↑(zmodFrequencyDistance h) / ↑N ≤ ‖ZMod.stdAddChar h - 1‖

noncomputable def KloostermanWeil.unitsEquivIsUnitSubtype (M : Type u_1) [Monoid M] :

Mˣ ≃ { x : M // IsUnit x }

Identify units with the subtype of elements satisfying IsUnit.

Equations

KloostermanWeil.unitsEquivIsUnitSubtype M = { toFun := fun (u : Mˣ) => ⟨↑u, ⋯⟩, invFun := fun (x : { x : M // IsUnit x }) => ⋯.unit, left_inv := ⋯, right_inv := ⋯ }

Instances For

noncomputable def KloostermanWeil.reciprocalPhase (N : ℕ) [NeZero N] (a x : ZMod N) :

The reciprocal additive phase on units, extended by zero on nonunits.

Equations

KloostermanWeil.reciprocalPhase N a x = if IsUnit x then ZMod.stdAddChar (a * x⁻¹) else 0

Instances For

noncomputable def KloostermanWeil.reciprocalMean (N : ℕ) [NeZero N] (a : ZMod N) :

The average of the reciprocal phase over all residue classes.

Equations

KloostermanWeil.reciprocalMean N a = (↑N)⁻¹ * ∑ x : ZMod N, KloostermanWeil.reciprocalPhase N a x

Instances For

noncomputable def KloostermanWeil.centeredReciprocalPhase (N : ℕ) [NeZero N] (a x : ZMod N) :

Subtract the full residue-class average from the reciprocal phase.

Equations

KloostermanWeil.centeredReciprocalPhase N a x = KloostermanWeil.reciprocalPhase N a x - KloostermanWeil.reciprocalMean N a

Instances For

theorem KloostermanWeil.sum_centeredReciprocalPhase_eq_zero (N : ℕ) [NeZero N] (a : ZMod N) :

∑ x : ZMod N, centeredReciprocalPhase N a x = 0

theorem KloostermanWeil.sum_reciprocalPhase_eq_kloostermanUnitSum (N : ℕ) [NeZero N] (a b : ZMod N) :

∑ x : ZMod N, ZMod.stdAddChar (b * x) * reciprocalPhase N a x = kloostermanUnitSum N a b

theorem KloostermanWeil.dft_centeredReciprocalPhase_nonzero (N : ℕ) [NeZero N] (a : ZMod N) {h : ZMod N} (hh : h ≠ 0) :

ZMod.dft (centeredReciprocalPhase N a) h = kloostermanUnitSum N a (-h)

theorem KloostermanWeil.stdAddChar_crt_bezout {m n : ℕ} [NeZero m] [NeZero n] [NeZero (m * n)] (hcop : m.Coprime n) (y : ℤ) :

ZMod.stdAddChar ↑y = ZMod.stdAddChar ↑(n.gcdA m * y) * ZMod.stdAddChar ↑(n.gcdB m * y)

Bézout/CRT factorization of the standard additive character on a coprime product modulus. The local shifts are units modulo the opposite factors.

theorem KloostermanWeil.norm_stdAddChar_eq_one (N : ℕ) [NeZero N] (h : ZMod N) :

‖ZMod.stdAddChar h‖ = 1

theorem KloostermanWeil.geometricKernel_norm_le {N : ℕ} [NeZero N] {h : ZMod N} (hh : h ≠ 0) (L : ℕ) :

‖∑ j ∈ Finset.range L, ZMod.stdAddChar h ^ j‖ ≤ ↑N / (2 * ↑(zmodFrequencyDistance h))

Geometric kernel bound for a nonzero Fourier frequency. This is the finite-completion denominator estimate used after centering.

theorem KloostermanWeil.sum_Ico_one_inv_le_harmonic (N : ℕ) :

∑ i ∈ Finset.Ico 1 N, (↑i)⁻¹ ≤ ↑(harmonic N)

theorem KloostermanWeil.sum_Ico_reflected_inv_eq (N : ℕ) :

∑ i ∈ Finset.Ico 1 N, (↑(N - i))⁻¹ = ∑ i ∈ Finset.Ico 1 N, (↑i)⁻¹

theorem KloostermanWeil.zmod_finEquiv_val {N : ℕ} [NeZero N] (i : Fin N) :

((ZMod.finEquiv N) i).val = ↑i

theorem KloostermanWeil.zmod_finEquiv_eq_zero_iff {N : ℕ} [NeZero N] (i : Fin N) :

(ZMod.finEquiv N) i = 0 ↔ ↑i = 0

theorem KloostermanWeil.fin_sum_inv_val_eq_Ico (N : ℕ) :

(∑ i : Fin N, if ↑i = 0 then 0 else (↑↑i)⁻¹) = ∑ i ∈ Finset.Ico 1 N, (↑i)⁻¹

theorem KloostermanWeil.fin_sum_inv_complement_eq_Ico_reflected (N : ℕ) :

(∑ i : Fin N, if ↑i = 0 then 0 else (↑(N - ↑i))⁻¹) = ∑ i ∈ Finset.Ico 1 N, (↑(N - i))⁻¹

theorem KloostermanWeil.frequencyReciprocalMass_le_two_harmonic (N : ℕ) [NeZero N] :

(∑ h : ZMod N, if h = 0 then 0 else (↑(zmodFrequencyDistance h))⁻¹) ≤ 2 * ↑(harmonic N)

Harmonic mass of all nonzero Fourier frequencies, in the symmetric distance normalization used by the geometric kernel.

theorem KloostermanWeil.frequencyReciprocalMass_le_log (N : ℕ) [NeZero N] :

(∑ h : ZMod N, if h = 0 then 0 else (↑(zmodFrequencyDistance h))⁻¹) ≤ 2 * (1 + Real.log ↑N)

noncomputable def KloostermanWeil.intervalCharacterKernel (N : ℕ) [NeZero N] (h x : ZMod N) (L : ℕ) :

The additive-character sum over L consecutive residue classes starting at x.

Equations

KloostermanWeil.intervalCharacterKernel N h x L = ∑ j ∈ Finset.range L, ZMod.stdAddChar (h * (x + ↑j))

Instances For

theorem KloostermanWeil.intervalCharacterKernel_eq (N : ℕ) [NeZero N] (h x : ZMod N) (L : ℕ) :

intervalCharacterKernel N h x L = ZMod.stdAddChar (h * x) * ∑ j ∈ Finset.range L, ZMod.stdAddChar h ^ j

theorem KloostermanWeil.intervalCharacterKernel_norm_le {N : ℕ} [NeZero N] {h : ZMod N} (hh : h ≠ 0) (x : ZMod N) (L : ℕ) :

‖intervalCharacterKernel N h x L‖ ≤ ↑N / (2 * ↑(zmodFrequencyDistance h))

noncomputable def KloostermanWeil.centeredIntervalSum (N : ℕ) [NeZero N] (a x : ZMod N) (L : ℕ) :

Sum the mean-centered reciprocal phase along a consecutive interval.

Equations

KloostermanWeil.centeredIntervalSum N a x L = ∑ j ∈ Finset.range L, KloostermanWeil.centeredReciprocalPhase N a (x + ↑j)

Instances For

theorem KloostermanWeil.finiteFourier_inversion {N : ℕ} [NeZero N] (f : ZMod N → ℂ) (y : ZMod N) :

f y = (↑N)⁻¹ * ∑ h : ZMod N, ZMod.stdAddChar (h * y) * ZMod.dft f h

theorem KloostermanWeil.intervalSum_fourier {N : ℕ} [NeZero N] (f : ZMod N → ℂ) (x : ZMod N) (L : ℕ) :

∑ j ∈ Finset.range L, f (x + ↑j) = (↑N)⁻¹ * ∑ h : ZMod N, ZMod.dft f h * intervalCharacterKernel N h x L

theorem KloostermanWeil.centeredReciprocalPhase_fourier_inversion (N : ℕ) [NeZero N] (a y : ZMod N) :

centeredReciprocalPhase N a y = (↑N)⁻¹ * ∑ h : ZMod N, ZMod.stdAddChar (h * y) * ZMod.dft (centeredReciprocalPhase N a) h

theorem KloostermanWeil.centeredIntervalSum_fourier (N : ℕ) [NeZero N] (a x : ZMod N) (L : ℕ) :

centeredIntervalSum N a x L = (↑N)⁻¹ * ∑ h : ZMod N, ZMod.dft (centeredReciprocalPhase N a) h * intervalCharacterKernel N h x L

theorem KloostermanWeil.intervalSum_norm_le_of_dft_bound {N : ℕ} [NeZero N] (f : ZMod N → ℂ) (hmean : ∑ y : ZMod N, f y = 0) (x : ZMod N) (L : ℕ) {B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (h : ZMod N), h ≠ 0 → ‖ZMod.dft f h‖ ≤ B) :

‖∑ j ∈ Finset.range L, f (x + ↑j)‖ ≤ B * (1 + Real.log ↑N)

Finite Fourier completion for any mean-zero function, using only a uniform bound on its nonzero Fourier coefficients.

theorem KloostermanWeil.centeredIntervalSum_norm_le_of_dft_bound {N : ℕ} [NeZero N] (a x : ZMod N) (L : ℕ) {B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ (h : ZMod N), h ≠ 0 → ‖ZMod.dft (centeredReciprocalPhase N a) h‖ ≤ B) :

‖centeredIntervalSum N a x L‖ ≤ B * (1 + Real.log ↑N)

Centered reciprocal-phase completion as an instance of mean-zero Fourier completion.

theorem KloostermanWeil.centeredReducedIntervalSum_le (hWeil : PrimeNondegenerateWeil) {A q : ℕ} (hq : 0 < q) (hsq : Squarefree q) (x : ZMod (reducedModulus A q)) (L : ℕ) :

‖centeredIntervalSum (reducedModulus A q) (↑(reducedNumerator A q)) x L‖ ≤ 2 ^ (reducedModulus A q).primeFactors.card * √↑(reducedModulus A q) * (1 + Real.log ↑(reducedModulus A q))

Centered incomplete reciprocal-phase completion at the reduced squarefree modulus. The interval length is unrestricted. The PrimeNondegenerateWeil premise is proved in LeanPool.KloostermanWeil.Weil.PrimeKloosterman.

Weighted region: discrete partial summation with reciprocal weights, an explicit consequence of the preceding centered interval bound.

noncomputable def KloostermanWeil.reciprocalNatWeight (Y i : ℕ) :

The reciprocal weight 1 / (Y + i), viewed as a complex number.

Equations

KloostermanWeil.reciprocalNatWeight Y i = ↑(↑(Y + i))⁻¹

Instances For

theorem KloostermanWeil.partialSummation_reciprocal_weight_le (Y L : ℕ) (hY : 0 < Y) (c : ℕ → ℂ) {C : ℝ} (hC0 : 0 ≤ C) (hprefix : ∀ k ≤ L, ‖∑ j ∈ Finset.range k, c j‖ ≤ C) :

‖∑ j ∈ Finset.range L, c j * reciprocalNatWeight Y j‖ ≤ 2 * C / ↑Y

Discrete partial summation for reciprocal weights. A uniform bound C on all initial partial sums over a consecutive interval starting at Y>0 gives an explicit 2C/Y weighted bound.

noncomputable def KloostermanWeil.weightedCenteredIntervalSum (N : ℕ) [NeZero N] (a x : ZMod N) (Y L : ℕ) :

The centered reciprocal-phase interval sum with weights 1 / (Y + j).

Equations

KloostermanWeil.weightedCenteredIntervalSum N a x Y L = ∑ j ∈ Finset.range L, KloostermanWeil.centeredReciprocalPhase N a (x + ↑j) * KloostermanWeil.reciprocalNatWeight Y j

Instances For

theorem KloostermanWeil.weightedCenteredReducedIntervalSum_le (hWeil : PrimeNondegenerateWeil) {A q : ℕ} (hq : 0 < q) (hsq : Squarefree q) (x : ZMod (reducedModulus A q)) (Y L : ℕ) (hY : 0 < Y) :

‖weightedCenteredIntervalSum (reducedModulus A q) (↑(reducedNumerator A q)) x Y L‖ ≤ 2 * (2 ^ (reducedModulus A q).primeFactors.card * √↑(reducedModulus A q) * (1 + Real.log ↑(reducedModulus A q))) / ↑Y

Partial summation applied to the centered reduced-modulus completion. The interval length remains unrestricted.