FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced

/-
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.Acyclic
public import Mathlib.Data.Real.Basic

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

largestInducedForestSize G is the size of a largest induced forest of G.

noncomputable def largestInducedForestSize (G : SimpleGraph α) : ℕ :=
  sSup { n | ∃ s : Finset α, (G.induce s).IsAcyclic ∧ s.card = n }

largestInducedBipartiteSubgraphSize G is the size of a largest induced bipartite subgraph of G.

noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=
  sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }

omit [Fintype α] in

An induced subgraph is bipartite exactly when its vertices admit a two-coloring.

theorem induce_isBipartite_iff_exists_coloring (G : SimpleGraph α) (s : Finset α) :
    (G.induce s).IsBipartite ↔
      ∃ c : α → Fin 2, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v := byα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset α⊢ (induce (↑s) G).IsBipartite ↔ ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v
  constructormpα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset α⊢ (induce (↑s) G).IsBipartite → ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c vmprα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset α⊢ (∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v) → (induce (↑s) G).IsBipartite
  ·mpα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset α⊢ (induce (↑s) G).IsBipartite → ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v rintro ⟨c⟩mpα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset αc:(induce (↑s) G).Coloring (Fin 2)⊢ ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v
    refine ⟨fun v => if hv : v ∈ s then c ⟨v, hv⟩ else 0, ?_⟩mpα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset αc:(induce (↑s) G).Coloring (Fin 2)⊢ ∀ u ∈ s,
  ∀ v ∈ s, G.Adj u v → (fun v ↦ if hv : v ∈ s then c ⟨v, hv⟩ else 0) u ≠ (fun v ↦ if hv : v ∈ s then c ⟨v, hv⟩ else 0) v
    intro u hu v hv huvmpα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset αc:(induce (↑s) G).Coloring (Fin 2)u:αhu:u ∈ sv:αhv:v ∈ shuv:G.Adj u v⊢ (fun v ↦ if hv : v ∈ s then c ⟨v, hv⟩ else 0) u ≠ (fun v ↦ if hv : v ∈ s then c ⟨v, hv⟩ else 0) v
    simp only [dif_pos hu, dif_pos hv]mpα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset αc:(induce (↑s) G).Coloring (Fin 2)u:αhu:u ∈ sv:αhv:v ∈ shuv:G.Adj u v⊢ c ⟨u, hu⟩ ≠ c ⟨v, hv⟩
    exact c.valid huvAll goals completed! 🐙
  ·mprα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset α⊢ (∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v) → (induce (↑s) G).IsBipartite rintro ⟨c, hc⟩mprα:Type u_1inst✝:DecidableEq αG:SimpleGraph αs:Finset αc:α → Fin 2hc:∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v⊢ (induce (↑s) G).IsBipartite
    exact ⟨Coloring.mk (fun v => c v) fun {u v} huv => hc u u.prop v v.prop huv⟩All goals completed! 🐙

Computable largest induced bipartite subgraph size via powerset enumeration.

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

The computable largest induced bipartite subgraph size agrees with the sSup definition.


theorem largestInducedBipartiteSubgraphSize_eq_computable
    (G : SimpleGraph α) [DecidableRel G.Adj] :
    G.largestInducedBipartiteSubgraphSize = G.computableLargestInducedBipartiteSubgraphSize := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.largestInducedBipartiteSubgraphSize = G.computableLargestInducedBipartiteSubgraphSize
  unfold largestInducedBipartiteSubgraphSize computableLargestInducedBipartiteSubgraphSizeα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n} =
  {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card
  apply le_antisymmaα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n} ≤
  {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.cardaα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card ≤
  sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}
  ·aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n} ≤
  {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card apply csSup_lea.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}.Nonemptyh₂α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n},
  b ≤ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card
    ·a.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}.Nonempty refine ⟨0, ∅, ?_, rfl⟩a.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ (induce (↑∅) G).IsBipartite
      rw [induce_isBipartite_iff_exists_coloringa.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∃ c, ∀ u ∈ ∅, ∀ v ∈ ∅, G.Adj u v → c u ≠ c va.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∃ c, ∀ u ∈ ∅, ∀ v ∈ ∅, G.Adj u v → c u ≠ c v]a.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∃ c, ∀ u ∈ ∅, ∀ v ∈ ∅, G.Adj u v → c u ≠ c v
      exact ⟨fun _ => 0, byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ u ∈ ∅, ∀ v ∈ ∅, G.Adj u v → (fun x ↦ 0) u ≠ (fun x ↦ 0) v simpAll goals completed! 🐙⟩
    ·h₂α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n},
  b ≤ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card rintro n ⟨s, hs, rfl⟩h₂α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:(induce (↑s) G).IsBipartite⊢ s.card ≤ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card
      apply Finset.le_suph₂α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:(induce (↑s) G).IsBipartite⊢ s ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}
      exact Finset.mem_filter.mpr ⟨Finset.mem_powerset.mpr (Finset.subset_univ s),
        (induce_isBipartite_iff_exists_coloring G s).mp hs⟩All goals completed! 🐙
  ·aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}.sup Finset.card ≤
  sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n} apply Finset.sup_leaα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v},
  b.card ≤ sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}
    intro s hsaα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}⊢ s.card ≤ sSup {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}
    apply le_csSupa.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}⊢ BddAbove {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}h₂α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}⊢ s.card ∈ {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n}
    ·a.h₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}⊢ BddAbove {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n} exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩All goals completed! 🐙
    ·h₂α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjs:Finset αhs:s ∈ {s ∈ Finset.univ.powerset | ∃ c, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v}⊢ s.card ∈ {n | ∃ s, (induce (↑s) G).IsBipartite ∧ s.card = n} exact ⟨s, (induce_isBipartite_iff_exists_coloring G s).mpr
        (Finset.mem_filter.mp hs).2, rfl⟩All goals completed! 🐙

b G is the number of vertices of a largest induced bipartite subgraph of G. Returned as a real number.

noncomputable def b (G : SimpleGraph α) : ℝ :=
  (largestInducedBipartiteSubgraphSize G : ℝ)

end SimpleGraph