1. FormalConjecturesForMathlib
  2. Combinatorics
  3. SimpleGraph
  4. Independence
/- 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.Clique public import Mathlib.Data.Real.Basic@[expose] public sectionnamespace SimpleGraphopen Finsetvariable {α : Type*} [Fintype α] [DecidableEq α]

The maximum cardinality among all independent sets s that maximize the quantity |s| - |N(s)|, where N(s) is the neighborhood of the set s.

noncomputable def aprime (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ := letI indep_sets : Finset (Finset α) := univ.powerset.filter (fun s => G.IsIndepSet (s : Set α)) letI diff (s : Finset α) : ℤ := (s.card : ℤ) - (⋃ v ∈ (s : Set α), G.neighborSet v).toFinset.card letI max_diff := (indep_sets.image diff).max letI critical_sets := indep_sets.filter (fun s ↦ diff s = max_diff.getD 0) letI max_card := (critical_sets.image Finset.card).max (max_card.getD 0 : ℝ)

Independence number of the neighbourhood of v.

noncomputable def indepNeighborsCard (G : SimpleGraph α) (v : α) : ℕ := (G.induce (G.neighborSet v)).indepNum

The same quantity as a real number.

noncomputable def indepNeighbors (G : SimpleGraph α) (v : α) : ℝ := (indepNeighborsCard G v : ℝ)

Average of indepNeighbors over all vertices.

noncomputable def averageIndepNeighbors (G : SimpleGraph α) : ℝ := (∑ v ∈ Finset.univ, indepNeighbors G v) / (Fintype.card α : ℝ)

Abbreviation for the average independence number of the neighborhoods.

noncomputable abbrev l (G : SimpleGraph α) : ℝ := averageIndepNeighbors G

The same quantity under a different name, used in some conjectures.

noncomputable abbrev l_avg (G : SimpleGraph α) : ℝ := averageIndepNeighbors G

Computable independence number via powerset enumeration.

def computable_indep_num (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ := (Finset.univ.powerset.filter (fun s : Finset α => ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v)).sup Finset.card

Equivalence between computable and noncomputable independence number.

theorem indep_num_eq_computable (G : SimpleGraph α) [DecidableRel G.Adj] : G.indepNum = computable_indep_num G := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.indepNum = G.computable_indep_num α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ sSup {n | ∃ s, G.IsNIndepSet n s} = {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ sSup {n | ∃ s, G.IsNIndepSet n s} ≤ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup cardα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card ≤ sSup {n | ∃ s, G.IsNIndepSet n s} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ sSup {n | ∃ s, G.IsNIndepSet n s} ≤ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {n | ∃ s, G.IsNIndepSet n s}.Nonemptyα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {n | ∃ s, G.IsNIndepSet n s}, b ≤ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {n | ∃ s, G.IsNIndepSet n s}.Nonempty α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.IsIndepSet ↑∅ All goals completed! 🐙 α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {n | ∃ s, G.IsNIndepSet n s}, b ≤ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjn:ℕs:Finset αhs:G.IsNIndepSet n s⊢ n ≤ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card calc α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjn:ℕs:Finset αhs:G.IsNIndepSet n s⊢ s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjn:ℕs:Finset αhs:G.IsNIndepSet n s⊢ s ⊆ univ ∧ ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v All goals completed! 🐙 α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup card ≤ sSup {n | ∃ s, G.IsNIndepSet n s} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}, #b ≤ sSup {n | ∃ s, G.IsNIndepSet n s} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}⊢ #s ≤ sSup {n | ∃ s, G.IsNIndepSet n s} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}⊢ BddAbove {n | ∃ s, G.IsNIndepSet n s}α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}⊢ #s ∈ {n | ∃ s, G.IsNIndepSet n s} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}⊢ BddAbove {n | ∃ s, G.IsNIndepSet n s} All goals completed! 🐙 α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}⊢ #s ∈ {n | ∃ s, G.IsNIndepSet n s} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}⊢ ∃ s_1, G.IsNIndepSet (#s) s_1 All goals completed! 🐙

Maximum local independence number over all vertices. For each vertex, we compute the independence number of the subgraph induced by its neighbors, and take the maximum over all vertices.

noncomputable def maxLocalIndependence (G : SimpleGraph α) : ℕ := let locals := Finset.univ.image (fun v => (G.induce (G.neighborSet v)).indepNum) (locals.max).getD 0

Minimum local independence number over all vertices. For each vertex, we compute the independence number of the subgraph induced by its neighbors, and take the minimum over all vertices.

noncomputable def minLocalIndependence (G : SimpleGraph α) : ℕ := let locals := Finset.univ.image (fun v => (G.induce (G.neighborSet v)).indepNum) (locals.min).getD 0end SimpleGraph