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

[SnirBroshi]

Define ENat versions of degree/minDegree/maxDegree called edegree/minEDegree/maxEDegree respectively.

The e prefix matches the existing edist/ediam/egirth.

---

TODO (future work): tsum G.edegree = 2 * G.edgeSet.encard and then ENat.card V * G.minEDegree ≤ 2 * G.edgeSet.encard ≤ ENat.card V * G.maxEDegree (can we avoid topology somehow?)

• depends on: [Merged by Bors] - feat: interactions between IsSuccLimit and WithTop #38244
• depends on: [Merged by Bors] - feat(Data/Set): singleton_iff_unique_mem and Finite.encard_lt_card #38354
• depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/Copy): maxDegree is monotonic, and minDegree is monotonic over a surjective Copy #38355
• depends on: [Merged by Bors] - feat(Order/ConditionallyCompleteLattice/Finset): sSup s ≠ ⊤ in a CompleteLinearOrder for a finite set without ⊤ #38356
• depends on: feat(Order/SuccPred/CompleteLinearOrder): sSup s < x iff theorems when we know if x is a successor pre-limit or not #38612
• depends on: feat(Order/SuccPred/CompleteLinearOrder): sSup s = ⊤ iff theorems for WithTop #40620
• depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/Basic): more neighborSet and IsIsolated lemmas #38747
• depends on: feat(Combinatorics/SimpleGraph/Finite): Set.ncard of neighborSet #40624

Note: this PR used to be a refactor of the existing degree/maxDegree/minDegree, see the edits of this description.

[github-actions]

PR summary e73d6ccd06

Import changes exceeding 2%

%	File
+33.39%	Mathlib.Combinatorics.SimpleGraph.Finite
+9.73%	Mathlib.Combinatorics.SimpleGraph.IncMatrix
+30.59%	Mathlib.Combinatorics.SimpleGraph.Subgraph

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Finite	581	775	+194 (+33.39%)
Mathlib.Combinatorics.SimpleGraph.Subgraph	595	777	+182 (+30.59%)
Mathlib.Combinatorics.SimpleGraph.IncMatrix	812	891	+79 (+9.73%)

Import changes for all files

Files	Import difference
10 files Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite	1
Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic	59
Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Metric	75
Mathlib.Combinatorics.SimpleGraph.IncMatrix	79
Mathlib.Combinatorics.SimpleGraph.Extremal.Basic	100
3 files Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Finsubgraph	133
Mathlib.Combinatorics.SimpleGraph.Trails	151
Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.LineGraph	179
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected	180
Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Subgraph	182
4 files Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Paths Mathlib.Combinatorics.SimpleGraph.Walk.Counting Mathlib.Combinatorics.SimpleGraph.Walks.Counting	186
9 files Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp Mathlib.Combinatorics.SimpleGraph.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Walk.Decomp Mathlib.Combinatorics.SimpleGraph.Walk.Maps Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks Mathlib.Combinatorics.SimpleGraph.Walks.Decomp Mathlib.Combinatorics.SimpleGraph.Walks.Maps Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks	188
Mathlib.Combinatorics.SimpleGraph.DeleteEdges	189
Mathlib.Combinatorics.SimpleGraph.Finite	194
Mathlib.Combinatorics.SimpleGraph.Degree (new file)	790

---

Declarations diff (regex)

+ Adj.edegree_ne_zero_left
+ Adj.edegree_ne_zero_right
+ Copy.edegree_le
+ Copy.minEDegree_le
+ Hom.minEDegree_le
+ IsContained.maxEDegree_le
+ IsIsolated.edegree_eq
+ IsRegularOfDegree.edegree_eq
+ IsRegularOfDegree.maxEDegree_eq
+ IsRegularOfDegree.minEDegree_eq
+ Iso.edegree_eq
+ Iso.maxEDegree_eq
+ Iso.minEDegree_eq
+ Order.IsSuccPrelimit.le_sSup_iff
+ coe_degree_eq_edegree
+ coe_maxDegree_eq_maxEDegree
+ coe_minDegree_eq_minEDegree
+ coe_toNat_edegree_eq_self
+ edegree
+ edegree_bot
+ edegree_eq_coe_iff
+ edegree_eq_one_iff_existsUnique_adj
+ edegree_eq_zero_iff_isIsolated
+ edegree_eq_zero_of_subsingleton
+ edegree_induce_of_neighborSet_subset
+ edegree_le_card
+ edegree_le_encard_edgeSet
+ edegree_le_maxEDegree
+ edegree_lt_card_of_ne_top
+ edegree_mono
+ edegree_ne_top_iff_finite_neighborSet
+ edegree_ne_top_of_finite
+ edegree_top
+ encard_commonNeighbors_top
+ encard_incidenceSet
+ encard_neighborSet
+ exists_edegree_eq_maxEDegree
+ exists_edegree_eq_minEDegree
+ forall_bot_lt
+ iSup_eq_top_iff_le
+ iSup_eq_top_iff_lt
+ le_minEDegree_induce_of_support_subset
+ le_minEDegree_of_forall_le_edegree
+ maxEDegree
+ maxEDegree_bot
+ maxEDegree_eq_coe_iff
+ maxEDegree_eq_iSup
+ maxEDegree_eq_top_iff_le
+ maxEDegree_eq_top_iff_lt
+ maxEDegree_eq_top_of_edegree_eq_top
+ maxEDegree_eq_zero_iff_eq_bot
+ maxEDegree_induce_of_support_subset
+ maxEDegree_le_card
+ maxEDegree_le_encard_edgeSet
+ maxEDegree_le_of_forall_edegree_le
+ maxEDegree_lt_card_of_ne_top
+ maxEDegree_mono
+ maxEDegree_ne_top_of_finite
+ maxEDegree_of_subsingleton
+ maxEDegree_top
+ minEDegree
+ minEDegree_bot
+ minEDegree_eq_coe_iff
+ minEDegree_eq_coe_iff_of_neZero
+ minEDegree_eq_iInf
+ minEDegree_eq_top_iff
+ minEDegree_eq_zero_iff_isIsolated
+ minEDegree_eq_zero_iff_support_ne
+ minEDegree_eq_zero_of_edegree_eq_zero
+ minEDegree_le_card
+ minEDegree_le_edegree
+ minEDegree_le_encard_edgeSet
+ minEDegree_le_maxEDegree
+ minEDegree_lt_card_of_ne_top
+ minEDegree_mono
+ minEDegree_ne_top_of_finite
+ minEDegree_of_isEmpty
+ minEDegree_of_subsingleton_of_nonempty
+ minEDegree_top
+ ncard_neighborSet
+ nontrivial_of_edegree_ne_zero
+ sSup_eq_top_iff_le
+ sSup_eq_top_iff_lt
+ toNat_edegree
+ toNat_maxEDegree
+ toNat_minEDegree

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e73d6cc).

• +87 new declarations
• −0 removed declarations

+Order.IsSuccPrelimit.le_sSup_iff
+SimpleGraph.Adj.edegree_ne_zero_left
+SimpleGraph.Adj.edegree_ne_zero_right
+SimpleGraph.Copy.edegree_le
+SimpleGraph.Copy.minEDegree_le
+SimpleGraph.Hom.minEDegree_le
+SimpleGraph.IsContained.maxEDegree_le
+SimpleGraph.IsIsolated.edegree_eq
+SimpleGraph.IsRegularOfDegree.edegree_eq
+SimpleGraph.IsRegularOfDegree.maxEDegree_eq
+SimpleGraph.IsRegularOfDegree.minEDegree_eq
+SimpleGraph.Iso.edegree_eq
+SimpleGraph.Iso.maxEDegree_eq
+SimpleGraph.Iso.minEDegree_eq
+SimpleGraph.coe_degree_eq_edegree
+SimpleGraph.coe_maxDegree_eq_maxEDegree
+SimpleGraph.coe_minDegree_eq_minEDegree
+SimpleGraph.coe_toNat_edegree_eq_self
+SimpleGraph.edegree
+SimpleGraph.edegree_bot
+SimpleGraph.edegree_eq_coe_iff
+SimpleGraph.edegree_eq_one_iff_existsUnique_adj
+SimpleGraph.edegree_eq_zero_iff_isIsolated
+SimpleGraph.edegree_eq_zero_of_subsingleton
+SimpleGraph.edegree_induce_of_neighborSet_subset
+SimpleGraph.edegree_le_card
+SimpleGraph.edegree_le_encard_edgeSet
+SimpleGraph.edegree_le_maxEDegree
+SimpleGraph.edegree_lt_card_of_ne_top
+SimpleGraph.edegree_mono
+SimpleGraph.edegree_ne_top_iff_finite_neighborSet
+SimpleGraph.edegree_ne_top_of_finite
+SimpleGraph.edegree_top
+SimpleGraph.encard_commonNeighbors_top
+SimpleGraph.encard_incidenceSet
+SimpleGraph.encard_neighborSet
+SimpleGraph.exists_edegree_eq_maxEDegree
+SimpleGraph.exists_edegree_eq_minEDegree
+SimpleGraph.le_minEDegree_induce_of_support_subset
+SimpleGraph.le_minEDegree_of_forall_le_edegree
+SimpleGraph.maxEDegree
+SimpleGraph.maxEDegree_bot
+SimpleGraph.maxEDegree_eq_coe_iff
+SimpleGraph.maxEDegree_eq_iSup
+SimpleGraph.maxEDegree_eq_top_iff_le
+SimpleGraph.maxEDegree_eq_top_iff_lt
+SimpleGraph.maxEDegree_eq_top_of_edegree_eq_top
+SimpleGraph.maxEDegree_eq_zero_iff_eq_bot
+SimpleGraph.maxEDegree_induce_of_support_subset
+SimpleGraph.maxEDegree_le_card
+SimpleGraph.maxEDegree_le_encard_edgeSet
+SimpleGraph.maxEDegree_le_of_forall_edegree_le
+SimpleGraph.maxEDegree_lt_card_of_ne_top
+SimpleGraph.maxEDegree_mono
+SimpleGraph.maxEDegree_ne_top_of_finite
+SimpleGraph.maxEDegree_of_subsingleton
+SimpleGraph.maxEDegree_top
+SimpleGraph.minEDegree
+SimpleGraph.minEDegree_bot
+SimpleGraph.minEDegree_eq_coe_iff
+SimpleGraph.minEDegree_eq_coe_iff_of_neZero
+SimpleGraph.minEDegree_eq_iInf
+SimpleGraph.minEDegree_eq_top_iff
+SimpleGraph.minEDegree_eq_zero_iff_isIsolated
+SimpleGraph.minEDegree_eq_zero_iff_support_ne
+SimpleGraph.minEDegree_eq_zero_of_edegree_eq_zero
+SimpleGraph.minEDegree_le_card
+SimpleGraph.minEDegree_le_edegree
+SimpleGraph.minEDegree_le_encard_edgeSet
+SimpleGraph.minEDegree_le_maxEDegree
+SimpleGraph.minEDegree_lt_card_of_ne_top
+SimpleGraph.minEDegree_mono
+SimpleGraph.minEDegree_ne_top_of_finite
+SimpleGraph.minEDegree_of_isEmpty
+SimpleGraph.minEDegree_of_subsingleton_of_nonempty
+SimpleGraph.minEDegree_top
+SimpleGraph.ncard_neighborSet
+SimpleGraph.nontrivial_of_edegree_ne_zero
+SimpleGraph.toNat_edegree
+SimpleGraph.toNat_maxEDegree
+SimpleGraph.toNat_minEDegree
+WithBot.forall_bot_lt
+WithTop.forall_lt_top
+WithTop.iSup_eq_top_iff_le
+WithTop.iSup_eq_top_iff_lt
+WithTop.sSup_eq_top_iff_le
+WithTop.sSup_eq_top_iff_lt

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e73d6ccd06
Reference commit 3dffaf2f18

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[b-mehta]

I'm not sure that this change is the right way to achieve degrees for infinite graphs. Instead, we should change degree v to ask that the neighbourhood of v is a fintype. I agree it's bad to ask for finiteness of the entire vertex set, but I don't think this is the right way to go about fixing it.

[SnirBroshi]

Instead, we should change degree v to ask that the neighbourhood of v is a fintype. I agree it's bad to ask for finiteness of the entire vertex set

Isn't that how degrees are currently defined? (they require Fintype <| G.neighborSet v)

I disagree that Fintype <| G.neighborSet v is the correct way, that makes it very hard to work with infinite graphs.
I'm not asking for cardinals, just to avoid this hypothesis. Like in other places in Mathilb, if we add a junk value of 0 when the neighborhood isn't finite that'll make things much easier. This is why I suggest G.neighborSet v |>.ncard.
Like division by zero, I don't want to justify Fintype every time I talk about the degree of a vertex.

[b-mehta]

Isn't that how degrees are currently defined? (they require Fintype <| G.neighborSet v)

Oops, yes, the only way I could imagine infinite graphs being difficult was with a worse definition than this one!

that makes it very hard to work with infinite graphs.

Do you have examples of where this makes it hard to talk about infinite graphs? In my experience, infinite graphs work quite nicely with this setup. This is the general pattern in Lean combinatorics, more generally. Since the Fintype is an instance argument, most of the time it doesn't need to be explicitly justified anyway.

[SnirBroshi]

I'm pretty baffled at why "junk values are better than dragging hypotheses around" isn't a good reason for the change, I thought that's the conventional wisdom in Mathlib.

Do you have examples of where this makes it hard to talk about infinite graphs? In my experience, infinite graphs work quite nicely with this setup.

Take any statement from https://loogle.lean-lang.org/?q=SimpleGraph.degree and try to apply it to an infinite graph. There's no reason why statements such as nontrivial_of_degree_ne_zero or degree_eq_one_iff_existsUnique_adj should require me to first prove that the vertex doesn't have too much neighbors.

Another random example I just thought of: "a graph is Hamiltonian 2-regular iff it's isomorphic to a cycle" is impossible to state for infinite graphs right now, even if we make IsHamiltonian not require a [Fintype V]:

theorem foo {V : Type*} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
    G.IsHamiltonian ∧ G.IsRegularOfDegree 2 ↔ Nonempty (G ≃g SimpleGraph.cycleGraph (Nat.card V)) := by
  sorry

Another user with a similar frustration: #graph theory > IsRegularOfDegree without DecidableRel @ 💬

But most importantly: minDegree and maxDegree require [Fintype V] [DecidableRel G.Adj], which means there's no way to use them in infinite graphs, even if I reluctantly prove an instance of G.LocallyFinite.

This is the general pattern in Lean combinatorics, more generally. Since the Fintype is an instance argument, most of the time it doesn't need to be explicitly justified anyway.

I don't understand how your fintypes don't have to be justified. Do you have such instances in your local context, or do you only use degrees on Fintype V? I'm really not sure where such instances should automagically come from, they don't for me.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.