UniformPartition.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Uniform dyadic partitions

The depth-n partition consists of all 2^n basic intervals at that depth. Coverage includes both endpoints of the unit interval. Distinct cells have disjoint open interiors; their closed carriers may share an endpoint.

def OAI.ThompsonNonamenability.BasicPartition.uniformCell line 24
Source documentation
The cell with index k in the depth-n uniform dyadic partition.
```
def uniformCell (n : ℕ) (k : Fin (2 ^ n)) : BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCell_depth line 27
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCell_index line 30
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCell_injective line 33
def OAI.ThompsonNonamenability.BasicPartition.uniformCells line 39
Source documentation
All cells at depth n, with no repeated intervals.
```
def uniformCells (n : ℕ) : Finset BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.mem_uniformCells line 42
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCell_mem_uniformCells line 46
theorem OAI.ThompsonNonamenability.BasicPartition.card_uniformCells line 50
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCell_disjoint line 54
Source documentation
At a fixed depth, the interiors of distinct cells are disjoint.
```
theorem uniformCell_disjoint {n : ℕ} {i j : Fin (2 ^ n)} (hij : i ≠ j) :
    Disjoint (uniformCell n i).interior (uniformCell n j).interior := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition.uniformCell
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCells_cover line 79
Source documentation
Every point of [0,1] lies in one of the closed depth-n cells.
```
theorem uniformCells_cover (n : ℕ) (x : ℝ) (hx : x ∈ Icc (0 : ℝ) 1) :
    ∃ I ∈ uniformCells n, x ∈ I.carrier := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition.uniformCells
def OAI.ThompsonNonamenability.BasicPartition.uniform line 113
Source documentation
The genuine partition into all depth-n dyadic cells.
```
def uniform (n : ℕ) : BasicPartition where
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition
theorem OAI.ThompsonNonamenability.BasicPartition.uniform_cells line 124
theorem OAI.ThompsonNonamenability.BasicPartition.uniform_cellCount line 126
theorem OAI.ThompsonNonamenability.BasicPartition.uniformCell_length line 129
theorem OAI.ThompsonNonamenability.BasicPartition.uniform_depth line 132
theorem OAI.ThompsonNonamenability.BasicPartition.uniform_length line 138
Source documentation
All cells in the uniform partition have the same positive length.
```
theorem uniform_length {n : ℕ} {I : BasicInterval} (hI : I ∈ (uniform n).cells) :
    I.length = ((2 : ℝ) ^ n)⁻¹ := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.BasicPartition.uniform
theorem OAI.ThompsonNonamenability.BasicPartition.uniform_respects_of_depth_le line 144
Source documentation
A uniform grid respects every basic interval resolved at its depth.
```
theorem uniform_respects_of_depth_le (n : ℕ) (I : BasicInterval)
    (hI : I.depth ≤ n) : (uniform n).Respects I := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.BasicPartition.uniform, OAI.ThompsonNonamenability.BasicPartition.Respects