Standard Bombieri--Vinogradov: finite character orthogonality

This file contains only the finite algebra between Chebyshev Λ sums in a reduced residue class and Dirichlet-character prefix sums. In particular, the principal character is split literally before any estimate is made. No Bombieri--Vinogradov conclusion is assumed or stated.

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaNatCoeff (n : ℕ) : ℂ

The Chebyshev Λ coefficient, regarded as a complex coefficient.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaNatCoeff n = ↑(ArithmeticFunction.vonMangoldt n)

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaAPPrefix (y q a : ℕ) : ℂ

The Chebyshev prefix in one residue class, through the integer endpoint y.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaAPPrefix y q a = ∑ n ∈ Finset.range (y + 1) with ↑n = ↑a, AnalyticNumberTheory.LargeSieve.lambdaNatCoeff n

noncomputable def AnalyticNumberTheory.LargeSieve.coprimeLambdaPrefix (y q : ℕ) : ℂ

The full Chebyshev prefix restricted to integers coprime to q.

Equations

• AnalyticNumberTheory.LargeSieve.coprimeLambdaPrefix y q = ∑ n ∈ Finset.range (y + 1) with n.Coprime q, AnalyticNumberTheory.LargeSieve.lambdaNatCoeff n

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix (y q : ℕ) (χ : DirichletCharacter ℂ q) : ℂ

The level-q character transform of the Chebyshev prefix.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix y q χ = ∑ n ∈ Finset.range (y + 1), AnalyticNumberTheory.LargeSieve.lambdaNatCoeff n * χ ↑n

theorem AnalyticNumberTheory.LargeSieve.lambdaAPPrefix_eq_character_average {q a : ℕ} (hq : 0 < q) (ha : a.Coprime q) (y : ℕ) : lambdaAPPrefix y q a = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, star (χ ↑a) * lambdaCharacterPrefix y q χ

Character orthogonality expands a reduced-residue Chebyshev prefix exactly. The normalization 1/φ(q) is retained literally.

theorem AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix_one (y q : ℕ) : lambdaCharacterPrefix y q 1 = coprimeLambdaPrefix y q

The principal character transform is exactly the coprime Λ total.

noncomputable def AnalyticNumberTheory.LargeSieve.principalLambdaContribution (y q : ℕ) : ℂ

The principal contribution to the character average.

Equations

• AnalyticNumberTheory.LargeSieve.principalLambdaContribution y q = (↑q.totient)⁻¹ * AnalyticNumberTheory.LargeSieve.coprimeLambdaPrefix y q

noncomputable def AnalyticNumberTheory.LargeSieve.principalLambdaMainError (y q : ℕ) : ℂ

Its error relative to the global Chebyshev main term y.

Equations

• AnalyticNumberTheory.LargeSieve.principalLambdaMainError y q = AnalyticNumberTheory.LargeSieve.coprimeLambdaPrefix y q - ↑y

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaAPMainError (y q a : ℕ) : ℂ

The reduced-residue Chebyshev error centered at the global main term.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaAPMainError y q a = AnalyticNumberTheory.LargeSieve.lambdaAPPrefix y q a - (↑q.totient)⁻¹ * ↑y

theorem AnalyticNumberTheory.LargeSieve.lambdaAPMainError_eq_principal_add_nonprincipal {q a : ℕ} (hq : 0 < q) (ha : a.Coprime q) (y : ℕ) : lambdaAPMainError y q a = (↑q.totient)⁻¹ * principalLambdaMainError y q + (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, star (χ ↑a) * lambdaCharacterPrefix y q χ

Literal principal/nonprincipal decomposition of the Chebyshev AP error. The first summand is precisely the principal PNT-type error divided by φ(q); all character estimates apply only to the second summand.

theorem AnalyticNumberTheory.LargeSieve.norm_lambdaAPMainError_le_principal_add_nonprincipal {q a : ℕ} (hq : 0 < q) (ha : a.Coprime q) (y : ℕ) : ‖lambdaAPMainError y q a‖ ≤ (↑q.totient)⁻¹ * (‖principalLambdaMainError y q‖ + ∑ χ ∈ nonprincipalCharacters q, ‖lambdaCharacterPrefix y q χ‖)

A pointwise reduced-residue error is bounded by the literal principal error plus the nonprincipal character transforms.

noncomputable def AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError (N q : ℕ) : ℝ

Maximum principal PNT-type error through endpoint N.

Equations

• AnalyticNumberTheory.LargeSieve.principalLambdaPrefixMaxError N q = (Finset.image (fun (y : ℕ) => ‖AnalyticNumberTheory.LargeSieve.principalLambdaMainError y q‖) (Finset.range (N + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefixMaxAmplitude (N q : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

Maximum transform amplitude for one character through endpoint N.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefixMaxAmplitude N q χ = (Finset.image (fun (y : ℕ) => ‖AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix y q χ‖) (Finset.range (N + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaAPPrefixMaxError (N q : ℕ) : ℝ

The Chebyshev AP error, maximized over canonical reduced residues and all prefixes through N. Adjoining zero gives the empty-modulus convention and a canonical witness for max'.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaAPPrefixMaxError N q = (insert 0 (Finset.image (fun (p : ℕ × ℕ) => ‖AnalyticNumberTheory.LargeSieve.lambdaAPMainError p.1 q p.2‖) ((Finset.range (N + 1)).product (AnalyticNumberTheory.Sieve.unitResidues q)))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.lambdaAPPrefixMaxError_le_character_majorant {q N : ℕ} (hq : 0 < q) : lambdaAPPrefixMaxError N q ≤ (↑q.totient)⁻¹ * (principalLambdaPrefixMaxError N q + ∑ χ ∈ nonprincipalCharacters q, lambdaCharacterPrefixMaxAmplitude N q χ)

Exact finite prefix-max consequence of character orthogonality.