FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SzegedIndex

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Combinatorics.SimpleGraph.Metric
public import Mathlib.Order.BourbakiWitt
public import Mathlib.Tactic.Ring.Basic
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance

@[expose] public sectionnamespace SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]

Auxiliary function for Szeged index: counts vertices closer to u than v.

noncomputable def szeged_aux (G : SimpleGraph α) (u v : α) : ℕ :=
  (Finset.univ.filter (fun w => G.edist w u < G.edist w v)).card

The Szeged index of G.

This is define as the sum ∑_{uv ∈ E(G)} n_u(u,v) * n_v(u,v) where n_u(uv) is the number of vertices closer to u than v.

noncomputable def szegedIndex (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
  ∑ e ∈ G.edgeFinset,
    e.lift ⟨fun u v => szeged_aux G u v * szeged_aux G v u, byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 α⊢ ∀ (a₁ a₂ : α),
  (fun u v ↦ G.szeged_aux u v * G.szeged_aux v u) a₁ a₂ = (fun u v ↦ G.szeged_aux u v * G.szeged_aux v u) a₂ a₁ simp [mul_comm]All goals completed! 🐙⟩

Computable Szeged auxiliary: count vertices closer to u than v.

def computable_szeged_aux (G : SimpleGraph α) [DecidableRel G.Adj] (u v : α) : ℕ :=
  (Finset.univ.filter (fun w => computable_dist G w u < computable_dist G w v)).card

Computable Szeged index.

def computable_szeged_index (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
  ∑ e ∈ G.edgeFinset,
    Sym2.lift ⟨fun u v => computable_szeged_aux G u v * computable_szeged_aux G v u,
      fun a b => byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αa:αb:α⊢ (fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u) a b =
  (fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u) b a ringAll goals completed! 🐙⟩ e



-- Helper: edist comparison ↔ dist comparison for adjacent endpoints
omit [Fintype α] [DecidableEq α] in
private lemma edist_lt_iff_dist_lt (G : SimpleGraph α) {u v : α} (hadj : G.Adj u v) (w : α) :
    G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v := byα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:α⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v
  by_cases hru : G.Reachable w uposα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:G.Reachable w u⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w vnegα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:¬G.Reachable w u⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v
  ·posα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:G.Reachable w u⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v have hrv : G.Reachable w v := hru.trans hadj.reachableposα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:G.Reachable w uhrv:G.Reachable w v⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v
    rw [← hru.coe_dist_eq_edist,posα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:G.Reachable w uhrv:G.Reachable w v⊢ ↑(G.dist w u) < G.edist w v ↔ G.dist w u < G.dist w vAll goals completed! 🐙 ← hrv.coe_dist_eq_edist,posα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:G.Reachable w uhrv:G.Reachable w v⊢ ↑(G.dist w u) < ↑(G.dist w v) ↔ G.dist w u < G.dist w vAll goals completed! 🐙 ENat.natCast_lt_natCastposα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:G.Reachable w uhrv:G.Reachable w v⊢ G.dist w u < G.dist w v ↔ G.dist w u < G.dist w vAll goals completed! 🐙]All goals completed! 🐙
  ·negα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:¬G.Reachable w u⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v have hrv : ¬G.Reachable w v :=
      fun h => hru (h.trans hadj.symm.reachable)negα:Type u_1G:SimpleGraph αu:αv:αhadj:G.Adj u vw:αhru:¬G.Reachable w uhrv:¬G.Reachable w v⊢ G.edist w u < G.edist w v ↔ G.dist w u < G.dist w v
    simp [edist_eq_top_of_not_reachable hru, edist_eq_top_of_not_reachable hrv,
          dist_eq_zero_of_not_reachable hru, dist_eq_zero_of_not_reachable hrv]All goals completed! 🐙



private lemma szeged_aux_eq_computable (G : SimpleGraph α) [DecidableRel G.Adj]
    {u v : α} (hadj : G.Adj u v) :
    szeged_aux G u v = computable_szeged_aux G u v := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u v⊢ G.szeged_aux u v = G.computable_szeged_aux u v
  unfold szeged_aux computable_szeged_auxα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u v⊢ {w | G.edist w u < G.edist w v}.card = {w | G.computable_dist w u < G.computable_dist w v}.card
  congr 1α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u v⊢ {w | G.edist w u < G.edist w v} = {w | G.computable_dist w u < G.computable_dist w v}; ext wα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u vw:α⊢ w ∈ {w | G.edist w u < G.edist w v} ↔ w ∈ {w | G.computable_dist w u < G.computable_dist w v}
  simp only [Finset.mem_filter, Finset.mem_univ, true_and]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u vw:α⊢ G.edist w u < G.edist w v ↔ G.computable_dist w u < G.computable_dist w v
  rw [edist_lt_iff_dist_lt G hadj w,α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u vw:α⊢ G.dist w u < G.dist w v ↔ G.computable_dist w u < G.computable_dist w vAll goals completed! 🐙 dist_eq_computable,α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u vw:α⊢ G.computable_dist w u < G.dist w v ↔ G.computable_dist w u < G.computable_dist w vAll goals completed! 🐙 dist_eq_computableα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αhadj:G.Adj u vw:α⊢ G.computable_dist w u < G.computable_dist w v ↔ G.computable_dist w u < G.computable_dist w vAll goals completed! 🐙]All goals completed! 🐙



theorem szeged_eq_computable (G : SimpleGraph α) [DecidableRel G.Adj] :
    szegedIndex G = computable_szeged_index G := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.szegedIndex = G.computable_szeged_index
  unfold szegedIndex computable_szeged_indexα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∑ e ∈ G.edgeFinset, Sym2.lift ⟨fun u v ↦ G.szeged_aux u v * G.szeged_aux v u, ⋯⟩ e =
  ∑ e ∈ G.edgeFinset, Sym2.lift ⟨fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ e
  apply Finset.sum_congr rflα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ x ∈ G.edgeFinset,
  Sym2.lift ⟨fun u v ↦ G.szeged_aux u v * G.szeged_aux v u, ⋯⟩ x =
    Sym2.lift ⟨fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ x
  intro e heα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αhe:e ∈ G.edgeFinset⊢ Sym2.lift ⟨fun u v ↦ G.szeged_aux u v * G.szeged_aux v u, ⋯⟩ e =
  Sym2.lift ⟨fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ e
  revert heα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 α⊢ e ∈ G.edgeFinset →
  Sym2.lift ⟨fun u v ↦ G.szeged_aux u v * G.szeged_aux v u, ⋯⟩ e =
    Sym2.lift ⟨fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ e
  refine Sym2.ind (fun u v => ?_) eα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:α⊢ s(u, v) ∈ G.edgeFinset →
  Sym2.lift ⟨fun u v ↦ G.szeged_aux u v * G.szeged_aux v u, ⋯⟩ s(u, v) =
    Sym2.lift ⟨fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ s(u, v)
  intro heα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinset⊢ Sym2.lift ⟨fun u v ↦ G.szeged_aux u v * G.szeged_aux v u, ⋯⟩ s(u, v) =
  Sym2.lift ⟨fun u v ↦ G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ s(u, v)
  simp only [Sym2.lift_mk]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinset⊢ G.szeged_aux u v * G.szeged_aux v u = G.computable_szeged_aux u v * G.computable_szeged_aux v u
  have hadj : G.Adj u v := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.szegedIndex = G.computable_szeged_indexα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v * G.szeged_aux v u = G.computable_szeged_aux u v * G.computable_szeged_aux v u rwa [mem_edgeFinset,α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeSet⊢ G.Adj u vα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v * G.szeged_aux v u = G.computable_szeged_aux u v * G.computable_szeged_aux v u mem_edgeSetα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:G.Adj u v⊢ G.Adj u vα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v * G.szeged_aux v u = G.computable_szeged_aux u v * G.computable_szeged_aux v u]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:G.Adj u v⊢ G.Adj u vα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v * G.szeged_aux v u = G.computable_szeged_aux u v * G.computable_szeged_aux v u at heα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v * G.szeged_aux v u = G.computable_szeged_aux u v * G.computable_szeged_aux v u
  congr 1e_aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v = G.computable_szeged_aux u ve_aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux v u = G.computable_szeged_aux v u
  ·e_aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux u v = G.computable_szeged_aux u v exact szeged_aux_eq_computable G hadjAll goals completed! 🐙
  ·e_aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adje:Sym2 αu:αv:αhe:s(u, v) ∈ G.edgeFinsethadj:G.Adj u v⊢ G.szeged_aux v u = G.computable_szeged_aux v u exact szeged_aux_eq_computable G hadj.symmAll goals completed! 🐙

end SimpleGraph