BasicIntervalNesting.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Nesting and normalization of basic dyadic intervals

The endpoint comparisons are made on a common dyadic grid. In particular, intersecting open interiors force one basic interval to contain the other.

theorem OAI.ThompsonNonamenability.BasicInterval.left_eq_on_finer_grid line 19
Source documentation
Express a left endpoint on any finer dyadic grid.
```
theorem left_eq_on_finer_grid (I : BasicInterval) {s : ℕ} (h : I.depth ≤ s) :
    I.left = ((I.index.val * 2 ^ (s - I.depth) : ℕ) : ℝ) / (2 : ℝ) ^ s := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicInterval.right_eq_on_finer_grid line 29
Source documentation
Express a right endpoint on any finer dyadic grid.
```
theorem right_eq_on_finer_grid (I : BasicInterval) {s : ℕ} (h : I.depth ≤ s) :
    I.right = (((I.index.val + 1) * 2 ^ (s - I.depth) : ℕ) : ℝ) /
      (2 : ℝ) ^ s := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicInterval.depth_le_of_contained line 41
Source documentation
A contained basic interval has at least the depth of its container.
```
theorem depth_le_of_contained {I K : BasicInterval} (h : K.Contained I) :
    I.depth ≤ K.depth := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval

theorem OAI.ThompsonNonamenability.BasicInterval.index_bounds_of_contained line 50

Source documentation

Containment gives the integer endpoint bounds on the finer grid.

theorem index_bounds_of_contained {I K : BasicInterval} (h : K.Contained I) :
    I.index.val * 2 ^ (K.depth - I.depth) ≤ K.index.val ∧
      K.index.val + 1 ≤ (I.index.val + 1) * 2 ^ (K.depth - I.depth) := by
…

Mentions: OAI.ThompsonNonamenability.BasicInterval

theorem OAI.ThompsonNonamenability.BasicInterval.contained_iff_exists_comp line 65
Source documentation
A subinterval is precisely the image of a basic interval under the container's affine chart.
```
theorem contained_iff_exists_comp {I K : BasicInterval} :
    K.Contained I ↔ ∃ J : BasicInterval, I.comp J = K := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicInterval.contained_iff_exists_unique_comp line 87
Source documentation
The affine preimage of a contained basic interval is unique.
```
theorem contained_iff_exists_unique_comp {I K : BasicInterval} :
    K.Contained I ↔ ∃! J : BasicInterval, I.comp J = K := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
def OAI.ThompsonNonamenability.BasicInterval.normalize line 101
Source documentation
The basic interval obtained by applying the inverse chart of I to K.
```
def normalize (I K : BasicInterval) (h : K.Contained I) : BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicInterval.comp_normalize line 104
theorem OAI.ThompsonNonamenability.BasicInterval.normalize_comp line 108
theorem OAI.ThompsonNonamenability.BasicInterval.contained_of_overlap_of_depth_le line 114
Source documentation
At ordered depths, overlap of open interiors implies containment.
```
theorem contained_of_overlap_of_depth_le {I K : BasicInterval}
    (hd : I.depth ≤ K.depth) (h : (I.interior ∩ K.interior).Nonempty) :
    K.Contained I := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicInterval.overlap_interior_nested line 138
Source documentation
Basic dyadic intervals with intersecting open interiors are nested.
```
theorem overlap_interior_nested {I J : BasicInterval}
    (h : (I.interior ∩ J.interior).Nonempty) : I.Contained J ∨ J.Contained I := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval