AffineGridArithmetic.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Alignment of dyadic affine images with basic intervals

A slope which is an integer power of two sends every sufficiently fine grid cell to a single grid cell, provided its dyadic translation has been absorbed into the target denominator. The target depth can be made arbitrarily large.

theorem OAI.ThompsonNonamenability.basicInterval_of_integer_grid line 18

Source documentation

An integer grid cell lying in the unit interval is a basic interval.

theorem basicInterval_of_integer_grid (d : ℕ) (j : ℤ)
    (h0 : 0 ≤ (j : ℝ) / (2 : ℝ) ^ d)
    (h1 : ((j : ℝ) + 1) / (2 : ℝ) ^ d ≤ 1) :
    ∃ I : BasicInterval, I.depth = d ∧
      I.left = (j : ℝ) / (2 : ℝ) ^ d ∧
      I.right = ((j : ℝ) + 1) / (2 : ℝ) ^ d := by
…

Mentions: OAI.ThompsonNonamenability.BasicInterval

theorem OAI.ThompsonNonamenability.dyadic_affine_aligned_denominators line 45
Source documentation
The target denominator simultaneously absorbs the translation and slope. The freely specified lower bound on target depth gives arbitrarily small cells.
```
theorem dyadic_affine_aligned_denominators (q : ℤ) (b : ℝ)
    (hb : IsDyadic b) (L : ℕ) :
    ∃ N : ℕ, ∀ n ≥ N, ∃ d : ℕ, L ≤ d ∧
      (∃ j : ℤ, b = (j : ℝ) / (2 : ℝ) ^ d) ∧
      (2 : ℝ) ^ q / (2 : ℝ) ^ n = 1 / (2 : ℝ) ^ d := by
…
```
Mentions: OAI.ThompsonNonamenability.IsDyadic

theorem OAI.ThompsonNonamenability.dyadic_affine_cell_of_denominator line 73

Source documentation

A single cell is aligned when the slope and translation share the target grid denominator. No assumption about the source cell's location is needed.

theorem dyadic_affine_cell_of_denominator (q : ℤ) (b : ℝ) (n d : ℕ)
    (hb : ∃ j : ℤ, b = (j : ℝ) / (2 : ℝ) ^ d)
    (hs : (2 : ℝ) ^ q / (2 : ℝ) ^ n = 1 / (2 : ℝ) ^ d)
    (k : Fin (2 ^ n))
    (h0 : 0 ≤ (2 : ℝ) ^ q * ((k.val : ℝ) / (2 : ℝ) ^ n) + b)
    (h1 : (2 : ℝ) ^ q * (((k.val : ℝ) + 1) / (2 : ℝ) ^ n) + b ≤ 1) :
    ∃ I : BasicInterval, I.depth = d ∧
      I.left = (2 : ℝ) ^ q * ((k.val : ℝ) / (2 : ℝ) ^ n) + b ∧
      I.right = (2 : ℝ) ^ q * (((k.val : ℝ) + 1) / (2 : ℝ) ^ n) + b := by
…

Mentions: OAI.ThompsonNonamenability.BasicInterval

theorem OAI.ThompsonNonamenability.dyadic_affine_grid_alignment line 103

Source documentation

Every sufficiently fine cell has a basic interval as its dyadic affine image whenever that image lies in [0,1].

theorem dyadic_affine_grid_alignment (q : ℤ) (b : ℝ) (hb : IsDyadic b) :
    ∃ N : ℕ, ∀ n ≥ N, ∀ k : Fin (2 ^ n),
      0 ≤ (2 : ℝ) ^ q * ((k.val : ℝ) / (2 : ℝ) ^ n) + b →
      (2 : ℝ) ^ q * (((k.val : ℝ) + 1) / (2 : ℝ) ^ n) + b ≤ 1 →
      ∃ I : BasicInterval,
        I.left = (2 : ℝ) ^ q * ((k.val : ℝ) / (2 : ℝ) ^ n) + b ∧
        I.right = (2 : ℝ) ^ q * (((k.val : ℝ) + 1) / (2 : ℝ) ^ n) + b := by
…

Mentions: OAI.ThompsonNonamenability.IsDyadic, OAI.ThompsonNonamenability.BasicInterval

theorem OAI.ThompsonNonamenability.dyadic_affine_grid_alignment_small line 119

Source documentation

The affine image cells can simultaneously be required to have any prescribed positive upper bound on their length.

theorem dyadic_affine_grid_alignment_small (q : ℤ) (b : ℝ) (hb : IsDyadic b)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ N : ℕ, ∀ n ≥ N, ∀ k : Fin (2 ^ n),
      0 ≤ (2 : ℝ) ^ q * ((k.val : ℝ) / (2 : ℝ) ^ n) + b →
      (2 : ℝ) ^ q * (((k.val : ℝ) + 1) / (2 : ℝ) ^ n) + b ≤ 1 →
      ∃ I : BasicInterval,
        I.left = (2 : ℝ) ^ q * ((k.val : ℝ) / (2 : ℝ) ^ n) + b ∧
        I.right = (2 : ℝ) ^ q * (((k.val : ℝ) + 1) / (2 : ℝ) ^ n) + b ∧
        I.length < ε := by
…

Mentions: OAI.ThompsonNonamenability.IsDyadic, OAI.ThompsonNonamenability.BasicInterval