|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lior Horesh. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Lior Horesh |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Combinatorics.SimpleGraph.Metric |
| 9 | +public import Mathlib.Combinatorics.SimpleGraph.Finite |
| 10 | +public import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 11 | + |
| 12 | +/-! |
| 13 | +# Cardinality of metric balls in a simple graph |
| 14 | +
|
| 15 | +This module introduces `SimpleGraph.ballFinset`, the `Finset` companion |
| 16 | +to `SimpleGraph.ball` on graphs with a `Fintype` vertex set, together |
| 17 | +with the polynomial cardinality envelope |
| 18 | +
|
| 19 | +`ball_card_le_pow_of_le_geom_series` |
| 20 | +
|
| 21 | +which rearranges the standard geometric-series ball bound |
| 22 | +`|ball v (r + 1)| ≤ ∑_{k=0}^{r} Δ^k` for locally-finite graphs of |
| 23 | +maximum degree at most `Δ` into the cruder polynomial form |
| 24 | +`(r + 1) · Δ^r`. The geometric-series hypothesis is taken as a |
| 25 | +parameter; the unconditional form requires a sphere-cardinality lemma |
| 26 | +and is planned as a follow-up PR. |
| 27 | +
|
| 28 | +Note that `SimpleGraph.ball` is the *open* metric ball |
| 29 | +`{u | edist u c < r}`, so the classical closed-ball cardinality |
| 30 | +`|{u | edist u c ≤ r}|` is `|ballFinset v (r + 1)|` in this file. |
| 31 | +
|
| 32 | +## Main definitions |
| 33 | +
|
| 34 | +* `SimpleGraph.ballFinset`: the `Finset` version of `SimpleGraph.ball` |
| 35 | + on graphs with a `Fintype` vertex set. |
| 36 | +
|
| 37 | +## Main results |
| 38 | +
|
| 39 | +* `SimpleGraph.mem_ballFinset`: membership in `ballFinset`. |
| 40 | +* `SimpleGraph.ballFinset_zero`: `ballFinset v 0 = ∅`. |
| 41 | +* `SimpleGraph.ballFinset_one`: `ballFinset v 1 = {v}`. |
| 42 | +* `SimpleGraph.ball_card_le_pow_of_le_geom_series`: polynomial envelope |
| 43 | + `|ballFinset v (r + 1)| ≤ (r + 1) · Δ^r` conditional on the |
| 44 | + geometric-series hypothesis |
| 45 | + `|ballFinset v (r + 1)| ≤ ∑_{k=0}^{r} Δ^k`. |
| 46 | +
|
| 47 | +## Tags |
| 48 | +
|
| 49 | +graph metric, ball, cardinality, geometric series |
| 50 | +-/ |
| 51 | + |
| 52 | +@[expose] public section |
| 53 | + |
| 54 | +namespace SimpleGraph |
| 55 | + |
| 56 | +variable {V : Type*} (G : SimpleGraph V) [Fintype V] |
| 57 | + |
| 58 | +/-- `Finset` version of `SimpleGraph.ball`. On graphs with a `Fintype` |
| 59 | +vertex set every set of vertices is finite, so the open metric ball |
| 60 | +coerces to a `Finset`. The radius is typed `ℕ` for ergonomics at |
| 61 | +cardinality-facing call sites; `SimpleGraph.ball` itself takes `ℕ∞`. -/ |
| 62 | +noncomputable def ballFinset (c : V) (r : ℕ) : Finset V := |
| 63 | + (G.ball c r).toFinite.toFinset |
| 64 | + |
| 65 | +@[simp] lemma mem_ballFinset {c v : V} {r : ℕ} : |
| 66 | + v ∈ G.ballFinset c r ↔ G.edist v c < (r : ℕ∞) := by |
| 67 | + simp [ballFinset] |
| 68 | + |
| 69 | +/-- The radius-`0` ball is empty. -/ |
| 70 | +@[simp] lemma ballFinset_zero (c : V) : G.ballFinset c 0 = ∅ := by |
| 71 | + ext v |
| 72 | + simp [ballFinset, ball_zero] |
| 73 | + |
| 74 | +/-- The radius-`1` ball is the singleton `{c}`. -/ |
| 75 | +@[simp] lemma ballFinset_one (c : V) : G.ballFinset c 1 = {c} := by |
| 76 | + ext v |
| 77 | + simp [ballFinset, ball_one] |
| 78 | + |
| 79 | +/-- **Polynomial bound from a geometric-series hypothesis.** If the |
| 80 | +open ball of radius `r + 1` (equivalently, the classical closed ball |
| 81 | +of radius `r`) has cardinality bounded above by the geometric series |
| 82 | +`∑_{k=0}^{r} Δ^k` (the standard envelope for locally-finite graphs |
| 83 | +of maximum degree at most `Δ`), then under `1 ≤ Δ` the ball has |
| 84 | +cardinality bounded above by the cruder polynomial `(r + 1) · Δ^r`. |
| 85 | +
|
| 86 | +The geometric-series bound itself, |
| 87 | +`|ballFinset v (r + 1)| ≤ ∑_{k=0}^{r} Δ^k`, is the natural companion |
| 88 | +of this theorem and is planned as a follow-up PR: its inductive step |
| 89 | +requires a sphere-cardinality lemma |
| 90 | +`|sphere v (r + 1)| ≤ Δ · |sphere v r|` not yet in Mathlib. By |
| 91 | +stating the polynomial bound conditionally on the geometric-series |
| 92 | +hypothesis, this PR stays zero-`sorry` while still packaging the |
| 93 | +algebraic rearrangement that downstream users (Lieb–Robinson |
| 94 | +cone-volume arguments, light-cone tensor-network contraction) consume. |
| 95 | +
|
| 96 | +The `(Δ + 1) · Δ^r` form fails at `Δ = 1`: a ball of radius `r` on a |
| 97 | +path has `2r + 1` vertices, exceeding `(Δ + 1) · Δ^r = 2` for |
| 98 | +`r ≥ 1`. The `(r + 1) · Δ^r` bound is the correct unconditional |
| 99 | +polynomial form. -/ |
| 100 | +theorem ball_card_le_pow_of_le_geom_series |
| 101 | + (Δ : ℕ) (hΔpos : 1 ≤ Δ) (v : V) (r : ℕ) |
| 102 | + (hgeom : (G.ballFinset v (r + 1)).card ≤ ∑ k ∈ Finset.range (r + 1), Δ ^ k) : |
| 103 | + (G.ballFinset v (r + 1)).card ≤ (r + 1) * Δ ^ r := by |
| 104 | + have hterm : ∀ k ∈ Finset.range (r + 1), Δ ^ k ≤ Δ ^ r := fun k hk => |
| 105 | + Nat.pow_le_pow_right hΔpos (Finset.mem_range_succ_iff.mp hk) |
| 106 | + have hsum : ∑ k ∈ Finset.range (r + 1), Δ ^ k ≤ |
| 107 | + ∑ _k ∈ Finset.range (r + 1), Δ ^ r := |
| 108 | + Finset.sum_le_sum hterm |
| 109 | + have hconst : |
| 110 | + ∑ _k ∈ Finset.range (r + 1), Δ ^ r = (r + 1) * Δ ^ r := by |
| 111 | + rw [Finset.sum_const, Finset.card_range, smul_eq_mul] |
| 112 | + calc (G.ballFinset v (r + 1)).card |
| 113 | + ≤ ∑ k ∈ Finset.range (r + 1), Δ ^ k := hgeom |
| 114 | + _ ≤ ∑ _k ∈ Finset.range (r + 1), Δ ^ r := hsum |
| 115 | + _ = (r + 1) * Δ ^ r := hconst |
| 116 | + |
| 117 | +end SimpleGraph |
0 commit comments