feat(Combinatorics/SimpleGraph/Degree): degrees for infinite graphs

Mathlib.lean

@@ -3651,6 +3651,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
 public import Mathlib.Combinatorics.SimpleGraph.Copy
 public import Mathlib.Combinatorics.SimpleGraph.CycleGraph
 public import Mathlib.Combinatorics.SimpleGraph.Dart
+public import Mathlib.Combinatorics.SimpleGraph.Degree
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
 public import Mathlib.Combinatorics.SimpleGraph.Density

Mathlib/Combinatorics/SimpleGraph/Degree.lean

@@ -0,0 +1,390 @@
+/-
+Copyright (c) 2026 Snir Broshi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Snir Broshi
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Copy
+public import Mathlib.Data.ENat.Lattice
+
+/-!
+# Degrees
+
+## Main definitions
+
+* `G.edegree v`: The extended degree of `v` in `G`: the number of vertices adjacent to `v`,
+  or `⊤` if there are infinitely many.
+* `G.maxEDegree`: The maximum extended degree of all vertices, or `0` if there are no vertices.
+* `G.minEDegree`: The minimum extended degree of all vertices, or `⊤` if there are no vertices.
+-/
+
+public section
+
+namespace SimpleGraph
+
+variable {V W : Type*} (G G' : SimpleGraph V) (H : SimpleGraph W) (u v : V)
+
+/-- `G.edegree v` is the extended degree of `v` in `G`: the number of vertices adjacent to `v`,
+or `⊤` if there are infinitely many. -/
+noncomputable def edegree : ℕ∞ :=
+  G.neighborSet v |>.encard
+
+@[simp]
+theorem encard_neighborSet : (G.neighborSet v).encard = G.edegree v := by
+  rfl
+
+variable {G v} in
+@[simp]
+theorem edegree_eq_zero_iff_isIsolated : G.edegree v = 0 ↔ G.IsIsolated v := by
+  simp [← encard_neighborSet]
+
+@[simp]
+alias ⟨_, IsIsolated.edegree_eq⟩ := edegree_eq_zero_iff_isIsolated
+
+variable {G u v} in
+theorem Adj.edegree_ne_zero_left (h : G.Adj u v) : G.edegree u ≠ 0 :=
+  edegree_eq_zero_iff_isIsolated.not.mpr h.not_isIsolated_left
+
+variable {G u v} in
+theorem Adj.edegree_ne_zero_right (h : G.Adj u v) : G.edegree v ≠ 0 :=
+  h.symm.edegree_ne_zero_left
+
+variable {G v} in
+theorem nontrivial_of_edegree_ne_zero (h : G.edegree v ≠ 0) : Nontrivial V :=
+  nontrivial_of_not_isIsolated <| edegree_eq_zero_iff_isIsolated.not.mp h
+
+theorem edegree_eq_zero_of_subsingleton [Subsingleton V] (G : SimpleGraph V) (v : V) :
+    G.edegree v = 0 := by
+  simp
+
+variable {G v} in
+theorem edegree_eq_one_iff_existsUnique_adj : G.edegree v = 1 ↔ ∃! u, G.Adj v u := by
+  simp [← encard_neighborSet, Set.encard_eq_one, Set.singleton_iff_unique_mem]
+
+variable {G v} in
+theorem edegree_ne_top_iff_finite_neighborSet : G.edegree v ≠ ⊤ ↔ (G.neighborSet v).Finite :=
+  Set.encard_ne_top_iff
+
+theorem edegree_ne_top_of_finite [Finite V] (G : SimpleGraph V) (v : V) : G.edegree v ≠ ⊤ :=
+  edegree_ne_top_iff_finite_neighborSet.mpr <| Set.toFinite _
+
+theorem coe_degree_eq_edegree [Fintype <| G.neighborSet v] : G.degree v = G.edegree v := by
+  simp [encard_neighborSet, ← ncard_neighborSet]
+
+variable {G v} in
+theorem edegree_eq_coe_iff [Fintype <| G.neighborSet v] {n : ℕ} :
+    G.edegree v = n ↔ G.degree v = n := by
+  simp [← coe_degree_eq_edegree]
+
+@[simp]
+theorem toNat_edegree [Fintype <| G.neighborSet v] : (G.edegree v).toNat = G.degree v := by
+  simp [← coe_degree_eq_edegree]
+
+theorem coe_toNat_edegree_eq_self :
+    (G.edegree v).toNat = G.edegree v ↔ (G.neighborSet v).Finite := by
+  simp [edegree_ne_top_iff_finite_neighborSet]
+
+theorem edegree_le_card : G.edegree v ≤ ENat.card V := by
+  grw [← encard_neighborSet, Set.encard_le_card]
+
+variable {v} in
+theorem edegree_lt_card_of_ne_top (h : G.edegree v ≠ ⊤) : G.edegree v < ENat.card V :=
+  edegree_ne_top_iff_finite_neighborSet.mp h |>.encard_lt_card <| G.neighborSet_ne_univ v
+
+@[simp]
+theorem encard_incidenceSet : (G.incidenceSet v).encard = G.edegree v := by
+  classical
+  simp [Set.encard_congr <| G.incidenceSetEquivNeighborSet v]
+
+theorem edegree_le_encard_edgeSet : G.edegree v ≤ G.edgeSet.encard := by
+  grw [← encard_incidenceSet, incidenceSet_subset]
+
+variable {G H} in
+theorem Copy.edegree_le (f : Copy G H) (v : V) : G.edegree v ≤ H.edegree (f v) :=
+  f.mapNeighborSet v |>.encard_le
+
+variable {G H} in
+@[simp]
+theorem Iso.edegree_eq (f : G ≃g H) (v : V) : H.edegree (f v) = G.edegree v :=
+  (Set.encard_congr <| f.mapNeighborSet v).symm
+
+variable {G G'} in
+@[gcongr]
+theorem edegree_mono (hle : G ≤ G') (v : V) : G.edegree v ≤ G'.edegree v :=
+  Copy.ofLE G G' hle |>.edegree_le v
+
+@[simp]
+theorem edegree_top : edegree ⊤ v = ENat.card V - 1 := by
+  rw [← encard_neighborSet, neighborSet_top, ← Set.encard_ne_add_one v, ← Set.compl_singleton_eq]
+  cases Set.encard {v}ᶜ <;> norm_cast
+
+theorem edegree_bot : edegree ⊥ v = 0 := by
+  simp
+
+variable {G} in
+theorem IsRegularOfDegree.edegree_eq [G.LocallyFinite] {d : ℕ} (h : G.IsRegularOfDegree d) (v : V) :
+    G.edegree v = d :=
+  edegree_eq_coe_iff.mpr <| h.degree_eq v
+
+/-- The maximum extended degree of all vertices, or `0` if there are no vertices -/
+noncomputable def maxEDegree : ℕ∞ :=
+  ⨆ v, G.edegree v
+
+/-- The minimum extended degree of all vertices, or `⊤` if there are no vertices -/
+noncomputable def minEDegree : ℕ∞ :=
+  ⨅ v, G.edegree v
+
+theorem maxEDegree_eq_iSup : G.maxEDegree = ⨆ v, G.edegree v := by
+  rfl
+
+theorem minEDegree_eq_iInf : G.minEDegree = ⨅ v, G.edegree v := by
+  rfl
+
+variable {G} in
+@[simp]
+theorem maxEDegree_eq_zero_iff_eq_bot : G.maxEDegree = 0 ↔ G = ⊥ := by
+  simp [maxEDegree_eq_iSup, eq_bot_iff_isIsolated]
+
+variable {G} in
+theorem minEDegree_eq_zero_iff_isIsolated : G.minEDegree = 0 ↔ ∃ v, G.IsIsolated v := by
+  simp [minEDegree_eq_iInf]
+
+variable {G} in
+theorem minEDegree_eq_zero_iff_support_ne : G.minEDegree = 0 ↔ G.support ≠ .univ := by
+  simp [minEDegree_eq_iInf, Set.ne_univ_iff_exists_notMem, notMem_support_iff_isIsolated]
+
+variable {G} in
+theorem maxEDegree_eq_top_iff_lt : G.maxEDegree = ⊤ ↔ ∀ n : ℕ, ∃ v, n < G.edegree v :=
+  WithTop.iSup_eq_top_iff_lt
+
+variable {G} in
+theorem maxEDegree_eq_top_iff_le : G.maxEDegree = ⊤ ↔ ∀ n : ℕ, ∃ v, n ≤ G.edegree v :=
+  WithTop.iSup_eq_top_iff_le
+
+variable {G} in
+theorem minEDegree_eq_top_iff : G.minEDegree = ⊤ ↔ ∀ v, G.edegree v = ⊤ :=
+  iInf_eq_top
+
+theorem exists_edegree_eq_maxEDegree [Nonempty V] (G : SimpleGraph V) (h : G.maxEDegree ≠ ⊤) :
+    ∃ v, G.edegree v = G.maxEDegree :=
+  Set.range_nonempty G.edegree |>.csSup_mem <| ENat.finite_of_sSup_lt_top h.lt_top
+
+theorem exists_edegree_eq_minEDegree [Nonempty V] (G : SimpleGraph V) :
+    ∃ v, G.edegree v = G.minEDegree :=
+  ciInf_mem G.edegree
+
+theorem edegree_le_maxEDegree : G.edegree v ≤ G.maxEDegree :=
+  le_iSup G.edegree v
+
+theorem minEDegree_le_edegree : G.minEDegree ≤ G.edegree v :=
+  iInf_le G.edegree v
+
+variable {G v} in
+theorem maxEDegree_eq_top_of_edegree_eq_top (h : G.edegree v = ⊤) : G.maxEDegree = ⊤ :=
+  eq_top_iff.mpr <| G.edegree_le_maxEDegree v |>.trans_eq' h
+
+variable {G v} in
+theorem minEDegree_eq_zero_of_edegree_eq_zero (h : G.edegree v = 0) : G.minEDegree = 0 :=
+  nonpos_iff_eq_zero.mp <| G.minEDegree_le_edegree v |>.trans_eq h
+
+variable {G} in
+theorem maxEDegree_le_of_forall_edegree_le {n : ℕ∞} (h : ∀ v, G.edegree v ≤ n) : G.maxEDegree ≤ n :=
+  iSup_le h
+
+variable {G} in
+theorem le_minEDegree_of_forall_le_edegree {n : ℕ∞} (h : ∀ v, n ≤ G.edegree v) : n ≤ G.minEDegree :=
+  le_iInf h
+
+@[simp]
+theorem maxEDegree_of_subsingleton [Subsingleton V] (G : SimpleGraph V) : G.maxEDegree = 0 := by
+  simp [maxEDegree_eq_iSup]
+
+@[simp]
+theorem minEDegree_of_isEmpty [IsEmpty V] (G : SimpleGraph V) : G.minEDegree = ⊤ :=
+  iInf_of_empty G.edegree
+
+@[simp]
+theorem minEDegree_of_subsingleton_of_nonempty [Subsingleton V] [Nonempty V] (G : SimpleGraph V) :
+    G.minEDegree = 0 := by
+  simp [minEDegree_eq_iInf]
+
+theorem maxEDegree_ne_top_of_finite [Finite V] (G : SimpleGraph V) : G.maxEDegree ≠ ⊤ :=
+  iSup_ne_top G.edegree_ne_top_of_finite
+
+theorem minEDegree_ne_top_of_finite [Nonempty V] [Finite V] (G : SimpleGraph V) :
+    G.minEDegree ≠ ⊤ := by
+  rw [minEDegree_eq_iInf, ne_eq, iInf_eq_top, not_forall]
+  have ⟨v⟩ := ‹Nonempty V›
+  exact ⟨v, G.edegree_ne_top_of_finite v⟩
+
+theorem coe_maxDegree_eq_maxEDegree [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
+    G.maxDegree = G.maxEDegree := by
+  cases isEmpty_or_nonempty V
+  · simp
+  rw [maxEDegree_eq_iSup, maxDegree, ← Finset.coe_max' <| by simp, Finset.max'_eq_sup',
+    Finset.sup'_image, Finset.sup'_univ_eq_ciSup]
+  simpa [← coe_degree_eq_edegree] using ENat.coe_iSup <| Set.finite_range _ |>.bddAbove
+
+theorem coe_minDegree_eq_minEDegree [Nonempty V] [Fintype V] (G : SimpleGraph V)
+    [DecidableRel G.Adj] : G.minDegree = G.minEDegree := by
+  rw [minEDegree_eq_iInf, minDegree, ← Finset.coe_min' <| by simp, Finset.min'_eq_inf',
+    Finset.inf'_image, Finset.inf'_univ_eq_ciInf]
+  simpa [← coe_degree_eq_edegree] using! ENat.coe_iInf
+
+variable {G} in
+theorem maxEDegree_eq_coe_iff [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ} :
+    G.maxEDegree = n ↔ G.maxDegree = n := by
+  simp [← coe_maxDegree_eq_maxEDegree]
+
+variable {G} in
+theorem minEDegree_eq_coe_iff [Nonempty V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
+    {n : ℕ} : G.minEDegree = n ↔ G.minDegree = n := by
+  simp [← coe_minDegree_eq_minEDegree]
+
+variable {G} in
+theorem minEDegree_eq_coe_iff_of_neZero [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ}
+    [NeZero n] : G.minEDegree = n ↔ G.minDegree = n := by
+  cases isEmpty_or_nonempty V
+  · simpa using NeZero.ne' n
+  simp [← coe_minDegree_eq_minEDegree]
+
+@[simp]
+theorem toNat_maxEDegree [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
+    G.maxEDegree.toNat = G.maxDegree := by
+  simp [← coe_maxDegree_eq_maxEDegree]
+
+@[simp]
+theorem toNat_minEDegree [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
+    G.minEDegree.toNat = G.minDegree := by
+  cases isEmpty_or_nonempty V
+  · simp
+  simp [← coe_minDegree_eq_minEDegree]
+
+variable {G H} in
+theorem IsContained.maxEDegree_le (h : G ⊑ H) : G.maxEDegree ≤ H.maxEDegree := by
+  refine G.maxEDegree_le_of_forall_edegree_le fun v ↦ ?_
+  grw [h.some.edegree_le, edegree_le_maxEDegree]
+
+variable {G H} in
+theorem Copy.minEDegree_le {f : Copy G H} (hf : Function.Surjective f) :
+    G.minEDegree ≤ H.minEDegree := by
+  refine H.le_minEDegree_of_forall_le_edegree fun w ↦ ?_
+  obtain ⟨v, rfl⟩ := hf w
+  grw [← f.edegree_le, ← minEDegree_le_edegree]
+
+variable {G H} in
+theorem Hom.minEDegree_le {f : G →g H} (hf : Function.Bijective f) : G.minEDegree ≤ H.minEDegree :=
+  Copy.minEDegree_le (f := ⟨f, hf.injective⟩) hf.surjective
+
+variable {G H} in
+theorem Iso.maxEDegree_eq (f : G ≃g H) : G.maxEDegree = H.maxEDegree :=
+  f.toEquiv.iSup_congr f.edegree_eq
+
+variable {G H} in
+theorem Iso.minEDegree_eq (f : G ≃g H) : G.minEDegree = H.minEDegree :=
+  f.toEquiv.iInf_congr f.edegree_eq
+
+variable {G G'} in
+@[gcongr]
+theorem maxEDegree_mono (hle : G ≤ G') : G.maxEDegree ≤ G'.maxEDegree :=
+  IsContained.of_le hle |>.maxEDegree_le
+
+variable {G G'} in
+@[gcongr]
+theorem minEDegree_mono (hle : G ≤ G') : G.minEDegree ≤ G'.minEDegree :=
+  Hom.ofLE hle |>.minEDegree_le Function.bijective_id
+
+theorem maxEDegree_le_card : G.maxEDegree ≤ ENat.card V :=
+  G.maxEDegree_le_of_forall_edegree_le G.edegree_le_card
+
+theorem minEDegree_le_card [Nonempty V] (G : SimpleGraph V) : G.minEDegree ≤ ENat.card V := by
+  have ⟨v⟩ := ‹Nonempty V›
+  grw [G.minEDegree_le_edegree v, edegree_le_card]
+
+variable {G} in
+theorem maxEDegree_lt_card_of_ne_top [Nonempty V] (G : SimpleGraph V) (h : G.maxEDegree ≠ ⊤) :
+    G.maxEDegree < ENat.card V := by
+  have ⟨v, hv⟩ := G.exists_edegree_eq_maxEDegree h
+  rw [← hv] at h ⊢
+  exact G.edegree_lt_card_of_ne_top h
+
+variable {G} in
+theorem minEDegree_lt_card_of_ne_top (h : G.minEDegree ≠ ⊤) : G.minEDegree < ENat.card V := by
+  cases isEmpty_or_nonempty V
+  · simp at h
+  have ⟨v, hv⟩ := G.exists_edegree_eq_minEDegree
+  rw [← hv] at h ⊢
+  exact G.edegree_lt_card_of_ne_top h
+
+theorem minEDegree_le_encard_edgeSet [Nonempty V] (G : SimpleGraph V) :
+    G.minEDegree ≤ G.edgeSet.encard := by
+  have ⟨v, hv⟩ := G.exists_edegree_eq_minEDegree
+  exact hv ▸ G.edegree_le_encard_edgeSet v
+
+theorem maxEDegree_le_encard_edgeSet : G.maxEDegree ≤ G.edgeSet.encard :=
+  maxEDegree_le_of_forall_edegree_le G.edegree_le_encard_edgeSet
+
+theorem minEDegree_le_maxEDegree [Nonempty V] (G : SimpleGraph V) :
+    G.minEDegree ≤ G.maxEDegree := by
+  have ⟨v⟩ := ‹Nonempty V›
+  grw [G.minEDegree_le_edegree v, edegree_le_maxEDegree]
+
+@[simp]
+theorem maxEDegree_top : (completeGraph V).maxEDegree = ENat.card V - 1 := by
+  cases isEmpty_or_nonempty V
+  · simp [ENat.card_eq_zero_iff_empty V |>.mpr ‹_›]
+  simp [maxEDegree_eq_iSup]
+
+@[simp]
+theorem minEDegree_top [Nonempty V] : (completeGraph V).minEDegree = ENat.card V - 1 := by
+  simp [minEDegree_eq_iInf]
+
+@[simp]
+theorem maxEDegree_bot : (emptyGraph V).maxEDegree = 0 := by
+  simp [maxEDegree_eq_iSup]
+
+@[simp]
+theorem minEDegree_bot [Nonempty V] : (emptyGraph V).minEDegree = 0 := by
+  simp [minEDegree_eq_iInf]
+
+variable {G} in
+theorem IsRegularOfDegree.maxEDegree_eq [Nonempty V] [G.LocallyFinite] {d : ℕ}
+    (h : G.IsRegularOfDegree d) : G.maxEDegree = d := by
+  simp [maxEDegree_eq_iSup, h.edegree_eq]
+
+variable {G} in
+theorem IsRegularOfDegree.minEDegree_eq [Nonempty V] [G.LocallyFinite] {d : ℕ}
+    (h : G.IsRegularOfDegree d) : G.minEDegree = d := by
+  simp [minEDegree_eq_iInf, h.edegree_eq]
+
+section Induce
+
+variable {s : Set V}
+
+variable {G} in
+theorem edegree_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
+    (G.induce s).edegree v = G.edegree v := by
+  rw [← encard_neighborSet, ← encard_neighborSet, neighborSet_induce,
+    Set.encard_preimage_of_injective_subset_range Subtype.val_injective <| by simpa]
+
+variable {G} in
+theorem maxEDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    (G.induce s).maxEDegree = G.maxEDegree := by
+  apply le_antisymm <| Embedding.induce s |>.isContained.maxEDegree_le
+  refine G.maxEDegree_le_of_forall_edegree_le fun v ↦ ?_
+  by_cases hv : G.IsIsolated v
+  · simp [hv]
+  grw [← edegree_le_maxEDegree _ ⟨v, h <| G.mem_support_iff_not_isIsolated.mpr hv⟩,
+    edegree_induce_of_neighborSet_subset <| G.neighborSet_subset_support v |>.trans h]
+
+variable {G} in
+theorem le_minEDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    G.minEDegree ≤ (G.induce s).minEDegree := by
+  refine le_minEDegree_of_forall_le_edegree fun v ↦ ?_
+  grw [G.minEDegree_le_edegree v, edegree_induce_of_neighborSet_subset]
+  grw [neighborSet_subset_support, h]
+
+end Induce
+
+end SimpleGraph