OAI/Topology/CoarseAssembly/FiberDegree.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A uniform degree bound for the finite fibered graphs

A neighbor is encoded by its base vertex, one integral left move, and nine binary digits. The digits distinguish children in a successive congruence fiber; at equal or smaller depth the reduced equation already determines the target. The resulting bound is independent of the disc radius.

  1. abbrev OAI.CoarseAssembly.FiberBits line 21
  2. def OAI.CoarseAssembly.fiberBits line 23
  3. def OAI.CoarseAssembly.baseNeighbors line 27
  4. theorem OAI.CoarseAssembly.mem_baseNeighbors line 31
  5. theorem OAI.CoarseAssembly.card_baseNeighbors_le line 36
  6. theorem OAI.CoarseAssembly.fiberBits_injective line 51
  7. theorem OAI.CoarseAssembly.target_eq_of_same_code line 57
  8. def OAI.CoarseAssembly.neighborMove line 80
  9. theorem OAI.CoarseAssembly.neighborMove_spec line 84
  10. def OAI.CoarseAssembly.neighborCode line 92
  11. theorem OAI.CoarseAssembly.neighborCode_injective line 100
  12. theorem OAI.CoarseAssembly.card_fibered_neighbors_le line 119

    Source documentation

    A bound uniform in the component and in the chosen vertex.

    theorem card_fibered_neighbors_le (S : Finset ArithmeticGroup) (t : ℤ_[2]ˣ)
    {j : ℕ} (x : FiberVertex j) :
    Nat.card {y // (fiberedGraph S t j).Adj x y} ≤
      7 * (symmetricMoves S).card * 2 ^ 9 := by
…

    Mentions: OAI.CoarseAssembly.FiberVertex, OAI.CoarseAssembly.fiberedGraph, OAI.CoarseAssembly.symmetricMoves

  13. def OAI.CoarseAssembly.fiberedNeighbors line 134
  14. theorem OAI.CoarseAssembly.mem_fiberedNeighbors line 139
  15. theorem OAI.CoarseAssembly.card_fiberedNeighbors_le line 145
  16. theorem OAI.CoarseAssembly.fiberedGraph_ball_bound line 154

    Source documentation

    Uniform bounded geometry in the intrinsic graph distance.

    theorem fiberedGraph_ball_bound (S : Finset ArithmeticGroup) (t : ℤ_[2]ˣ)
    {j : ℕ} (x : FiberVertex j) (r : ℕ) :
    Set.ncard {y | (fiberedGraph S t j).edist x y ≤ (r : ℕ∞)} ≤
      (7 * (symmetricMoves S).card * 2 ^ 9 + 1) ^ r := by
…

    Mentions: OAI.CoarseAssembly.FiberVertex, OAI.CoarseAssembly.fiberedGraph, OAI.CoarseAssembly.symmetricMoves