ShortPeriodCut.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A failed affine lift of centered circle representatives crosses the cut.

The crossing is allowed at either endpoint of the parameter interval. This is needed when the initial centered representative is the included endpoint -1 / 2 and the affine line immediately leaves the centered interval.

theorem OAI.QuantitativeVanDerWaerden.centered_representative_unique_of_integer_difference line 15

Source documentation

Two centered representatives congruent modulo the integers are equal.

theorem centered_representative_unique_of_integer_difference {x y : ℝ}
    (hx : -(1 / 2 : ℝ) ≤ x ∧ x < 1 / 2)
    (hy : -(1 / 2 : ℝ) ≤ y ∧ y < 1 / 2)
    (hcongr : ∃ z : ℤ, x - y = z) : x = y := by
…

theorem OAI.QuantitativeVanDerWaerden.affine_cut_of_leaving_centered_interval line 29

Source documentation

A real affine segment starting in the centered interval and ending outside it meets one of the two boundary representatives of the circle cut.

theorem affine_cut_of_leaving_centered_interval {A w T : ℝ}
    (hA : -(1 / 2 : ℝ) ≤ A ∧ A < 1 / 2) (hT : 0 ≤ T)
    (hout : ¬ (-(1 / 2 : ℝ) ≤ A + T * w ∧ A + T * w < 1 / 2)) :
    w ≠ 0 ∧ ∃ t : ℝ, 0 ≤ t ∧ t ≤ T ∧
      ∃ z : ℤ, A + t * w = 1 / 2 + z := by
…

theorem OAI.QuantitativeVanDerWaerden.failed_centered_lift_cut line 62

Source documentation

Failure of a real affine lift of a finite centered progression gives a cut crossing at a real parameter between 0 and k - 1. Integer congruence alone suffices; no assumption on the size of the affine step is needed.

theorem failed_centered_lift_cut {Y : ℕ → ℝ} {A w : ℝ} {k : ℕ}
    (hrep : ∀ j, j < k → -(1 / 2 : ℝ) ≤ Y j ∧ Y j < 1 / 2)
    (hbase : Y 0 = A)
    (hcongr : ∀ j, j < k → ∃ z : ℤ, Y j - (A + (j : ℝ) * w) = z)
    (hfail : ∃ j, j < k ∧ Y j ≠ A + (j : ℝ) * w) :
    w ≠ 0 ∧ ∃ t : ℝ, 0 ≤ t ∧ t ≤ (k : ℝ) - 1 ∧
      ∃ z : ℤ, A + t * w = 1 / 2 + z := by
…