OAI/NumberTheory/CubicMoment/Estimates/PrimeIntervalGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The stopped crossing tests with one prime left free. A distinguished prime enters by its actual norm; a selected-bin prime leaves every surrogate prefix unchanged while its bin is fixed.

  1. def OAI.CubicFirstMoment.largestPrimePredicate line 13
  2. lemma OAI.CubicFirstMoment.largestPrimePredicate_away_tie line 19

    Source documentation

    A fixed-order tie rule changes the lower norm interval at just the single norm of the largest complementary prime.

    lemma largestPrimePredicate_away_tie (code : Eisenstein → ℕ)
    (s : Finset Eisenstein) (p : Eisenstein) (hne : normNat p ≠ s.sup normNat) :
    largestPrimePredicate code s p ↔ s.sup normNat < normNat p := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.largestPrimePredicate

  3. lemma OAI.CubicFirstMoment.crossing_norm_interval line 34
  4. lemma OAI.CubicFirstMoment.distinguished_prime_crossing_interval line 49
  5. lemma OAI.CubicFirstMoment.product_norm_interval line 56
  6. lemma OAI.CubicFirstMoment.primeSurrogate_insert_same_bin line 70
  7. lemma OAI.CubicFirstMoment.primeSurrogate_prefix_insert_same_bin line 76
  8. lemma OAI.CubicFirstMoment.primeBin_card_insert_same_bin line 90