OAI/NumberTheory/CubicMoment/Estimates/PrimeBins.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The first stopping bin is selected from actual finite prime bins. Only the final bin and its selected count are exposed as outer indices.

  1. def OAI.CubicFirstMoment.primeBin line 12
  2. def OAI.CubicFirstMoment.primeBinPrefix line 15
  3. def OAI.CubicFirstMoment.primeSurrogate line 18
  4. lemma OAI.CubicFirstMoment.primeBinPrefix_succ line 21
  5. lemma OAI.CubicFirstMoment.primeBinPrefix_disjoint line 29
  6. lemma OAI.CubicFirstMoment.primeSurrogate_prefix_succ line 37
  7. lemma OAI.CubicFirstMoment.first_crossing_index line 51
  8. theorem OAI.CubicFirstMoment.first_prime_bin line 71

    Source documentation

    Exact selection of the first bin and the first count within it. The terminal bin contributes no occupancy-vector outer index.

    theorem first_prime_bin (s : Finset Eisenstein) (b : Eisenstein → ℕ)
    (ell : ℕ → ℝ) {m : ℕ} (hb : ∀ p ∈ s, b p < m)
    (hell : ∀ j < m, 1 < ell j) {R Z : ℝ} (hR : 0 < R) (hstart : R < Z)
    (hend : Z ≤ R*primeSurrogate s b ell) :
    ∃ j < m, ∃ k : ℕ, 1 ≤ k ∧ k ≤ (primeBin s b j).card ∧
      (R*primeSurrogate (primeBinPrefix s b j) b ell)*ell j^k/ell j < Z ∧
      Z ≤ (R*primeSurrogate (primeBinPrefix s b j) b ell)*ell j^k := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.primeBinPrefix