DistinguishedCoefficients.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The distinguished-tuple weight occurring in stopped coefficients. Its multiplicity is bounded in terms of the fixed tuple length, so the literal beta coefficient has one divisor-count loss independently of bins.

def OAI.CubicFirstMoment.distinguishedTupleCoefficient line 15
lemma OAI.CubicFirstMoment.distinguishedPrimeWeight_norm_le_one line 20
theorem OAI.CubicFirstMoment.distinguishedTupleCoefficient_norm line 28

theorem OAI.CubicFirstMoment.stoppedBeta_distinguished_divisor_bound line 50

Source documentation

The source beta built from a bounded distinguished tuple and the actual cutoff-Mobius divisor has a fixed divisor bound. No occupancy count and no roughness-boundary parameter appears in its constant.

theorem stoppedBeta_distinguished_divisor_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) (w z : ℝ)
    (selected : Eisenstein → Eisenstein → Prop) (b : Eisenstein) :
    ‖stoppedBeta R D (distinguishedTupleCoefficient S W ψ w z) ψ w selected b‖ ≤
      ((R.filter (fun r => r ∣ b)).card:ℝ) *
        (‖((Fintype.card ι).factorial:ℂ)⁻¹‖ *
          ((Fintype.card ι)^(Fintype.card ι):ℕ)) :=
…

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