PrimeNormEndpoints.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Endpoint and largest-prime tie corrections. At most two primary primes have a prescribed norm, so endpoint choices cost an absolute constant in a bounded prime sum.

lemma OAI.CubicFirstMoment.primaryPrime_eq_or_conjugate_of_norm_eq line 13
Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/PrimeSharpCutoff.lean:20 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.primaryPrime_eq_or_conjugate_of_norm_eq@path.
theorem OAI.CubicFirstMoment.primaryPrime_norm_fiber_card line 27
lemma OAI.CubicFirstMoment.primaryPrime_two_norm_card line 48

theorem OAI.CubicFirstMoment.prime_interval_endpoint_difference line 63

Source documentation

This also covers an arbitrary fixed-order selection among equal-norm largest primes. Away from the two boundary norms the predicates agree.

theorem prime_interval_endpoint_difference (S : Finset Eisenstein)
    (hS : ∀ p ∈ S, primaryPrime p) (P Q : Eisenstein → Prop) (a b : ℝ)
    (hPQ : ∀ p ∈ S, norm p ≠ a → norm p ≠ b → (P p ↔ Q p))
    (w : Eisenstein → ℂ) {M : ℝ} (hM : 0 ≤ M) (hw : ∀ p ∈ S, ‖w p‖ ≤ M) :
    ‖(∑ p ∈ S with P p, w p)-(∑ p ∈ S with Q p, w p)‖ ≤ 4*M := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm