UniformPL.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Resolving a finite dyadic PL subdivision on a uniform grid

All original knots lie on a sufficiently fine dyadic grid. Such a knot cannot lie strictly between consecutive grid points. The source piece containing a cell's midpoint therefore contains the whole closed cell.

def OAI.ThompsonNonamenability.uniformDyadicPoint line 24
Source documentation
A point on the closed depth-n dyadic grid, including both endpoints.
```
def uniformDyadicPoint (n : ℕ) (j : Fin (2 ^ n + 1)) : UnitInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.UnitInterval
theorem OAI.ThompsonNonamenability.coe_uniformDyadicPoint line 31
theorem OAI.ThompsonNonamenability.uniformDyadicPoint_castSucc_coe line 34
theorem OAI.ThompsonNonamenability.uniformDyadicPoint_succ_coe line 37
theorem OAI.ThompsonNonamenability.uniformDyadicPoint_strictMono line 43
theorem OAI.ThompsonNonamenability.uniformDyadicPoint_zero line 50
theorem OAI.ThompsonNonamenability.uniformDyadicPoint_last line 55
theorem OAI.ThompsonNonamenability.uniformDyadicPoint_dyadic line 60

theorem OAI.ThompsonNonamenability.grid_point_not_inside_uniform_cell line 65

Source documentation

There is no grid point strictly between consecutive grid points.

theorem grid_point_not_inside_uniform_cell (n : ℕ) (k : Fin (2 ^ n)) (j : ℤ) :
    ¬ ((uniformCell n k).left < (j : ℝ) / (2 : ℝ) ^ n ∧
      (j : ℝ) / (2 : ℝ) ^ n < (uniformCell n k).right) := by
…

theorem OAI.ThompsonNonamenability.DyadicPLWitness.eventually_uniform_refines line 82
Source documentation
A single grid depth resolves every knot of the original subdivision. At all larger depths each closed grid cell lies in one original piece.
```
theorem eventually_uniform_refines {f : IntervalHomeomorph} (w : DyadicPLWitness f) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ k : Fin (2 ^ n),
      ∃ i : Fin w.pieceCount,
        w.knots i.castSucc ≤ uniformDyadicPoint n k.castSucc ∧
        uniformDyadicPoint n k.succ ≤ w.knots i.succ := by
…
```
Mentions: OAI.ThompsonNonamenability.IntervalHomeomorph, OAI.ThompsonNonamenability.DyadicPLWitness, OAI.ThompsonNonamenability.uniformDyadicPoint
structure OAI.ThompsonNonamenability.UniformDyadicPLWitness line 124
Source documentation
A genuine affine formula on every closed cell of one uniform subdivision.
```
structure UniformDyadicPLWitness (f : IntervalHomeomorph) (n : ℕ) where
…
```
Mentions: OAI.ThompsonNonamenability.IntervalHomeomorph
def OAI.ThompsonNonamenability.DyadicPLWitness.uniformOfRefines line 135
Source documentation
Restricting an original affine piece to a contained grid cell preserves its exact exponent; the translation is rebased at the new left endpoint.
```
def uniformOfRefines {f : IntervalHomeomorph} (w : DyadicPLWitness f) (n : ℕ)
    (hr : ∀ k : Fin (2 ^ n), ∃ i : Fin w.pieceCount,
      w.knots i.castSucc ≤ uniformDyadicPoint n k.castSucc ∧
      uniformDyadicPoint n k.succ ≤ w.knots i.succ) : UniformDyadicPLWitness f n where
…
```
Mentions: OAI.ThompsonNonamenability.IntervalHomeomorph, OAI.ThompsonNonamenability.DyadicPLWitness, OAI.ThompsonNonamenability.uniformDyadicPoint, OAI.ThompsonNonamenability.UniformDyadicPLWitness
theorem OAI.ThompsonNonamenability.DyadicPLWitness.eventually_uniform_affine line 160
def OAI.ThompsonNonamenability.UniformDyadicPLWitness.toDyadicPLWitness line 170
Source documentation
Uniform affine data is an ordinary finite dyadic PL subdivision.
```
def toDyadicPLWitness {f : IntervalHomeomorph} {n : ℕ}
    (w : UniformDyadicPLWitness f n) : DyadicPLWitness f where
…
```
Mentions: OAI.ThompsonNonamenability.IntervalHomeomorph, OAI.ThompsonNonamenability.UniformDyadicPLWitness, OAI.ThompsonNonamenability.DyadicPLWitness
theorem OAI.ThompsonNonamenability.hasDyadicPLPieces_iff_uniform line 199