Lattice.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RuledApproximation.nearestInteger line 13
Source documentation
Rounding convention: half-integers are rounded upwards.
```
def nearestInteger (t : ℝ) : ℤ := ⌊t + 1 / 2⌋
```
lemma OAI.RuledApproximation.nearestInteger_mono line 15
lemma OAI.RuledApproximation.nearestInteger_error line 19
lemma OAI.RuledApproximation.integer_fixed_point_of_bounded_drift line 28
Source documentation
An integer version of the monotone fixed-point argument. The bounded drift with slope strictly less than one supplies both end barriers.
```
lemma integer_fixed_point_of_bounded_drift (F : ℤ → ℤ) (hF : Monotone F)
    (q B : ℝ) (hq : q < 1) (hB : ∀ i : ℤ, |(F i : ℝ) - q * i| ≤ B) :
    ∃ i : ℤ, F i = i := by
…
```

theorem OAI.RuledApproximation.asymmetric_lattice_cover line 52

Source documentation

A useful strengthening of the lattice estimates: only the product conditions are needed; either off-diagonal entry may be arbitrarily large.

theorem asymmetric_lattice_cover (alpha beta : ℝ)
    (hprod : 0 ≤ alpha * beta) (hprod' : alpha * beta < 1) (u₁ u₂ : ℝ) :
    ∃ i j : ℤ, |u₁ - ((i : ℝ) + alpha * j)| ≤ 1 / 2 ∧
      |u₂ - (beta * i + (j : ℝ))| ≤ 1 / 2 := by
…

lemma OAI.RuledApproximation.symmetric_lattice_distance line 110

theorem OAI.RuledApproximation.lattice_covering line 133

Source documentation

Lattice covering with a uniform distance estimate.

theorem lattice_covering (a : ℝ) (ha : |a| < 1) (z₁ z₂ : ℝ) :
    ∃ i j : ℤ,
      |(z₁ - i) + a * (z₂ - j)| ≤ 1 / 2 ∧
      |(z₂ - j) + a * (z₁ - i)| ≤ 1 / 2 ∧
      max |z₁ - i| |z₂ - j| ≤ 1 / (2 * (1 - |a|)) := by
…

theorem OAI.RuledApproximation.sliding_rows_cover line 152

Source documentation

Sliding rows have no shear bound. This is the local nilpotent model.

theorem sliding_rows_cover (d : ℝ) (u₁ u₂ : ℝ) :
    ∃ i j : ℤ, |u₁ - ((i : ℝ) + d * j)| ≤ 1 / 2 ∧
      |u₂ - (j : ℝ)| ≤ 1 / 2 := by
…