fix misleading definition of f

FormalConjectures/Paper/DegreeSequencesTriangleFree.lean

@@ -120,9 +120,6 @@ namespace SimpleGraph
 
 variable {α : Type*} [Fintype α] [DecidableEq α]
 
-/-- The degree sequence of a graph, sorted in nondecreasing order. -/
-noncomputable def degreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ :=
-  (Finset.univ.val.map fun v : α => G.degree v).sort (· ≤ ·)
 
 /-- The degree sequence of `G` is **compact** if it satisfies
 `IsCompactSequenceOn` for all valid indices `k` such that `k + 2 < Fintype.card α`. -/
@@ -133,7 +130,8 @@ def HasCompactdegreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : Prop :=
 then it is bipartite, has minimum degree `1`, and
 its degree sequence is compact. -/
 @[category research solved, AMS 5]
-theorem theorem1 (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (h₂ : f G = 2) :
+theorem theorem1 (G : SimpleGraph α) (h_conn: G.Connected) [DecidableRel G.Adj]
+    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :
     G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G := by
   sorry
 
@@ -142,7 +140,7 @@ theorem theorem1 (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree
 @[category API, AMS 5]
 lemma lemma3 (n : ℕ) (hn : 0 < n) :
     ∃ (G : SimpleGraph (Fin (8 * n))) (_ : DecidableRel G.Adj),
-      G.IsBipartite ∧ G.minDegree = n + 1 ∧ f G = 3 := by
+      G.IsBipartite ∧ G.minDegree = n + 1 ∧ degreeSequenceMultiplicity G = 3 := by
   sorry
 
 /-- **Lemma 4.** Let `G` be a triangle-free graph with `n` vertices and let `v` be a vertex of `G`.
@@ -151,29 +149,31 @@ There exists a triangle-free graph `H` containing `G` as an induced subgraph suc
 (ii) for every vertex `w` of `G` other than `v` the degree of `w` in `H` is the same as its degree in `G`;
 (iii) if `J` is the subgraph of `H` induced by the vertices not in `G`, then `f(J)=3` and `δ(J) ≥ 2n`. -/
 @[category API, AMS 5]
-lemma lemma4 (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (v : α) :
+lemma lemma4 (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn: G.Connected)
+    (h₁ : G.CliqueFree 3) (v : α) :
     ∃ (β : Type*) (_ : Fintype β) (H : SimpleGraph β) (_ : DecidableRel H.Adj) (i : G ↪g H),
       H.CliqueFree 3 ∧
       H.degree (i v) = G.degree v + 1 ∧
       (∀ w ≠ v, H.degree (i w) = G.degree w) ∧
       let J := H.induce (Set.compl (Set.range i))
-      f J = 3 ∧ J.minDegree ≥ 2 * Fintype.card α := by
+      degreeSequenceMultiplicity J = 3 ∧ J.minDegree ≥ 2 * Fintype.card α := by
   sorry
 
 /-- **Theorem 2.** Every triangle-free graph is an induced subgraph of one
 with `f = 3`. -/
 @[category research solved, AMS 5]
-theorem theorem2 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.CliqueFree 3) :
+theorem theorem2 (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn: G.Connected)
+    (h : G.CliqueFree 3) :
     ∃ (β : Type*) (_ : Fintype β) (H : SimpleGraph β) (_ : DecidableRel H.Adj) (i : G ↪g H),
-      H.CliqueFree 3 ∧ f H = 3 := by
+      H.CliqueFree 3 ∧ degreeSequenceMultiplicity H = 3 := by
   sorry
 
 /-- `F n` is the smallest number of vertices of a triangle-free graph
 with chromatic number `n` and `f = 3`. -/
 @[category research solved, AMS 5]
 noncomputable def F (n : ℕ) : ℕ :=
   sInf { p | ∃ (G : SimpleGraph (Fin p)) (_ : DecidableRel G.Adj),
-    G.CliqueFree 3 ∧ G.chromaticNumber = n ∧ f G = 3 }
+    G.CliqueFree 3 ∧ G.chromaticNumber = n ∧ degreeSequenceMultiplicity G = 3 }
 
 @[category research solved, AMS 5]
 theorem F_three : F 3 = 7 := by

FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean

@@ -31,7 +31,7 @@ number and `b(G)` is the largest induced bipartite subgraph size.
 -/
 @[category research open, AMS 5]
 theorem conjecture40 (h_conn : G.Connected) (h_nontrivial : 1 < Fintype.card α) :
-    ⌈((p G + b G + 1) / 2)⌉ ≤ f G := by
+    ⌈((p G + b G + 1) / 2)⌉ ≤  G.largestInducedForestSize := by
   sorry
 
 end WrittenOnTheWallII.GraphConjecture40

FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean

@@ -31,7 +31,7 @@ bipartite subgraph and `l(v)` is the independence number of `G.neighborSet v`.
 -/
 @[category research open, AMS 5]
 theorem conjecture58 (hG : G.Connected) :
-    Nat.ceil (G.b / G.l_avg) ≤ G.f := by
+    Nat.ceil (G.b / G.l_avg) ≤ G.largestInducedForestSize := by
   sorry
 
 end WrittenOnTheWallII.GraphConjecture58

FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Definitions.lean

@@ -61,9 +61,16 @@ noncomputable def aprime (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
 noncomputable def largestInducedForestSize (G : SimpleGraph α) : ℕ :=
   sSup { n | ∃ s : Finset α, (G.induce s).IsAcyclic ∧ s.card = n }
 
-/-- `f G` is the number of vertices of a largest induced forest of `G` as a real. -/
-noncomputable def f (G : SimpleGraph α) : ℝ :=
-  (largestInducedForestSize G : ℝ)
+/-- The degree sequence of a graph, sorted in nondecreasing order. -/
+noncomputable def degreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ :=
+  (Finset.univ.val.map fun v : α => G.degree v).sort (· ≤ ·)
+
+/--
+The maximum number of occurrences of any term of the degree sequence of `G`.
+-/
+noncomputable def degreeSequenceMultiplicity (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
+  letI degs := degreeSequence G
+  (List.max? (degs.map (fun d => degs.count d))).getD 0
 
 /-- `largestInducedBipartiteSubgraphSize G` is the size of a largest induced
 bipartite subgraph of `G`. -/