GridGeometry.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.periodicGridKey line 9
Source documentation
The integer label of the half-open periodic grid cell containing a point.
```
def periodicGridKey (q x : ℝ) : ℤ := ⌊q * Int.fract x⌋
```
theorem OAI.Problem310.periodicGridKey_ne_of_separated line 13
Source documentation
Two points separated from each other in both directions around the circle cannot occupy the same cell of a periodic grid.
```
theorem periodicGridKey_ne_of_separated {q x y : ℝ} (hq : 2 ≤ q)
    (hlo : q⁻¹ ≤ y - x) (hhi : y - x ≤ 1 - q⁻¹) :
    periodicGridKey q x ≠ periodicGridKey q y := by
…
```
Mentions: OAI.Problem310.periodicGridKey
theorem OAI.Problem310.periodicGridKey_eq_emod line 48
Source documentation
The periodic label is the residue of the label on the real-line grid.
```
theorem periodicGridKey_eq_emod (q : ℕ) (hq : 0 < q) (x : ℝ) :
    periodicGridKey q x = ⌊(q : ℝ) * x⌋ % (q : ℤ) := by
…
```
Mentions: OAI.Problem310.periodicGridKey
theorem OAI.Problem310.periodicGridKey_eq_of_no_crossing line 61
Source documentation
Absence of a real-line grid boundary between ordered points preserves keys. The interval is open at its left end, so a center on a boundary is allowed.
```
theorem periodicGridKey_eq_of_no_crossing (q : ℕ) (hq : 0 < q) {x y : ℝ}
    (hxy : x ≤ y) (hcross : ∀ k : ℤ, (k : ℝ) / q ∉ Set.Ioc x y) :
    periodicGridKey q x = periodicGridKey q y := by
…
```
Mentions: OAI.Problem310.periodicGridKey
def OAI.Problem310.dyadicGridKey line 84
Source documentation
Periodic cells used for a dyadic window with last index b.
```
def dyadicGridKey (b : ℕ) (x : ℝ) : ℤ := periodicGridKey ((2 : ℝ) ^ (b + 2)) x
```
Mentions: OAI.Problem310.periodicGridKey
theorem OAI.Problem310.dyadicGridKey_add_one line 86
theorem OAI.Problem310.dyadicGridKey_nonneg line 90
theorem OAI.Problem310.dyadicGridKey_lt line 94
theorem OAI.Problem310.dyadicGridKey_nested line 101
Source documentation
Fine dyadic grid labels determine all coarser labels by integer division.
```
theorem dyadicGridKey_nested {b B : ℕ} (hb : b ≤ B) (x : ℝ) :
    dyadicGridKey B x / (2 : ℤ) ^ (B - b) = dyadicGridKey b x := by
…
```
Mentions: OAI.Problem310.dyadicGridKey
theorem OAI.Problem310.dyadicGridKey_ne_of_coarse_ne line 114
theorem OAI.Problem310.half_pow_antitone line 121
theorem OAI.Problem310.grid_resolution_bound line 124
theorem OAI.Problem310.grid_width_eq line 129

theorem OAI.Problem310.dyadicGridKey_center_ne line 134

Source documentation

The center and any requested point in a window occupy different cells.

theorem dyadicGridKey_center_ne {a b n : ℕ} {x t : ℝ}
    (ha : 3 ≤ a) (han : a ≤ n) (hnb : n ≤ b)
    (ht : t ∈ Set.Icc (1 : ℝ) 2) :
    dyadicGridKey b x ≠ dyadicGridKey b (x + t * ((2 : ℝ)⁻¹) ^ n) := by
…

Mentions: OAI.Problem310.dyadicGridKey

theorem OAI.Problem310.dyadicGridKey_pair_ne line 151

Source documentation

Different indices in a window supply different selector addresses.

theorem dyadicGridKey_pair_ne {a b n m : ℕ} {x t : ℝ}
    (ha : 3 ≤ a) (han : a ≤ n) (hnm : n < m) (hmb : m ≤ b)
    (ht : t ∈ Set.Icc (1 : ℝ) 2) :
    dyadicGridKey b (x + t * ((2 : ℝ)⁻¹) ^ m) ≠
      dyadicGridKey b (x + t * ((2 : ℝ)⁻¹) ^ n) := by
…

Mentions: OAI.Problem310.dyadicGridKey

theorem OAI.Problem310.dyadicGridKey_eq_of_stable line 177

Source documentation

The no-crossing stability condition for a later window preserves an earlier key.

theorem dyadicGridKey_eq_of_stable {a b n : ℕ} {x t : ℝ}
    (han : a ≤ n) (ht : t ∈ Set.Icc (1 : ℝ) 2)
    (hstable : ∀ k : ℤ, (k : ℝ) / (2 : ℝ) ^ (b + 2) ∉
      Set.Ioc x (x + 2 * ((2 : ℝ)⁻¹) ^ a)) :
    dyadicGridKey b (x + t * ((2 : ℝ)⁻¹) ^ n) = dyadicGridKey b x := by
…

Mentions: OAI.Problem310.dyadicGridKey

theorem OAI.Problem310.dyadicGridKey_injOn_window line 198

Source documentation

All the trial addresses in one dyadic window are distinct.

theorem dyadicGridKey_injOn_window {a b : ℕ} {x t : ℝ}
    (ha : 3 ≤ a) (ht : t ∈ Set.Icc (1 : ℝ) 2) :
    Set.InjOn (fun n : ℕ ↦ dyadicGridKey b (x + t * ((2 : ℝ)⁻¹) ^ n))
      (Set.Icc a b) := by
…

Mentions: OAI.Problem310.dyadicGridKey