2607.19268v1 / BootsRoyle/Identities.lean
all files
import BootsRoyle.Spectral
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
/-!
# Perron-vector identities
This file formalizes the summation identities in Lemma 3.3 of the paper.
-/
namespace BootsRoyle
open Matrix
variable {V : Type*} [Fintype V] [DecidableEq V]
/-- The normalized Perron data fixed in Sections 3--6 of the paper. -/
structure PerronData (G : SimpleGraph V) where
lambda : ℝ
x : EuclideanSpace ℝ V
nonneg : ∀ v, 0 ≤ x v
l1 : ∑ v, x v = 1
eigen : adjacencyOperator G x = lambda • x
namespace PerronData
variable {G : SimpleGraph V} [DecidableRel G.Adj] (P : PerronData G)
lemma eigen_at (v : V) :
P.lambda * P.x v = ∑ w, if G.Adj v w then P.x w else 0 := by
classical
have h := congrArg (fun y : EuclideanSpace ℝ V ↦ y v) P.eigen
simpa [adjacencyOperator_apply, adjacencyMatrix,
Matrix.mulVec, dotProduct, SimpleGraph.adjMatrix_apply, mul_comm] using h.symm
lemma sum_neighborSums :
∑ v, (∑ w, if G.Adj v w then P.x w else 0) =
∑ v, (G.degree v : ℝ) * P.x v := by
classical
calc
∑ v, (∑ w, if G.Adj v w then P.x w else 0) =
∑ w, ∑ v, if G.Adj v w then P.x w else 0 := Finset.sum_comm
_ = ∑ w, (G.degree w : ℝ) * P.x w := by
apply Finset.sum_congr rfl
intro w _
rw [show (∑ v, if G.Adj v w then P.x w else 0) =
∑ v ∈ G.neighborFinset w, P.x w by
rw [G.neighborFinset_eq_filter, Finset.sum_filter]
simp [G.adj_comm]]
rw [Finset.sum_const, nsmul_eq_mul, G.card_neighborFinset_eq_degree]
/-- Summing the eigenvector equations weights each coordinate by its
vertex degree. This is equation (3.3) in the paper. -/
lemma lambda_eq_sum_degree_mul :
P.lambda = ∑ v, (G.degree v : ℝ) * P.x v := by
calc
P.lambda = ∑ v, P.lambda * P.x v := by rw [← Finset.mul_sum, P.l1, mul_one]
_ = ∑ v, (∑ w, if G.Adj v w then P.x w else 0) := by
apply Finset.sum_congr rfl
intro v _
exact P.eigen_at v
_ = ∑ v, (G.degree v : ℝ) * P.x v := P.sum_neighborSums
/-- Vertices of degree three. -/
def cubicVertices : Finset V :=
Finset.univ.filter fun v ↦ G.degree v = 3
/-- The total Perron weight on cubic vertices, called `L` in the paper. -/
def cubicWeight : ℝ :=
∑ v ∈ cubicVertices (G := G), P.x v
/-- The number `k` of cubic vertices. -/
def cubicCount : ℕ :=
(cubicVertices (G := G)).card
/-- `c_v = max(0,d(v)-4)`, represented by truncated subtraction in `ℕ`. -/
def degreeExcess (v : V) : ℕ :=
G.degree v - 4
/-- The degree-excess Perron weight, called `E` in the paper. -/
def excessWeight : ℝ :=
∑ v, (degreeExcess (G := G) v : ℝ) * P.x v
lemma degree_term_eq (hmin : ∀ v, 3 ≤ G.degree v) (v : V) :
(G.degree v : ℝ) * P.x v =
4 * P.x v + (degreeExcess (G := G) v : ℝ) * P.x v -
(if G.degree v = 3 then P.x v else 0) := by
by_cases hv : G.degree v = 3
· simp [hv, degreeExcess]
<;> ring
· have hv4 : 4 ≤ G.degree v := by
have := hmin v
omega
rw [degreeExcess, Nat.cast_sub hv4]
simp [hv]
ring
/-- The first identity in (3.2), `λ = 4 + E - L`. -/
lemma lambda_eq_four_add_excess_sub_cubicWeight
(hmin : ∀ v, 3 ≤ G.degree v) :
P.lambda = 4 + P.excessWeight - P.cubicWeight := by
rw [P.lambda_eq_sum_degree_mul]
calc
∑ v, (G.degree v : ℝ) * P.x v =
∑ v, (4 * P.x v + (degreeExcess (G := G) v : ℝ) * P.x v -
(if G.degree v = 3 then P.x v else 0)) := by
apply Finset.sum_congr rfl
intro v _
exact P.degree_term_eq hmin v
_ = 4 * (∑ v, P.x v) + P.excessWeight -
(∑ v, if G.degree v = 3 then P.x v else 0) := by
simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.mul_sum,
excessWeight]
_ = 4 + P.excessWeight - P.cubicWeight := by
rw [P.l1, mul_one]
congr 1
rw [cubicWeight, cubicVertices, Finset.sum_filter]
omit [DecidableEq V] in
lemma degreeExcess_cast_eq (hmin : ∀ v, 3 ≤ G.degree v) (v : V) :
(degreeExcess (G := G) v : ℤ) =
(G.degree v : ℤ) - 4 + if G.degree v = 3 then 1 else 0 := by
by_cases hv : G.degree v = 3
· simp [hv, degreeExcess]
· have hv4 : 4 ≤ G.degree v := by
have := hmin v
omega
rw [degreeExcess, Nat.cast_sub hv4]
simp [hv]
/-- The second identity in (3.2), written over `ℤ` to avoid hiding the
subtractions behind truncated natural-number subtraction. -/
lemma sum_degreeExcess_eq (hmin : ∀ v, 3 ≤ G.degree v)
(hedges : (G.edgeFinset.card : ℤ) = 3 * (Fintype.card V : ℤ) - 6) :
∑ v, (degreeExcess (G := G) v : ℤ) =
2 * (Fintype.card V : ℤ) - 12 + cubicCount (G := G) := by
classical
have hdegree :
∑ v, (G.degree v : ℤ) = 2 * (G.edgeFinset.card : ℤ) := by
exact_mod_cast G.sum_degrees_eq_twice_card_edges
calc
∑ v, (degreeExcess (G := G) v : ℤ) =
∑ v, ((G.degree v : ℤ) - 4 +
if G.degree v = 3 then 1 else 0) := by
apply Finset.sum_congr rfl
intro v _
exact degreeExcess_cast_eq hmin v
_ = (∑ v, (G.degree v : ℤ)) - 4 * Fintype.card V +
∑ v, (if G.degree v = 3 then (1 : ℤ) else 0) := by
rw [Finset.sum_add_distrib, Finset.sum_sub_distrib]
simp
ring
_ = 2 * (Fintype.card V : ℤ) - 12 + cubicCount (G := G) := by
rw [hdegree, hedges]
have hcubic :
∑ v, (if G.degree v = 3 then (1 : ℤ) else 0) =
(cubicCount (G := G) : ℤ) := by
rw [cubicCount, cubicVertices]
simp
rw [hcubic]
ring
/-- The total Perron mass outside the closed neighborhood of `v`. -/
noncomputable def remoteMass (v : V) : ℝ := by
classical
exact ∑ w ∈ Finset.univ.filter (fun w ↦ w ≠ v ∧ ¬G.Adj v w), P.x w
/-- The last assertion of Lemma 3.3:
`r_v = 1 - (λ + 1)x_v`. -/
lemma remoteMass_eq (v : V) :
P.remoteMass v = 1 - (P.lambda + 1) * P.x v := by
classical
have hpartition :
P.x v + (∑ w, if G.Adj v w then P.x w else 0) + P.remoteMass v = 1 := by
rw [← P.l1]
rw [remoteMass, Finset.sum_filter]
rw [show P.x v = ∑ w, if w = v then P.x w else 0 by simp]
rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro w hw
by_cases hwv : w = v
· subst w
simp
· by_cases hadj : G.Adj v w
· simp [hwv, hadj]
· simp [hwv, hadj]
rw [← P.eigen_at] at hpartition
linarith
end PerronData
end BootsRoyle