2607.19268v1 / CoreLemma.lean
all files
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
import Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-!
# Lemma 3.3: the bookkeeping identities driving the Perron-vector argument
This file formalizes the three identities in Lemma 3.3 for a finite simple
graph of minimum degree at least three and, for the degree-excess identity,
the triangulation edge count `3n - 6`.
-/
open Finset
namespace BootsRoyleCaoVince.CoreLemma
variable {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
/-- Vertices of degree three. -/
def cubicVertices : Finset (Fin n) :=
Finset.univ.filter fun v => G.degree v = 3
/-- `c_v = max(0,d(v)-4)`, represented by truncated natural subtraction. -/
def excess (v : Fin n) : ℕ := G.degree v - 4
/-- The Perron mass on cubic vertices. -/
def cubicMass (x : Fin n → ℝ) : ℝ :=
∑ v ∈ cubicVertices G, x v
/-- The degree-excess term `E`. -/
def excessEnergy (x : Fin n → ℝ) : ℝ :=
∑ v, (excess G v : ℝ) * x v
/-- Perron mass outside the closed neighborhood of `v`. -/
def outsideClosedMass (x : Fin n → ℝ) (v : Fin n) : ℝ :=
∑ w ∈ Finset.univ.filter (fun w => w ≠ v ∧ ¬G.Adj v w), x w
private lemma sum_neighbor_values_eq_weighted_degrees (x : Fin n → ℝ) :
(∑ v, ∑ w ∈ G.neighborFinset v, x w) = ∑ v, (G.degree v : ℝ) * x v := by
calc
(∑ v, ∑ w ∈ G.neighborFinset v, x w) =
∑ v, ∑ w, if G.Adj v w then x w else 0 := by
apply Finset.sum_congr rfl
intro v _
rw [← Finset.sum_filter]
congr 1
ext w
simp
_ = ∑ w, ∑ v, if G.Adj v w then x w else 0 := by
rw [Finset.sum_comm]
_ = ∑ w, (G.degree w : ℝ) * x w := by
apply Finset.sum_congr rfl
intro w _
rw [G.degree_eq_sum_if_adj w]
rw [Finset.sum_mul]
apply Finset.sum_congr rfl
intro v _
by_cases h : G.Adj v w
· have h' : G.Adj w v := G.adj_symm h
simp [h, h']
· have h' : ¬G.Adj w v := fun hwv => h (G.adj_symm hwv)
simp [h, h']
private lemma weighted_degree_identity {x : Fin n → ℝ} {lam : ℝ}
(hxsum : ∑ v, x v = 1)
(heigen : Matrix.mulVec (G.adjMatrix ℝ) x = lam • x) :
lam = ∑ v, (G.degree v : ℝ) * x v := by
have hpoint (v : Fin n) :
∑ w ∈ G.neighborFinset v, x w = lam * x v := by
have h := congrFun heigen v
simpa [G.adjMatrix_mulVec_apply, Pi.smul_apply, smul_eq_mul] using h
calc
lam = ∑ v, lam * x v := by rw [← Finset.mul_sum, hxsum, mul_one]
_ = ∑ v, ∑ w ∈ G.neighborFinset v, x w := by
apply Finset.sum_congr rfl
intro v _
exact (hpoint v).symm
_ = ∑ v, (G.degree v : ℝ) * x v := sum_neighbor_values_eq_weighted_degrees G x
/-- The first identity in Lemma 3.3: `λ = 4 + E - L`. -/
theorem lambda_eq_four_add_excessEnergy_sub_cubicMass {x : Fin n → ℝ} {lam : ℝ}
(hmin : ∀ v, 3 ≤ G.degree v)
(hxsum : ∑ v, x v = 1)
(heigen : Matrix.mulVec (G.adjMatrix ℝ) x = lam • x) :
lam = 4 + excessEnergy G x - cubicMass G x := by
have hdecomp (v : Fin n) :
(G.degree v : ℝ) * x v =
4 * x v + (excess G v : ℝ) * x v -
(if G.degree v = 3 then x v else 0) := by
by_cases h3 : G.degree v = 3
· simp only [excess, h3, if_true]
norm_num
ring
· have hvmin := hmin v
have h4 : 4 ≤ G.degree v := by omega
rw [if_neg h3]
simp only [sub_zero, excess]
rw [Nat.cast_sub h4]
ring
have hcubic : (∑ v, if G.degree v = 3 then x v else 0) = cubicMass G x := by
rw [cubicMass, cubicVertices, Finset.sum_filter]
rw [weighted_degree_identity G hxsum heigen]
calc
(∑ v, (G.degree v : ℝ) * x v) =
∑ v, (4 * x v + (excess G v : ℝ) * x v -
(if G.degree v = 3 then x v else 0)) := by
apply Finset.sum_congr rfl
intro v _
exact hdecomp v
_ = 4 + excessEnergy G x - cubicMass G x := by
simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.mul_sum,
hxsum, mul_one, excessEnergy]
rw [hcubic]
/-- The degree-excess identity in Lemma 3.3, stated in `ℤ` to avoid
truncated subtraction on the right: `∑ c_v = 2n - 12 + k`. -/
theorem sum_excess_eq {hn : 3 ≤ n}
(hmin : ∀ v, 3 ≤ G.degree v)
(hedges : G.edgeFinset.card = 3 * n - 6) :
(∑ v, (excess G v : ℤ)) =
2 * (n : ℤ) - 12 + (cubicVertices G).card := by
have hdegreeNat : ∑ v, G.degree v = 6 * n - 12 := by
rw [G.sum_degrees_eq_twice_card_edges, hedges]
omega
have hpoint (v : Fin n) :
(G.degree v : ℤ) - 4 = (excess G v : ℤ) -
(if G.degree v = 3 then 1 else 0) := by
by_cases h3 : G.degree v = 3
· simp [h3, excess]
· have hvmin := hmin v
have h4 : 4 ≤ G.degree v := by omega
rw [if_neg h3]
simp only [sub_zero, excess, Nat.cast_sub h4]
norm_num
have hsumPoint :
(∑ v, ((G.degree v : ℤ) - 4)) =
∑ v, ((excess G v : ℤ) - if G.degree v = 3 then 1 else 0) := by
apply Finset.sum_congr rfl
intro v _
exact hpoint v
rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
Fintype.card_fin, nsmul_eq_mul] at hsumPoint
rw [Finset.sum_sub_distrib] at hsumPoint
have hcubic : (∑ v : Fin n, if G.degree v = 3 then (1 : ℤ) else 0) =
(cubicVertices G).card := by
simp [cubicVertices]
rw [hcubic] at hsumPoint
have hdegreeInt : (∑ v, (G.degree v : ℤ)) = 6 * (n : ℤ) - 12 := by
calc
(∑ v, (G.degree v : ℤ)) = ((∑ v, G.degree v : ℕ) : ℤ) := by simp
_ = ((6 * n - 12 : ℕ) : ℤ) := by rw [hdegreeNat]
_ = 6 * (n : ℤ) - 12 := by
rw [Nat.cast_sub (by omega : 12 ≤ 6 * n)]
push_cast
norm_num
rw [hdegreeInt] at hsumPoint
linarith
private lemma total_mass_partition (x : Fin n → ℝ) (v : Fin n) :
(∑ w, x w) = x v + (∑ w ∈ G.neighborFinset v, x w) + outsideClosedMass G x v := by
have hself : (∑ w, if w = v then x w else 0) = x v := by simp
have hneighbor : (∑ w, if G.Adj v w then x w else 0) =
∑ w ∈ G.neighborFinset v, x w := by
rw [← Finset.sum_filter]
congr 1
ext w
simp
have houtside : (∑ w, if w ≠ v ∧ ¬G.Adj v w then x w else 0) =
outsideClosedMass G x v := by
rw [outsideClosedMass, Finset.sum_filter]
calc
(∑ w, x w) = ∑ w, ((if w = v then x w else 0) +
(if G.Adj v w then x w else 0) +
(if w ≠ v ∧ ¬G.Adj v w then x w else 0)) := by
apply Finset.sum_congr rfl
intro w _
by_cases hwv : w = v
· subst w
simp
· by_cases ha : G.Adj v w <;> simp [hwv, ha]
_ = x v + (∑ w ∈ G.neighborFinset v, x w) + outsideClosedMass G x v := by
rw [Finset.sum_add_distrib, Finset.sum_add_distrib, hself, hneighbor, houtside]
/-- The final identity of Lemma 3.3: mass outside a closed neighborhood is
`1 - (λ+1)x_v`. -/
theorem outsideClosedMass_eq {x : Fin n → ℝ} {lam : ℝ}
(hxsum : ∑ w, x w = 1)
(heigen : Matrix.mulVec (G.adjMatrix ℝ) x = lam • x) (v : Fin n) :
outsideClosedMass G x v = 1 - (lam + 1) * x v := by
have hpoint : ∑ w ∈ G.neighborFinset v, x w = lam * x v := by
have h := congrFun heigen v
simpa [G.adjMatrix_mulVec_apply, Pi.smul_apply, smul_eq_mul] using h
have hp := total_mass_partition G x v
rw [hxsum, hpoint] at hp
linarith
#print axioms lambda_eq_four_add_excessEnergy_sub_cubicMass
#print axioms sum_excess_eq
#print axioms outsideClosedMass_eq
end BootsRoyleCaoVince.CoreLemma