OAI/Topology/CoarseAssembly/Lattice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The triangular-lattice discs

The vertex set, adjacency, radius and depth used in §3 of the coarse Novikov manuscript. The three integer linear forms are precisely those in its hexagonal radius max {|a|, |b|, |a+b|}. These definitions do not assert the unproved identification of the filled geometric realization with a topological disc.

  1. theorem OAI.CoarseAssembly.latticeRadius_nonneg line 21
  2. def OAI.CoarseAssembly.latticeNeighbors line 24
  3. theorem OAI.CoarseAssembly.mem_latticeNeighbors_iff line 28
  4. theorem OAI.CoarseAssembly.card_latticeNeighbors_le line 36
  5. theorem OAI.CoarseAssembly.latticeRadius_adj line 49

    Source documentation

    Radius changes by at most one across a lattice edge.

    theorem latticeRadius_adj {u v : LatticeVertex} (h : triangularGraph.Adj u v) :
    |latticeRadius u - latticeRadius v| ≤ 1 := by
…

    Mentions: OAI.CoarseAssembly.LatticeVertex, OAI.CoarseAssembly.latticeRadius

  6. theorem OAI.CoarseAssembly.finite_disc line 59
  7. instance OAI.CoarseAssembly.(instance at line 65) line 65
  8. theorem OAI.CoarseAssembly.discDepth_int line 68
  9. theorem OAI.CoarseAssembly.discDepth_adj line 72
  10. theorem OAI.CoarseAssembly.discDepth_eq_zero_iff line 79