Dichotomy.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Real-representative lemmas for the outer-color dichotomy

The integer congruences here are the concrete meaning of equality modulo one. In particular, the heavy-interval estimate uses only its two endpoint representatives and does not assume that the path between them avoids a cut.

theorem OAI.QuantitativeVanDerWaerden.real_eq_of_integer_difference_small line 15

theorem OAI.QuantitativeVanDerWaerden.dilation_drift_eq line 24

Source documentation

The short displacement in the two coordinate systems agrees over the reals.

theorem dilation_drift_eq {u v lam A B : ℝ}
    (hint : ∃ z : ℤ, v - lam * u = (z : ℝ))
    (hv : |v| ≤ A) (hu : |lam * u| ≤ B) (hsmall : A + B < 1) : v = lam * u := by
…

theorem OAI.QuantitativeVanDerWaerden.heavy_endpoint_eq line 31

Source documentation

Endpoint congruence and short total drift give equality before reduction modulo one.

theorem heavy_endpoint_eq {Δ a v L T : ℝ}
    (hint : ∃ z : ℤ, Δ - a * v = (z : ℝ))
    (hΔ : |Δ| ≤ L) (hv : |a * v| ≤ T) (hsmall : L + T < 1) : Δ = a * v := by
…

theorem OAI.QuantitativeVanDerWaerden.heavy_interval_drift_div line 37

theorem OAI.QuantitativeVanDerWaerden.heavy_interval_relative_drift line 46

Source documentation

The relative-width estimate for every heavy interval in the progression.

theorem heavy_interval_relative_drift {Δ a v L T k M : ℝ}
    (hk : 0 < k) (hM : 0 < M) (ha : k / (2 * M) ≤ a)
    (hint : ∃ z : ℤ, Δ - a * v = (z : ℝ))
    (hΔ : |Δ| ≤ L) (hv : |a * v| ≤ T) (hsmall : L + T < 1) :
    |v| ≤ (2 * M / k) * L := by
…

theorem OAI.QuantitativeVanDerWaerden.short_cut_interval_lt_step line 69

Source documentation

A discrete nonzero step makes every cut-near adaptive interval narrower than one step.

theorem short_cut_interval_lt_step {H k ρ α width w : ℝ}
    (hH : 0 ≤ H) (hw : w ≠ 0) (hα : α ≤ |w|) (hρ : ρ ≤ k * |w|)
    (hwidth : width ≤ 2 * H * (ρ + α)) (hsmall : 2 * H * (k + 1) < 1) :
    width < |w| := by
…

theorem OAI.QuantitativeVanDerWaerden.abs_nat_difference_ge_one line 83

theorem OAI.QuantitativeVanDerWaerden.short_step_not_same_interval line 95

Source documentation

Distinct samples of a short nonzero real step cannot occupy an interval narrower than the step, even if their representatives cross the cut.

theorem short_step_not_same_interval {a b k : ℕ} {za zb w : ℝ}
    (hab : a ≠ b) (hak : a < k) (hbk : b < k)
    (hmotion : (k : ℝ) * |w| < 1 / 2)
    (hint : ∃ z : ℤ, (za - zb) - ((a : ℝ) - b) * w = (z : ℝ))
    (hnarrow : |za - zb| < |w|) : False := by
…