OAI/NumberTheory/TwoPoint/Walks/FiveColorOrientation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Five colors separate the two orientations of a short interval of shifts.

  1. def OAI.TwoPointCorrelations.intervalColor line 10
  2. def OAI.TwoPointCorrelations.forwardColorPair line 12
  3. lemma OAI.TwoPointCorrelations.short_shift_quotient_gap line 16
  4. lemma OAI.TwoPointCorrelations.short_shift_forward_colors line 24
  5. lemma OAI.TwoPointCorrelations.short_shift_not_reverse_colors line 30
  6. lemma OAI.TwoPointCorrelations.intervalColor_bounds line 36
  7. lemma OAI.TwoPointCorrelations.five_color_isolates_forward line 41

    Source documentation

    Once a pair of endpoint colors has been fixed, the symmetric graph's reverse edge cannot appear in its forward bilinear test.

    lemma five_color_isolates_forward (D x y : ℤ) (hD : 0 < D)
    (hcolors : forwardColorPair D x y)
    (hedge : (D ≤ y - x ∧ y - x < 2 * D) ∨ (D ≤ x - y ∧ x - y < 2 * D)) :
    D ≤ y - x ∧ y - x < 2 * D := by
…

    Mentions: OAI.TwoPointCorrelations.forwardColorPair