OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupingGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The uniform ordinary-block grouping gap away from the exceptional three-prime configuration. All bounds come from finite-dimensional compactness applied to the proved subset-sum alternative.

  1. def OAI.CubicFirstMoment.primeGroupingGap line 15
  2. lemma OAI.CubicFirstMoment.continuous_primeGroupingGap line 20
  3. lemma OAI.CubicFirstMoment.primeGroupingGap_pos line 25
  4. theorem OAI.CubicFirstMoment.uniform_prime_grouping_gap line 38

    Source documentation

    The ordinary-configuration compactness argument, with an explicit fixed neighborhood of the exceptional triple removed.

    theorem uniform_prime_grouping_gap {ξ b δ : ℝ} (hξ : 0 < ξ)
    (hb : b < 2/3) (hδ : 0 < δ) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ a : ι → ℝ,
      (∀ i, ξ ≤ a i ∧ a i ≤ b) → (∑ i, a i) = 1 →
      (Fintype.card ι = 3 → δ ≤ ∑ i, |a i-1/3|) →
      ∃ s : Finset ι, 1/3+ε ≤ ∑ i ∈ s, a i ∧ ∑ i ∈ s, a i ≤ 2/3-ε := by
…