CubicPathwidth.T2.Charging

Source file CubicPathwidth/T2/Charging.lean of the Lean project (how it is built).

import CubicPathwidth.T2.DefsB

/-!
# Charging along edges joining degrees 3 and 4 (Theorem 2(b),(c) plan, claim B3)

Proves `ChargingClaim`: under the per-type charging inequalities, the total charge
is at most `a₃ n₃ + a₄ n₄`. The transfer terms cancel by the double count of
edges joining a degree-3 vertex and a degree-4 vertex.
-/

noncomputable section
open scoped Classical

namespace CubicPathwidth
namespace T2

open Finset

/-- The number of neighbors of degree `d`, as a sum of adjacency indicators. -/
lemma nbrCount_cast_eq {n : ℕ} (G : SimpleGraph (Fin n)) (v : Fin n) (d : ℕ) :
    (nbrCount G v d : ℝ) =
      ∑ u, if G.Adj v u ∧ G.degree u = d then (1 : ℝ) else 0 := by
  classical
  unfold nbrCount
  rw [Finset.card_filter, Nat.cast_sum, SimpleGraph.neighborFinset_eq_filter,
    Finset.sum_filter]
  push_cast
  refine Finset.sum_congr rfl fun u _ => ?_
  by_cases h1 : G.Adj v u <;> by_cases h2 : G.degree u = d <;> simp [h1, h2]

/-- Double count: the edges joining a degree-3 and a degree-4 vertex are counted
the same way from both ends. -/
lemma edge_double_count {n : ℕ} (G : SimpleGraph (Fin n)) :
    ∑ v, (if G.degree v = 3 then (nbrCount G v 4 : ℝ) else 0) =
      ∑ u, (if G.degree u = 4 then (nbrCount G u 3 : ℝ) else 0) := by
  classical
  have hL : ∀ v : Fin n,
      (if G.degree v = 3 then (nbrCount G v 4 : ℝ) else 0) =
        ∑ u, if G.degree v = 3 ∧ G.Adj v u ∧ G.degree u = 4 then (1 : ℝ) else 0 := by
    intro v
    rw [nbrCount_cast_eq]
    split_ifs with h
    · simp [h]
    · simp [h]
  have hR : ∀ u : Fin n,
      (if G.degree u = 4 then (nbrCount G u 3 : ℝ) else 0) =
        ∑ v, if G.degree v = 3 ∧ G.Adj v u ∧ G.degree u = 4 then (1 : ℝ) else 0 := by
    intro u
    rw [nbrCount_cast_eq]
    split_ifs with h
    · refine Finset.sum_congr rfl fun v _ => ?_
      simp only [h, and_true]
      by_cases h1 : G.Adj v u
      · have h1' := h1.symm
        by_cases h2 : G.degree v = 3 <;> simp [h1, h1', h2]
      · have h1' : ¬G.Adj u v := fun h' => h1 h'.symm
        by_cases h2 : G.degree v = 3 <;> simp [h1, h1', h2]
    · simp [h]
  simp_rw [hL, hR]
  exact Finset.sum_comm

/-- Each vertex of degree 3 or 4 is counted once: the number of vertices of degree
exactly `d` weighted by a constant. -/
lemma sum_ite_degree_const {n : ℕ} (G : SimpleGraph (Fin n)) (d : ℕ) (a : ℝ) :
    ∑ v, (if G.degree v = d then a else 0) = a * (degreeCount G d : ℝ) := by
  unfold degreeCount
  rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul]
  ring

theorem charging : ChargingClaim := by
  classical
  unfold ChargingClaim
  intro n G hmin hmax C a₃ a₄ t h3 h4
  unfold MinDegreeAtLeast at hmin
  unfold MaxDegreeAtMost at hmax
  have hdeg : ∀ v : Fin n, G.degree v = 3 ∨ G.degree v = 4 := by
    intro v
    have h1 := hmin v
    have h2 := hmax v
    omega
  have hpt : ∀ v : Fin n,
      C v ≤ (if G.degree v = 3 then a₃ else 0) + (if G.degree v = 4 then a₄ else 0) +
        t * ((if G.degree v = 3 then (nbrCount G v 4 : ℝ) else 0) -
          (if G.degree v = 4 then (nbrCount G v 3 : ℝ) else 0)) := by
    intro v
    rcases hdeg v with h | h
    · have := h3 v h
      simp [h]
      linarith
    · have := h4 v h
      simp [h]
      linarith
  calc ∑ v, C v
      ≤ ∑ v, ((if G.degree v = 3 then a₃ else 0) + (if G.degree v = 4 then a₄ else 0) +
          t * ((if G.degree v = 3 then (nbrCount G v 4 : ℝ) else 0) -
            (if G.degree v = 4 then (nbrCount G v 3 : ℝ) else 0))) :=
        Finset.sum_le_sum fun v _ => hpt v
    _ = (∑ v, (if G.degree v = 3 then a₃ else 0)) + (∑ v, (if G.degree v = 4 then a₄ else 0))
          + t * ((∑ v, (if G.degree v = 3 then (nbrCount G v 4 : ℝ) else 0)) -
            (∑ v, (if G.degree v = 4 then (nbrCount G v 3 : ℝ) else 0))) := by
        rw [Finset.sum_add_distrib, Finset.sum_add_distrib, ← Finset.mul_sum,
          Finset.sum_sub_distrib]
    _ = a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) := by
        rw [sum_ite_degree_const, sum_ite_degree_const, edge_double_count, sub_self, mul_zero,
          add_zero]

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.charging