HarmonicResidueDomination.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coarse residue domination for the original harmonic prime priors

Only an upper bound is needed here. Dyadic interval counts give it without any distribution theorem for primes, including at the boundary of a word bin.

theorem OAI.Ostmann.harmonic_residue_block_le line 18

theorem OAI.Ostmann.harmonic_residue_dyadic_le line 50

Source documentation

The number of dyadic blocks, rather than the length of the prime range, controls the harmonic mass of a residue class.

theorem harmonic_residue_dyadic_le (S : Finset ℕ) (q h J : ℕ)
    (hq : 0 < q) (hsmall : q ≤ 2 ^ h)
    (hrange : ∀ n ∈ S, 2 ^ h ≤ n ∧ n < 2 ^ (h + J))
    (hcongr : ∀ a ∈ S, ∀ b ∈ S, a ≡ b [MOD q]) :
    (∑ n ∈ S, (n : ℝ)⁻¹) ≤ 3 * J / q := by
…

theorem OAI.Ostmann.primeSubsetPrior_residue_le line 94

Source documentation

Exact harmonic priors on arbitrary prime subsets obey the same bound. No primality or interval closure of the selected subset is needed.

theorem primeSubsetPrior_residue_le (P S : Finset ℕ) (q h J : ℕ)
    (hq : 0 < q) (hsmall : q ≤ 2 ^ h)
    (hrange : ∀ n ∈ S, 2 ^ h ≤ n ∧ n < 2 ^ (h + J)) (a : ZMod q) :
    cellPrior (primeSubsetPrior P S) (fun p => ((p : ℕ) : ZMod q)) a ≤
      (∑ n ∈ S, (n : ℝ)⁻¹)⁻¹ * (3 * J / q) := by
…

Mentions: OAI.Ostmann.cellPrior, OAI.Ostmann.primeSubsetPrior