FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Degrees.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 0 contain sorry, 0 declared as axioms

Imports (9)
Imported by 2 files
  1. def SimpleGraph.averageDegree The average degree of G line 35 source

    Source documentation

    The average degree of G.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Rat

    Proof uses: HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Fintype.card

    8 instances, coercions and auxiliary constants left out.

    noncomputable def averageDegree (G : SimpleGraph α) [DecidableRel G.Adj] : ℚ  :=
…
  2. def SimpleGraph.degreeMultiset The multiset of degrees of a graph line 39 source

    Source documentation

    The multiset of degrees of a graph.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Multiset, Nat

    Proof uses: Multiset.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.val, Finset.univ

    3 instances, coercions and auxiliary constants left out.

    def degreeMultiset (G : SimpleGraph α) [DecidableRel G.Adj] : Multiset ℕ :=
…
  3. def SimpleGraph.degreeSequence The degree sequence of a graph, sorted in nondecreasing order line 43 source

    Source documentation

    The degree sequence of a graph, sorted in nondecreasing order.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, List, Nat

    Proof uses: Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.val, Finset.univ, LE.le

    10 instances, coercions and auxiliary constants left out.

    noncomputable def degreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ :=
…
  4. def SimpleGraph.degreeSequenceMultiplicity The maximum number of occurrences of any term of the degree sequence of G line 49 source

    Source documentation

    The maximum number of occurrences of any term of the degree sequence of G.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat

    Proof uses: Option.getD, List.max?, List.map, List.count, SimpleGraph.degreeSequence, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

    noncomputable def degreeSequenceMultiplicity (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
  5. def SimpleGraph.edegree line 58 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, ENat

    Proof uses: Set.encard, SimpleGraph.neighborSet

  6. def SimpleGraph.emaxDegree line 61 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, ENat

    Proof uses: iSup, SimpleGraph.edegree

    5 instances, coercions and auxiliary constants left out.

  7. def SimpleGraph.non_edge_neighborhood_card Cardinality of the union of the neighbourhoods of the ends of the non-edge e line 64 source

    Source documentation

    Cardinality of the union of the neighbourhoods of the ends of the non-edge e.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Sym2, Nat

    Proof uses: Equiv, Subtype, Eq, Sym2.lift, Subtype.mk, Finset.card, Union.union, Finset, SimpleGraph.neighborFinset, Membership.mem, Set, SimpleGraph.neighborSet

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    def non_edge_neighborhood_card (G : SimpleGraph α) [DecidableRel G.Adj] (e : Sym2 α) : ℕ :=
…
  8. def SimpleGraph.NG Minimum size of the neighbourhood of a non-edge of G line 69 source

    Source documentation

    Minimum size of the neighbourhood of a non-edge of G.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Real

    Proof uses: Finset, Sym2, SimpleGraph.edgeFinset, Compl.compl, dite, Finset.Nonempty, Nat, Finset.image, SimpleGraph.non_edge_neighborhood_card, Finset.min', Not, Fintype.card

    10 instances, coercions and auxiliary constants left out.

    noncomputable def NG (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
…
  9. def SimpleGraph.S line 77 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, Real

    Proof uses: Nat, Fintype.card, ite, LT.lt, OfNat.ofNat, Multiset, List.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Classical.propDecidable, SimpleGraph.Adj, Finset.toList, Finset.univ, List, Multiset.sort, LE.le, Option.getD, GetElem?.getElem? and 2 more

    21 instances, coercions and auxiliary constants left out.

  10. def SimpleGraph.secondSmallestDegree Documented declaration: secondSmallestDegree line 90 source

    Source documentation

    The second-smallest degree of G's degree sequence — DeLaVina's σ(G) per the WOWII definitions popup (defEntry 65): "order the degree sequence in nondecreasing order d₁ ≤ d₂ ≤ … ≤ dₙ, the second smallest degree of the sequence is the 2nd entry". For graphs with n ≤ 1 we conventionally return 0.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat

    Proof uses: List.getD, SimpleGraph.degreeSequence, OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

    noncomputable def secondSmallestDegree (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
  11. lemma SimpleGraph.exists_distinct_degree_one_of_secondSmallestDegree_eq_one In a nontrivial preconnected finite graph, second-smallest degree one forces two leaves line 95 source

    Source documentation

    In a nontrivial preconnected finite graph, second-smallest degree one forces two leaves.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Preconnected, Eq, Nat, SimpleGraph.secondSmallestDegree, OfNat.ofNat, Exists, And, Ne, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet

    Proof uses: List, SimpleGraph.degreeSequence, LE.le, List.length, Eq.mpr, Fintype.card, id, congrArg, Eq.trans, Multiset.card, Multiset.map, Finset.val, Finset.univ, Multiset.sort, SimpleGraph.degreeSequence.eq_1, Multiset.length_sort, Multiset.card_map, Nat.succ_le_of_lt, Fintype.one_lt_card, List.cons and 57 more

    106 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

    Open to load the checked before-and-after goal states.

    lemma exists_distinct_degree_one_of_secondSmallestDegree_eq_one [Nontrivial α]
    (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Preconnected)
    (hσ : secondSmallestDegree G = 1) :
    ∃ x y : α, x ≠ y ∧ G.degree x = 1 ∧ G.degree y = 1 := by
…

    Mentions: SimpleGraph.secondSmallestDegree

  12. def SimpleGraph.numTrianglesAtVertex The number of triangles (3-cliques) of G incident to vertex v: the number of 3-element cliques containing v line 143 source

    Source documentation

    The number of triangles (3-cliques) of G incident to vertex v: the number of 3-element cliques containing v.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat

    Proof uses: Finset.card, Finset, Finset.filter, Membership.mem, SimpleGraph.cliqueFinset, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

    noncomputable def numTrianglesAtVertex (G : SimpleGraph α) [DecidableRel G.Adj] (v : α) : ℕ :=
…
  13. def SimpleGraph.degreeL2Norm The length of a graph: the square root of the sum of the squares of degrees line 147 source

    Source documentation

    The length of a graph: the square root of the sum of the squares of degrees.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Real

    Proof uses: Real.sqrt, Finset.sum, Finset.univ, HPow.hPow, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, OfNat.ofNat

    11 instances, coercions and auxiliary constants left out.

    noncomputable def degreeL2Norm (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
…
  14. def SimpleGraph.countDegreeK The number of vertices of degree k in G line 151 source

    Source documentation

    The number of vertices of degree k in G.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat

    Proof uses: Finset.card, Finset.filter, Eq, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.univ

    4 instances, coercions and auxiliary constants left out.

    def countDegreeK (G : SimpleGraph α) [DecidableRel G.Adj] (k : ℕ) : ℕ :=
…