MellinExceptionalSamples.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sparse samples in the exceptional frequency class

Every exceptional frequency has a large prime polynomial in each selected band. The exact high-moment bound therefore controls any separated sample of this class. The statement retains the chosen moment order and cutoff.

def OAI.JointDickman.MellinPrimeBands.sampleCost line 18
lemma OAI.JointDickman.MellinPrimeBands.bin_sample_bound line 25

theorem OAI.JointDickman.MellinPrimeBands.exceptional_samples line 57

Source documentation

A separated sample of the residual class is covered by the large values in any one of its bands. This is a finite counting argument, followed by the proved prime high-moment estimate.

theorem exceptional_samples (D : MellinPrimeBands) (f : ℕ → ℂ)
    (hf : OneBounded f) {J j : ℕ} (hj : j < J)
    (hprime : ∀ p ∈ D.primes j, p.Prime)
    (M : ℕ → ℕ) (r : ℕ)
    (hM : ∀ k ∈ D.bins j, ∀ p ∈ D.primes j, D.bin j p = k → p ≤ M k)
    (hV : ∀ k ∈ D.bins j, 0 < D.threshold j k)
    (S : Finset ℝ) {T : ℝ} (hT : 0 ≤ T)
    (hS : ∀ t ∈ S, |t| ≤ T)
    (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|)
    (hres : ∀ t ∈ S, t ∈ mrtNoSmallBand D.bins (D.polynomial f) D.threshold J) :
    (S.card : ℝ) ≤ ∑ k ∈ D.bins j, D.sampleCost j k (M k) r T := by
…

Mentions: OAI.JointDickman.MellinPrimeBands