OAI/GroupTheory/Thompson/DyadicImages.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThompsonNonamenability.ImageBasic line 15

   Source documentation

   Every actual image of a depth-n uniform cell is a basic interval.

   def ImageBasic (g : F) (n : ℕ) : Prop :=
   …

   Mentions: OAI.ThompsonNonamenability.F

2. def OAI.ThompsonNonamenability.imageCell line 21

   Source documentation

   The unique basic interval with the actual image endpoints.

   def imageCell (g : F) (n : ℕ) (hg : ImageBasic g n) (k : Fin (2 ^ n)) :
       BasicInterval := Classical.choose (hg k)

   Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.ImageBasic, OAI.ThompsonNonamenability.BasicInterval

3. theorem OAI.ThompsonNonamenability.imageCell_left line 24
4. theorem OAI.ThompsonNonamenability.imageCell_right line 29
5. theorem OAI.ThompsonNonamenability.imageCell_proof_irrel line 34
6. theorem OAI.ThompsonNonamenability.imageCell_mem_carrier_iff line 38
7. theorem OAI.ThompsonNonamenability.imageCell_mem_interior_iff line 50
8. theorem OAI.ThompsonNonamenability.imageCell_injective line 62
9. def OAI.ThompsonNonamenability.imagePartition line 77

   Source documentation

   The actual images, with coverage and disjoint open interiors proved.

   def imagePartition (g : F) (n : ℕ) (hg : ImageBasic g n) : BasicPartition where
   …

   Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.ImageBasic, OAI.ThompsonNonamenability.BasicPartition

10. theorem OAI.ThompsonNonamenability.imagePartition_cells line 108
11. theorem OAI.ThompsonNonamenability.mem_imagePartition_cells line 111
12. theorem OAI.ThompsonNonamenability.imagePartition_proof_irrel line 116
13. theorem OAI.ThompsonNonamenability.imagePartition_cellCount line 120
14. theorem OAI.ThompsonNonamenability.eventually_image_cells_small line 127

    Source documentation

    Simultaneously gives actual image cells and the desired mesh bound.

    theorem eventually_image_cells_small (g : F) (ε : ℝ) (hε : 0 < ε) :
        ∃ N : ℕ, ∀ n ≥ N, ∀ k : Fin (2 ^ n), ∃ I : BasicInterval,
          I.left = (g (uniformDyadicPoint n k.castSucc) : ℝ) ∧
          I.right = (g (uniformDyadicPoint n k.succ) : ℝ) ∧ I.length < ε := by
    …

    Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.uniformDyadicPoint

15. theorem OAI.ThompsonNonamenability.eventually_image_basic line 177
16. theorem OAI.ThompsonNonamenability.eventually_image_mesh_lt line 184
17. theorem OAI.ThompsonNonamenability.eventually_image_respects line 204

    Source documentation

    A single actual grid level works for both finite families.

    theorem eventually_image_respects (K : Finset F) (J : Finset BasicInterval) :
        ∃ N, ∀ n ≥ N, ∀ g ∈ K, ∃ hg : ImageBasic g n,
          ∀ I ∈ J, (imagePartition g n hg).Respects I := by
    …

    Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.ImageBasic, OAI.ThompsonNonamenability.imagePartition