DyadicGapChain.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Consecutive dyadic cells

A chain is an ordered list of actual basic intervals whose consecutive endpoints agree. Its endpoints and coverage are proved from this data.

def OAI.ThompsonNonamenability.GapChain line 18
Source documentation
A finite list of consecutive cells starts at a and ends at b. The empty list represents a gap of length zero.
```
def GapChain : ℝ → ℝ → List BasicInterval → Prop
  | a, b, [] => a = b
  | a, b, I :: L => I.left = a ∧ GapChain I.right b L

namespace GapChain
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.GapChain.nil_iff line 24
theorem OAI.ThompsonNonamenability.GapChain.cons_iff line 26
theorem OAI.ThompsonNonamenability.GapChain.singleton line 29
theorem OAI.ThompsonNonamenability.GapChain.singleton_iff line 32
theorem OAI.ThompsonNonamenability.GapChain.append line 35
theorem OAI.ThompsonNonamenability.GapChain.le_endpoints line 45
theorem OAI.ThompsonNonamenability.GapChain.lt_endpoints_of_ne_nil line 55
theorem OAI.ThompsonNonamenability.GapChain.ne_nil_of_lt_endpoints line 65
theorem OAI.ThompsonNonamenability.GapChain.left_le_of_mem line 71
theorem OAI.ThompsonNonamenability.GapChain.right_le_of_mem line 83
theorem OAI.ThompsonNonamenability.GapChain.carrier_subset line 92
theorem OAI.ThompsonNonamenability.GapChain.pairwise line 99
Source documentation
Cells later in the chain start no earlier than the current cell ends.
```
theorem pairwise {a b : ℝ} {L : List BasicInterval} (h : GapChain a b L) :
    L.Pairwise (fun I J => I.right ≤ J.left) := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain
theorem OAI.ThompsonNonamenability.GapChain.mem_carrier_iff line 108
Source documentation
A nonempty chain covers exactly its closed endpoint interval.
```
theorem mem_carrier_iff {a b : ℝ} {L : List BasicInterval}
    (h : GapChain a b L) (hL : L ≠ []) (x : ℝ) :
    (∃ I ∈ L, x ∈ I.carrier) ↔ a ≤ x ∧ x ≤ b := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain
structure OAI.ThompsonNonamenability.DyadicGapPartition line 132
Source documentation
A nonempty ordered partition of an actual interval by basic dyadic cells.
```
structure DyadicGapPartition (a b : ℝ) where
…
```
theorem OAI.ThompsonNonamenability.DyadicGapPartition.left_lt_right line 139
theorem OAI.ThompsonNonamenability.DyadicGapPartition.mem_covered_iff line 142
theorem OAI.ThompsonNonamenability.DyadicGapPartition.cell_bounds line 146