OAI/MathematicalPhysics/Heisenberg/RegularComponents.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.LatticeRegular.component_exit line 13
  2. lemma OAI.Heisenberg.LatticeRegular.component_witness line 29
  3. theorem OAI.Heisenberg.LatticeRegular.small_component_of_local_count line 57
  4. theorem OAI.Heisenberg.LatticeRegular.component_radius line 71
  5. lemma OAI.Heisenberg.Geometry.dist_le_iff_mem_ball line 89
  6. lemma OAI.Heisenberg.Geometry.step_dist_le_one line 97
  7. def OAI.Heisenberg.LatticeRegular.Regular line 105
  8. theorem OAI.Heisenberg.LatticeRegular.regular_component_envelope line 110
  9. lemma OAI.Heisenberg.RoutingDecay.eventually_half line 166
  10. theorem OAI.Heisenberg.RoutingDecay.comparable_radii line 183
  11. theorem OAI.Heisenberg.RoutingDecay.neighborhood_displacement line 216
  12. theorem OAI.Heisenberg.RoutingDecay.inverse_displacement line 239