OAI/Topology/CoarseAssembly/GraphMetric.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The metric of a connected graph

The metric on a connected graph is exactly the real-valued shortest-path length. A proof-independent extension uses the discrete metric otherwise.

  1. theorem OAI.CoarseAssembly.graphMetricOrDiscrete_eq line 20
  2. def OAI.CoarseAssembly.graphMetric line 25
  3. theorem OAI.CoarseAssembly.graphMetric_eq line 28
  4. theorem OAI.CoarseAssembly.graphMetric_separated line 32
  5. theorem OAI.CoarseAssembly.graphMetric_ball_bound line 39

    Source documentation

    An exact metric ball, with the explicit bound inherited from degree.

    theorem graphMetric_ball_bound [DecidableEq V] (hG : G.Connected)
    (neighbors : V → Finset V) (d : ℕ)
    (hN : ∀ x y, G.Adj x y → y ∈ neighbors x)
    (hd : ∀ x, (neighbors x).card ≤ d) (R : ℝ) (x : V) :
    ∃ b : Finset V,
      (∀ y, y ∈ b ↔ (G.dist x y : ℝ) ≤ R) ∧ b.card ≤ (d + 1) ^ ⌈R⌉₊ := by
…