DyadicGapPartition.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Partitions of positive dyadic gaps

The initial partition consists of consecutive cells of a common dyadic grid. Splitting one cell gives exactly one additional cell. Thus each pair of gaps can be partitioned into the same number of cells independently.

def OAI.ThompsonNonamenability.uniformGapCells line 20
Source documentation
Consecutive cells with indices A, ..., A+c-1 on grid level n.
```
def uniformGapCells (n A c : ℕ) (h : A + c ≤ 2 ^ n) : List BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.uniformGapCells_length line 28
theorem OAI.ThompsonNonamenability.uniformGapCells_chain line 34
theorem OAI.ThompsonNonamenability.exists_dyadicGapPartition line 46
Source documentation
An actual basic-cell partition of any positive dyadic subinterval.
```
theorem exists_dyadicGapPartition {a b : ℝ}
    (ha : IsDyadic a) (hb : IsDyadic b)
    (h0 : 0 ≤ a) (hab : a < b) (h1 : b ≤ 1) :
    Nonempty (DyadicGapPartition a b) := by
…
```
Mentions: OAI.ThompsonNonamenability.IsDyadic, OAI.ThompsonNonamenability.DyadicGapPartition
def OAI.ThompsonNonamenability.BasicInterval.splitLeft line 78
Source documentation
The left half of an actual basic interval.
```
def splitLeft (I : BasicInterval) : BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
def OAI.ThompsonNonamenability.BasicInterval.splitRight line 82
Source documentation
The right half of an actual basic interval.
```
def splitRight (I : BasicInterval) : BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicInterval.splitLeft_left line 85
theorem OAI.ThompsonNonamenability.BasicInterval.splitRight_right line 91
theorem OAI.ThompsonNonamenability.BasicInterval.split_adjacent line 97
theorem OAI.ThompsonNonamenability.BasicInterval.splitLeft_contained line 102
theorem OAI.ThompsonNonamenability.BasicInterval.splitRight_contained line 105
def OAI.ThompsonNonamenability.GapRefines line 111
Source documentation
Every cell in the refined list lies in an original cell.
```
def GapRefines (newCells oldCells : List BasicInterval) : Prop :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.GapRefines.refl line 116
theorem OAI.ThompsonNonamenability.GapRefines.trans line 120
theorem OAI.ThompsonNonamenability.GapChain.split_head line 131
theorem OAI.ThompsonNonamenability.GapChain.split_head_refines line 138
theorem OAI.ThompsonNonamenability.GapChain.exists_succ_length line 148
Source documentation
Bisection increases a nonempty chain's cardinality by exactly one.
```
theorem exists_succ_length {a b : ℝ} {L : List BasicInterval}
    (h : GapChain a b L) (hne : L ≠ []) :
    ∃ M : List BasicInterval, GapChain a b M ∧
      M.length = L.length + 1 ∧ GapRefines M L := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain, OAI.ThompsonNonamenability.GapRefines
theorem OAI.ThompsonNonamenability.GapChain.exists_length_add line 159
Source documentation
Any prescribed nonnegative number of extra cells can be obtained by bisection.
```
theorem exists_length_add {a b : ℝ} {L : List BasicInterval}
    (h : GapChain a b L) (hne : L ≠ []) (k : ℕ) :
    ∃ M : List BasicInterval, GapChain a b M ∧
      M.length = L.length + k ∧ GapRefines M L := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain, OAI.ThompsonNonamenability.GapRefines
theorem OAI.ThompsonNonamenability.GapChain.exists_length_ge line 175
theorem OAI.ThompsonNonamenability.DyadicGapPartition.exists_refinement_card line 185

theorem OAI.ThompsonNonamenability.DyadicGapPartition.equalize line 197

Source documentation

Equalization is performed for this pair of gaps, with both refinements retained.

theorem equalize {a b c d : ℝ} (P : DyadicGapPartition a b) (Q : DyadicGapPartition c d) :
    ∃ (P' : DyadicGapPartition a b) (Q' : DyadicGapPartition c d),
      P'.cells.length = Q'.cells.length ∧
      GapRefines P'.cells P.cells ∧ GapRefines Q'.cells Q.cells := by
…

Mentions: OAI.ThompsonNonamenability.DyadicGapPartition, OAI.ThompsonNonamenability.GapRefines

theorem OAI.ThompsonNonamenability.equalize_dyadic_gaps line 208

Source documentation

Any two positive dyadic gaps admit ordered basic-cell chains of equal length.

theorem equalize_dyadic_gaps {a b c d : ℝ}
    (ha : IsDyadic a) (hb : IsDyadic b) (h0 : 0 ≤ a) (hab : a < b) (h1 : b ≤ 1)
    (hc : IsDyadic c) (hd : IsDyadic d) (h0' : 0 ≤ c) (hcd : c < d) (h1' : d ≤ 1) :
    ∃ A B : List BasicInterval, GapChain a b A ∧ GapChain c d B ∧
      A ≠ [] ∧ B ≠ [] ∧ A.length = B.length := by
…

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

theorem OAI.ThompsonNonamenability.exists_equal_length_partitions line 218