FormalConjecturesForMathlib/Combinatorics/SimpleGraph/WienerIndex.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

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. def SimpleGraph.wienerIndex The Wiener index of G, which is the sum of distances between all pairs of vertices line 28 source

    Source documentation

    The Wiener index of G, which is the sum of distances between all pairs of vertices.

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

    Statement uses: Fintype, SimpleGraph, Nat

    Proof uses: Finset.sum, Sym2, Finset.univ, Equiv, Subtype, Eq, Sym2.lift, Subtype.mk, SimpleGraph.dist

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    noncomputable def wienerIndex (G : SimpleGraph α) : ℕ :=
…
  2. def SimpleGraph.computable_wiener Computable Wiener index: half the sum of all ordered pairwise distances line 32 source

    Source documentation

    Computable Wiener index: half the sum of all ordered pairwise distances.

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

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

    Proof uses: HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.computable_dist, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

    def computable_wiener (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
  3. lemma SimpleGraph.double_sum_eq_two_mul_sym2_sum Helper: ∑∑ f = 2 * ∑ Sym2 (lift f) when f symmetric with f(a,a) = 0 line 37 source

    Source comment

    Helper: ∑∑ f = 2 * ∑ Sym2 (lift f) when f symmetric with f(a,a) = 0
    private lemma double_sum_eq_two_mul_sym2_sum {f : α → α → ℕ}
    (hf : ∀ a b, f a b = f b a) (hd : ∀ a, f a a = 0) :
    ∑ u : α, ∑ v : α, f u v =
    2 * ∑ x : Sym2 α, Sym2.lift ⟨f, fun a b => hf a b⟩ x := by
…

    Mentions: SimpleGraph.b

  4. theorem SimpleGraph.wiener_eq_computable line 84 source

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.wienerIndex, SimpleGraph.computable_wiener

    Proof uses: id, Finset.sum, Sym2, Finset.univ, Equiv, Subtype, Sym2.lift, Subtype.mk, SimpleGraph.dist, SimpleGraph.computable_dist, Eq.mpr, congrArg, Eq.symm, SimpleGraph.dist_eq_computable, SimpleGraph.dist_comm, Eq.refl, OfNat.ofNat, of_eq_true, Eq.trans, True and 17 more

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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