SmallBoxAffinity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Affinity of representatives inside a small box

The input is the integer-valued cross difference of three representatives of an arithmetic progression modulo one. A box of width 2 * H makes this integer strictly smaller than one in absolute value, so it vanishes. Interpolation then produces one real affine lift on all selected indices.

theorem OAI.QuantitativeVanDerWaerden.integer_zero_of_abs_lt_one line 24
Source documentation
An integer whose real absolute value is less than one vanishes.
```
theorem integer_zero_of_abs_lt_one {m : ℤ} (h : |(m : ℝ)| < 1) : m = 0 := by
…
```

theorem OAI.QuantitativeVanDerWaerden.triple_integral_of_integer_errors line 30

Source documentation

Integer errors in affine representatives imply an integer cross difference. No ordering assumption on the three indices is needed here.

theorem triple_integral_of_integer_errors {z : ℕ → ℝ} {A B : ℝ}
    (h : ∀ j, ∃ m : ℤ, z j - A - (j : ℝ) * B = (m : ℝ))
    (a b c : ℕ) :
    ∃ m : ℤ, ((c : ℝ) - b) * (z b - z a) -
      ((b : ℝ) - a) * (z c - z b) = (m : ℝ) := by
…

theorem OAI.QuantitativeVanDerWaerden.abs_cross_difference_lt_one line 47

Source documentation

The cross difference of three points in a short real interval is small.

theorem abs_cross_difference_lt_one {k a b c : ℕ} {H : ℝ} {z : ℕ → ℝ}
    (hab : a < b) (hbc : b < c) (hck : c < k)
    (hH : 0 ≤ H) (hsmall : 2 * (k : ℝ) * H < 1)
    (habox : |z b - z a| ≤ 2 * H) (hbbox : |z c - z b| ≤ 2 * H) :
    |((c : ℝ) - b) * (z b - z a) -
      ((b : ℝ) - a) * (z c - z b)| < 1 := by
…

theorem OAI.QuantitativeVanDerWaerden.cross_difference_eq_zero_of_small_box line 73

Source documentation

In a small box, the integral cross difference is exactly zero.

theorem cross_difference_eq_zero_of_small_box {k a b c : ℕ} {H : ℝ}
    {z : ℕ → ℝ} (hab : a < b) (hbc : b < c) (hck : c < k)
    (hH : 0 ≤ H) (hsmall : 2 * (k : ℝ) * H < 1)
    (habox : |z b - z a| ≤ 2 * H) (hbbox : |z c - z b| ≤ 2 * H)
    (hint : ∃ m : ℤ, ((c : ℝ) - b) * (z b - z a) -
      ((b : ℝ) - a) * (z c - z b) = (m : ℝ)) :
    ((c : ℝ) - b) * (z b - z a) -
      ((b : ℝ) - a) * (z c - z b) = 0 := by
…

theorem OAI.QuantitativeVanDerWaerden.exists_affine_of_cross_difference_eq_zero line 89

Source documentation

Vanishing cross differences on ordered triples give one affine interpolation on a finite set, including the empty and singleton cases.

theorem exists_affine_of_cross_difference_eq_zero (J : Finset ℕ) (z : ℕ → ℝ)
    (hcross : ∀ a ∈ J, ∀ b ∈ J, ∀ c ∈ J, a < b → b < c →
      ((c : ℝ) - b) * (z b - z a) -
        ((b : ℝ) - a) * (z c - z b) = 0) :
    ∃ A B : ℝ, ∀ j ∈ J, z j = A + (j : ℝ) * B := by
…

theorem OAI.QuantitativeVanDerWaerden.exists_affine_of_small_box line 141

Source documentation

Scalar affinity inside a box of width 2 * H. The integer premise is the explicit consequence of arithmetic progression modulo one.

theorem exists_affine_of_small_box {k : ℕ} {H : ℝ}
    (J : Finset ℕ) (z : ℕ → ℝ) (hJ : ∀ j ∈ J, j < k)
    (hH : 0 ≤ H) (hsmall : 2 * (k : ℝ) * H < 1)
    (hbox : ∀ i ∈ J, ∀ j ∈ J, |z j - z i| ≤ 2 * H)
    (hint : ∀ a ∈ J, ∀ b ∈ J, ∀ c ∈ J, a < b → b < c →
      ∃ m : ℤ, ((c : ℝ) - b) * (z b - z a) -
        ((b : ℝ) - a) * (z c - z b) = (m : ℝ)) :
    ∃ A B : ℝ, ∀ j ∈ J, z j = A + (j : ℝ) * B := by
…

theorem OAI.QuantitativeVanDerWaerden.exists_affine_of_small_box_vector line 156

Source documentation

The coordinatewise form gives a single real affine vector lift. In the application the coordinate type is Fin D (or two copies of Fin D).

theorem exists_affine_of_small_box_vector {ι : Type uIndex} {k : ℕ} {H : ℝ}
    (J : Finset ℕ) (z : ℕ → ι → ℝ) (hJ : ∀ j ∈ J, j < k)
    (hH : 0 ≤ H) (hsmall : 2 * (k : ℝ) * H < 1)
    (hbox : ∀ i ∈ J, ∀ j ∈ J, ∀ d, |z j d - z i d| ≤ 2 * H)
    (hint : ∀ a ∈ J, ∀ b ∈ J, ∀ c ∈ J, a < b → b < c → ∀ d,
      ∃ m : ℤ, ((c : ℝ) - b) * (z b d - z a d) -
        ((b : ℝ) - a) * (z c d - z b d) = (m : ℝ)) :
    ∃ A B : ι → ℝ, ∀ j ∈ J, ∀ d, z j d = A d + (j : ℝ) * B d := by
…