Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Counting Steiner trees

Lax280166.CountingSteinerTrees · concepts/Lax280166/CountingSteinerTrees.lean · lax-280166

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    On a finite graph with terminals and kk marked vertices, #Steiner Tree counts the sets of exactly kk non-terminal vertices which, with the terminals, induce a connected subgraph.

    Concept map
    9 concepts; 25 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Tactic.FinCases
    2import Mathlib.Order.PiLex
    3import Mathlib.Data.Prod.Lex
    4import Mathlib.Data.Fintype.EquivFin
    5import Mathlib.ModelTheory.Order
    6import Mathlib.ModelTheory.Semantics
    7import Mathlib.ModelTheory.Complexity
    8import Mathlib.Logic.Equiv.Fin.Basic
    9import Mathlib.Data.Fintype.Lattice
    10import Mathlib.Data.Finite.Sigma
    11import Mathlib.Order.Lattice.Nat
    12import Mathlib.Data.Set.Card
    13import Mathlib.Data.Fintype.Pigeonhole
    14import Mathlib.Dynamics.FixedPoints.Basic
    15import Mathlib.ModelTheory.Syntax
    16import Mathlib.Algebra.Order.BigOperators.Group.Finset
    17import Mathlib.Data.Fintype.Card
    18import Mathlib.SetTheory.Cardinal.Finite
    19import Mathlib.Data.Fintype.Sort
    20import Mathlib.Order.Hom.Set
    21import Mathlib.Logic.Equiv.Prod
    22import Lax799700.Steiner
    23import Mathlib.SetTheory.Cardinal.Finite
    24import Lax366625.CountingProblems
    25
    26/-!
    27---
    28title: Counting Steiner trees
    29type: definition
    30---
    31On a finite graph with terminals and kk marked vertices, #Steiner Tree counts
    32the sets of exactly kk non-terminal vertices which, with the terminals,
    33induce a connected subgraph.
    34-/
    35
    36namespace Lax280166.CountingSteinerTrees
    37
    38open Lax799700.Steiner
    39
    40open FirstOrder
    41
    42open Language Structure
    43
    44section Generic
    45
    46variable {A B : Type}
    47
    48/-- The set `S` contains every terminal, is connected, and has exactly as many
    49non-terminals as the `Kp`-marked set has elements. -/
    50def SteinerOfSizeOn (Adjp : A → A → Prop) (Term Kp : A → Prop) (S : A → Prop) : Prop :=
    51 (∀ x, Term x → S x) ∧ ConnectedOn Adjp S ∧
    52 {x | S x ∧ ¬Term x}.ncard = {x | Kp x}.ncard
    53
    54end Generic
    55
    56section Problem
    57
    58variable (A : Type) [steinerGraph.Structure A]
    59
    60/-- The set `S` is a connected set containing every terminal and using exactly
    61as many non-terminals as the marked set has elements, in a finite graph. -/
    62def SteinerOfSize (S : A → Prop) : Prop :=
    63 Finite A ∧ SteinerOfSizeOn (fun a b : A => STAdj a b) (fun a => STTerminal a)
    64 (fun a => STMarked a) S
    65
    66end Problem
    67
    68open Lax366625.CountingProblems
    69
    70/-- **#Steiner Tree**, as a counting problem. -/
    71noncomputable def SharpSteinerTree : CountingProblem Lax799700.Steiner.steinerGraph :=
    72 CountingProblem.ofFun fun A _ =>
    73 Nat.card {S : A → Prop // SteinerOfSize A S}
    74
    75end Lax280166.CountingSteinerTrees
    76
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…