OAI/NumberTheory/TotientAsymptotic/FirstCollision.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual first-difference partition and its suffix quotient.

  1. def OAI.TotientAsymptotic.FirstDifferenceAt line 16
  2. def OAI.TotientAsymptotic.firstCollisionPairs line 23
  3. def OAI.TotientAsymptotic.firstCollisionSuffixes line 27
  4. lemma OAI.TotientAsymptotic.firstCollisionPairs_data line 31
  5. lemma OAI.TotientAsymptotic.firstCollisionSuffixes_equal_value line 41
  6. theorem OAI.TotientAsymptotic.first_collision_dyadic_blocks line 57

    Source documentation

    Every actual positive first-difference pair lies in Ford's counting block at its suffix's dyadic endpoint. This holds for both chosen witnesses.

    theorem first_collision_dyadic_blocks : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, 1 ≤ i → i ≤ R x H → L x H < m x → R x H < L x H →
    ∀ t y : ℝ, ∀ q ∈ firstCollisionPairs x H t i,
    y/2 < (prefixDenominator (tupleSuffix q.1 i) : ℝ) →
    (prefixDenominator (tupleSuffix q.1 i) : ℝ) ≤ y →
    GoodCollisionBlock x t H i y q ∧
    (87/100 : ℝ)*fordBandScale x i ≤ B y ∧ B y ≤ (113/100 : ℝ)*fordBandScale x i := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.firstCollisionPairs, OAI.TotientAsymptotic.prefixDenominator, OAI.TotientAsymptotic.tupleSuffix, OAI.TotientAsymptotic.GoodCollisionBlock, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.B