DistinguishedRoughness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The roughness of the actual distinguished coefficient, followed by a uniform bound for the stopped beta. Zero distinguished coefficients are removed before counting divisors, so no support hypothesis is added.

theorem OAI.CubicFirstMoment.distinguishedTupleCoefficient_prime_support line 15
lemma OAI.CubicFirstMoment.stoppedBeta_filter_nonzero line 38

theorem OAI.CubicFirstMoment.stoppedBeta_distinguished_rough_bound line 60

Source documentation

Literal beta has a fixed bound, independent of the number of bin primes. Only distinguished prime factors are counted in its divisor fibre.

theorem stoppedBeta_distinguished_rough_bound
    (S : ι → Finset Eisenstein) (hS : ∀ i, ∀ p ∈ S i, primaryPrime p)
    (W : ι → Eisenstein → ℂ) (hW : ∀ i, ∀ p ∈ S i, ‖W i p‖ ≤ 1)
    (R D : Finset Eisenstein) (hR : ∀ r ∈ R, primary r)
    {ψ : ℝ → ℝ} (hψ : ∀ x, 0 ≤ ψ x ∧ ψ x ≤ 1)
    (hψone : ∀ x : ℝ, 0 < x → x ≤ 1 → ψ x = 1)
    (hψzero : ∀ x : ℝ, 2 ≤ x → ψ x = 0)
    {w z : ℝ} (hw : 1 ≤ w) (hwz : w ≤ z)
    (selected : Eisenstein → Eisenstein → Prop)
    {b : Eisenstein} (hb : primary b) (hs : Squarefree b) {k : ℕ}
    (hsize : norm b < w^k) :
    ‖stoppedBeta R D (distinguishedTupleCoefficient S W ψ w z) ψ w selected b‖ ≤
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.stoppedBeta, OAI.CubicFirstMoment.distinguishedTupleCoefficient