FixedAngularHecke.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Quantitative fixed-angular Hecke prime estimates

The published input is the degree-two, nonexceptional specialization of Kaneko--Thorner, Highly uniform prime number theorems, Ann. Inst. Fourier 75 (2025), Theorem 1.2, pp. 1904--1905 (restating Iwaniec--Kowalski, Theorem 5.13), with the zero-free region and completion from Rajan (1998), Proposition 1 and Section 1. The exponential conductor-dependent error is retained. Arbitrary logarithmic savings are derived below; they are not included among the published-input hypotheses.

def OAI.CubicFirstMoment.heckeExponentialError line 26
Source documentation
The conductor-dependent error in the published prime number theorem.
```
def heckeExponentialError (c x Q : ℝ) : ℝ :=
…
```
lemma OAI.CubicFirstMoment.eventually_loglog_small line 30
lemma OAI.CubicFirstMoment.heckeExponentialError_logSaving line 51
Source documentation
Logarithmic conductor growth makes the published exponential error smaller than any prescribed logarithmic saving, uniformly in the conductor.
```
lemma heckeExponentialError_logSaving {c K A D : ℝ}
    (hc : 0 < c) (hK : 0 < K) :
    ∀ᶠ x : ℝ in atTop, ∀ Q : ℝ, 1 ≤ Q → Q ≤ K * (Real.log x) ^ A →
      heckeExponentialError c x Q ≤ 16 * x / (Real.log x) ^ D := by
…
```
Mentions: OAI.CubicFirstMoment.heckeExponentialError
lemma OAI.CubicFirstMoment.sqrt_logSq_logSaving line 109
Source documentation
The prime-power deletion error is also negligible at every fixed logarithmic scale.
```
lemma sqrt_logSq_logSaving (D : ℝ) :
    ∀ᶠ x : ℝ in atTop, Real.sqrt x * (Real.log x) ^ 2 ≤ x / (Real.log x) ^ D := by
…
```
def OAI.CubicFirstMoment.angularMixedCubic line 130
Source documentation
The actual fixed-angular character on the primary generators used by this development. A nonzero angular index makes it nonprincipal.
```
def angularMixedCubic (ℓ : ℤ) (q₁ q₂ a : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.angularConductorFactor line 135
Source documentation
Upper bound for the degree-two analytic conductor: finite conductor at most 9 N(q₁q₂), field discriminant 3, and gamma shifts k,k+1.
```
def angularConductorFactor (ℓ : ℤ) : ℝ :=
…
```
def OAI.CubicFirstMoment.angularAnalyticConductor line 138
lemma OAI.CubicFirstMoment.angularConductorFactor_ge_one line 141
lemma OAI.CubicFirstMoment.angularAnalyticConductor_ge_one line 145
def OAI.CubicFirstMoment.primeChebyshev line 156
Source documentation
The logarithmically weighted sum over the actual primary prime elements.
```
def primeChebyshev (ψ : Eisenstein → ℂ) (x : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.FixedAngularPrimeExplicitEstimate line 164
Source documentation
Published fixed-type explicit prime estimate, before any logarithmic saving is deduced. This is the degree-two, nonexceptional case of Kaneko--Thorner Theorem 1.2 with Rajan's fixed-type zero-free region. The displayed second term retains the cost of higher prime powers and the omitted prime above three. It is an explicit input, not an axiom.
```
def FixedAngularPrimeExplicitEstimate : Prop :=
…
```

theorem OAI.CubicFirstMoment.fixedAngular_chebyshev_logSaving line 175

Source documentation

The logarithmic saving is a deduction from the conductor-dependent published error, uniform in the small-conductor family.

theorem fixedAngular_chebyshev_logSaving (hEF : FixedAngularPrimeExplicitEstimate)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) (A D : ℝ) (_hA : 0 < A) (_hD : 0 < D) :
    ∃ C X₀ : ℝ, 0 < C ∧ 1 < X₀ ∧
      ∀ x : ℝ, X₀ ≤ x → ∀ q₁ q₂ : Eisenstein,
        primary q₁ → primary q₂ → Squarefree q₁ → Squarefree q₂ → IsCoprime q₁ q₂ →
        norm (q₁ * q₂) ≤ (Real.log x) ^ A →
        ‖primeChebyshev (angularMixedCubic ℓ q₁ q₂) x‖ ≤ C * x / (Real.log x) ^ D := by
…

Mentions: OAI.CubicFirstMoment.FixedAngularPrimeExplicitEstimate, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeChebyshev, OAI.CubicFirstMoment.angularMixedCubic

theorem OAI.CubicFirstMoment.weighted_fixedAngular_prime_bound line 202

Source documentation

Partial summation removes the logarithmic prime weight, permitting smooth weights and norm phases. The derivative cost is retained exactly.

theorem weighted_fixedAngular_prime_bound (hEF : FixedAngularPrimeExplicitEstimate)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) (A D : ℝ) (hA : 0 < A) (hD : 0 < D) :
    ∃ C X₀ : ℝ, 0 < C ∧ 1 < X₀ ∧
      ∀ a b : ℝ, X₀ ≤ a → a ≤ b → ∀ q₁ q₂ : Eisenstein,
        primary q₁ → primary q₂ → Squarefree q₁ → Squarefree q₂ → IsCoprime q₁ q₂ →
        norm (q₁ * q₂) ≤ (Real.log a) ^ A → ∀ f : ℝ → ℂ,
          (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ (fun t => f t / (Real.log t : ℂ)) t) →
          IntegrableOn (deriv (fun t => f t / (Real.log t : ℂ))) (Set.Icc a b) →
          ‖∑ p ∈ (primeCutoff b).filter (fun p => a < norm p),
            f (norm p) * angularMixedCubic ℓ q₁ q₂ p‖ ≤
          (C * b / (Real.log a) ^ D) *
            (‖f a / (Real.log a : ℂ)‖ + ‖f b / (Real.log b : ℂ)‖ +
…

theorem OAI.CubicFirstMoment.finite_prime_deletion_bound line 246

Source documentation

Removing any finite set of Euler factors has this exact error; no implicit identification of ramified or omitted prime values is used.

theorem finite_prime_deletion_bound (ψ : Eisenstein → ℂ) (f : ℝ → ℂ)
    (E : Finset Eisenstein) (x : ℝ) :
    ‖(∑ p ∈ (primeCutoff x).filter (fun p => p ∉ E), f (norm p) * ψ p) -
      primeCutoffSum (fun p => f (norm p) * ψ p) x‖ ≤
      ∑ p ∈ (primeCutoff x).filter (fun p => p ∈ E), ‖f (norm p)‖ * ‖ψ p‖ := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCutoffSum

lemma OAI.CubicFirstMoment.angularMixedCubic_mul line 262
lemma OAI.CubicFirstMoment.angularMixedCubic_one line 269
lemma OAI.CubicFirstMoment.angularMixedCubic_prod line 274

theorem OAI.CubicFirstMoment.independent_angular_prime_tuple_character_sum line 285

Source documentation

Independent prime-convolution constituents factor with the same fixed angular character; all smooth weights remain in the separate factors.

theorem independent_angular_prime_tuple_character_sum {ι : Type*} [Fintype ι] [DecidableEq ι]
    (supports : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ)
    {q₁ q₂ : Eisenstein} (h₁ : primary q₁) (h₂ : primary q₂) (ℓ : ℤ) :
    (∑ f ∈ Fintype.piFinset supports,
      (∏ i, w i (f i)) * angularMixedCubic ℓ q₁ q₂ (∏ i, f i)) =
      ∏ i, ∑ p ∈ supports i, w i p * angularMixedCubic ℓ q₁ q₂ p := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.angularMixedCubic

theorem OAI.CubicFirstMoment.independent_angular_prime_tuple_bound line 298

Source documentation

Cancellation bounds for the individual prime sums propagate to the actual independent convolution, with no condition coupling the factors.

theorem independent_angular_prime_tuple_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    (supports : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ)
    {q₁ q₂ : Eisenstein} (h₁ : primary q₁) (h₂ : primary q₂) (ℓ : ℤ)
    (H : ι → ℝ)
    (hH : ∀ i, ‖∑ p ∈ supports i, w i p * angularMixedCubic ℓ q₁ q₂ p‖ ≤ H i) :
    ‖∑ f ∈ Fintype.piFinset supports,
      (∏ i, w i (f i)) * angularMixedCubic ℓ q₁ q₂ (∏ i, f i)‖ ≤ ∏ i, H i := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.angularMixedCubic

def OAI.CubicFirstMoment.normPrimeInterval line 309
Source documentation
Independently prescribed interval of primary primes.
```
def normPrimeInterval (a b : ℝ) : Finset Eisenstein :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.primeLogVariation line 313
Source documentation
The exact partial-summation cost after removing the logarithmic weight.
```
def primeLogVariation (f : ℝ → ℂ) (a b : ℝ) : ℝ :=
…
```
def OAI.CubicFirstMoment.independentNormPrimeSum line 318
Source documentation
Actual weighted independent prime convolution, before collecting products.
```
def independentNormPrimeSum {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a b : ι → ℝ) (f : ι → ℝ → ℂ) (ψ : Eisenstein → ℂ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein

theorem OAI.CubicFirstMoment.fixedAngular_prime_convolution_bound line 325

Source documentation

Small-conductor cancellation for the actual independently weighted prime convolution, deduced from the quantitative published input.

theorem fixedAngular_prime_convolution_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    (hEF : FixedAngularPrimeExplicitEstimate) (ℓ : ℤ) (hℓ : ℓ ≠ 0)
    (A D : ℝ) (hA : 0 < A) (hD : 0 < D) :
    ∃ C X₀ : ℝ, 0 < C ∧ 1 < X₀ ∧
      ∀ q₁ q₂ : Eisenstein,
        primary q₁ → primary q₂ → Squarefree q₁ → Squarefree q₂ → IsCoprime q₁ q₂ →
        ∀ (a b : ι → ℝ) (f : ι → ℝ → ℂ),
          (∀ i, X₀ ≤ a i) → (∀ i, a i ≤ b i) →
          (∀ i, norm (q₁ * q₂) ≤ (Real.log (a i)) ^ A) →
          (∀ i t, t ∈ Set.Icc (a i) (b i) →
            DifferentiableAt ℝ (fun t => f i t / (Real.log t : ℂ)) t) →
          (∀ i, IntegrableOn (deriv (fun t => f i t / (Real.log t : ℂ)))
…

Mentions: OAI.CubicFirstMoment.FixedAngularPrimeExplicitEstimate, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm