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

10 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. def SimpleGraph.lovaszThetaFunction Lovász Theta Function ($\vartheta(G)$) line 38 source

    Source documentation

    Lovász Theta Function ($\vartheta(G)$). The Lovász theta function is defined as: $$\vartheta(G) = \min \lambda_{\max}(A)$$ where the minimum is taken over all real symmetric (Hermitian) matrices $A$ such that:

    • $A_{ii} = 1$ for all $i$ (diagonal entries are $1$), and
    • $A_{ij} = 1$ for all $\{i,j\} \notin E(G)$ (entries corresponding to non-edges are $1$).

    Here $\lambda_{\max}(A)$ denotes the maximum eigenvalue of $A$.

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

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

    Proof uses: InfSet.sInf, Set.ofPred, Exists, Matrix, Matrix.IsHermitian, Eq, OfNat.ofNat, Not, Matrix.IsHermitian.maxEigenvalue

    15 instances, coercions and auxiliary constants left out.

    noncomputable def lovaszThetaFunction
    (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
…
  2. theorem SimpleGraph.lovaszThetaFunction_isEmpty The Lovász theta function of a graph on an empty vertex type is $0$ line 44 source

    Source documentation

    The Lovász theta function of a graph on an empty vertex type is $0$.

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

    Statement uses: Fintype, DecidableEq, IsEmpty, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Real, SimpleGraph.lovaszThetaFunction, OfNat.ofNat

    Proof uses: Set, Set.ofPred, Exists, Matrix, Matrix.IsHermitian, Not, Matrix.IsHermitian.maxEigenvalue, Singleton.singleton, Set.ext, Eq.mpr, Iff, Membership.mem, id, congrArg, Iff.intro, of_eq_true, Eq.trans, True, congrFun', Real.iSup_of_isEmpty and 10 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    theorem lovaszThetaFunction_isEmpty [IsEmpty α] (G : SimpleGraph α) [DecidableRel G.Adj] :
    lovaszThetaFunction G = 0 := by
…

    Mentions: SimpleGraph.lovaszThetaFunction

  3. lemma SimpleGraph.one_le_maxEigenvalue_of_diag_eq_one line 59 source

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

    Statement uses: Fintype, DecidableEq, Nonempty, Matrix, Real, Matrix.IsHermitian, Eq, OfNat.ofNat, LE.le, Matrix.IsHermitian.maxEigenvalue

    Proof uses: Fintype.card, Finset.sum, Finset.univ, Matrix.IsHermitian.eigenvalues, Matrix.trace, Matrix.IsHermitian.trace_eq_sum_eigenvalues, Eq.mp, congr, congrArg, Eq.trans, Matrix.diag, HSMul.hSMul, Nat, Finset.card, funext, Finset.sum_const, HMul.hMul, nsmul_eq_mul, mul_one, Finset.sum_congr and 14 more

    92 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  4. lemma SimpleGraph.bddBelow_lovaszThetaSet line 73 source

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, BddBelow, Real, Set.ofPred, Exists, Matrix, Matrix.IsHermitian, Eq, OfNat.ofNat, Not, Matrix.IsHermitian.maxEigenvalue

    Proof uses: dite, Nonempty, Classical.propDecidable, Exists.intro, Membership.mem, Set, lowerBounds, LE.le, SimpleGraph.one_le_maxEigenvalue_of_diag_eq_one, of_eq_true, Eq.trans, True, congrArg, Real.iSup_of_isEmpty, Eq.mp, IsEmpty, propext, not_nonempty_iff, Matrix.IsHermitian.eigenvalues

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  5. lemma SimpleGraph.nonempty_lovaszThetaSet line 85 source

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Set.Nonempty, Real, Set.ofPred, Exists, Matrix, Matrix.IsHermitian, Eq, OfNat.ofNat, Not, Matrix.IsHermitian.maxEigenvalue

    Proof uses: Equiv, Matrix.of, Matrix.ext, Matrix.conjTranspose, of_eq_true, Eq.trans, True, congrFun', congrArg, TrivialStar.star_trivial, eq_self, Exists.intro, Membership.mem, Set, rfl

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  6. theorem SimpleGraph.one_le_lovaszThetaFunction The Lovász theta function of any nonempty graph is at least $1$ line 95 source

    Source documentation

    The Lovász theta function of any nonempty graph is at least $1$.

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

    Statement uses: Fintype, DecidableEq, Nonempty, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, OfNat.ofNat, SimpleGraph.lovaszThetaFunction

    Proof uses: le_csInf, Set.ofPred, Exists, Matrix, Matrix.IsHermitian, Eq, Not, Matrix.IsHermitian.maxEigenvalue, SimpleGraph.nonempty_lovaszThetaSet, Membership.mem, Set, SimpleGraph.one_le_maxEigenvalue_of_diag_eq_one

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    theorem one_le_lovaszThetaFunction [Nonempty α] (G : SimpleGraph α) [DecidableRel G.Adj] :
    1 ≤ lovaszThetaFunction G := by
…

    Mentions: SimpleGraph.lovaszThetaFunction

  7. theorem SimpleGraph.lovaszThetaFunction_anti Adding edges to a graph can only decrease or preserve its Lovász theta function line 102 source

    Source documentation

    Adding edges to a graph can only decrease or preserve its Lovász theta function.

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, SimpleGraph.lovaszThetaFunction

    Proof uses: csInf_le_csInf, Set.ofPred, Exists, Matrix, Matrix.IsHermitian, Eq, OfNat.ofNat, Not, Matrix.IsHermitian.maxEigenvalue, SimpleGraph.bddBelow_lovaszThetaSet, SimpleGraph.nonempty_lovaszThetaSet, Membership.mem, Set, Exists.intro, rfl

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    theorem lovaszThetaFunction_anti {G H : SimpleGraph α} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (h : G ≤ H) :
    lovaszThetaFunction H ≤ lovaszThetaFunction G := by
…

    Mentions: SimpleGraph.lovaszThetaFunction

  8. theorem SimpleGraph.lovaszThetaFunction_top The Lovász theta function of the complete graph $K_n$ ($n \ge 1$) is $1$ line 110 source

    Source documentation

    The Lovász theta function of the complete graph $K_n$ ($n \ge 1$) is $1$.

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

    Statement uses: Fintype, DecidableEq, Nonempty, Eq, Real, SimpleGraph.lovaszThetaFunction, Top.top, SimpleGraph, OfNat.ofNat

    Proof uses: le_antisymm, Matrix.IsHermitian, Matrix, Matrix.isHermitian_one, Membership.mem, Set, Set.ofPred, Exists, Not, SimpleGraph.Adj, Matrix.IsHermitian.maxEigenvalue, Exists.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, Matrix.one_apply_eq, eq_self, Eq.mp and 88 more

    146 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

    theorem lovaszThetaFunction_top [Nonempty α] :
    lovaszThetaFunction (⊤ : SimpleGraph α) = 1 := by
…

    Mentions: SimpleGraph.lovaszThetaFunction

  9. theorem SimpleGraph.lovaszThetaFunction_bot The Lovász theta function of the edgeless graph $\overline{K_n}$ is $n$ line 135 source

    Source documentation

    The Lovász theta function of the edgeless graph $\overline{K_n}$ is $n$.

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

    Statement uses: Fintype, DecidableEq, Eq, Real, SimpleGraph.lovaszThetaFunction, Bot.bot, SimpleGraph, Fintype.card

    Proof uses: dite, Nonempty, Classical.propDecidable, Matrix, Equiv, Matrix.of, OfNat.ofNat, Matrix.IsHermitian, Matrix.ext, Matrix.conjTranspose, of_eq_true, Eq.trans, True, congrFun', congrArg, TrivialStar.star_trivial, eq_self, Set, Set.ofPred, Exists and 123 more

    174 instances, coercions and auxiliary constants left out.

    Tactic trace: 75 steps

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

    theorem lovaszThetaFunction_bot :
    lovaszThetaFunction (⊥ : SimpleGraph α) = Fintype.card α := by
…

    Mentions: SimpleGraph.lovaszThetaFunction

  10. theorem SimpleGraph.lovaszThetaFunction_le_card The Lovász theta function of any graph is at most its number of vertices line 204 source

    Source documentation

    The Lovász theta function of any graph is at most its number of vertices.

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, SimpleGraph.lovaszThetaFunction, Fintype.card

    Proof uses: LE.le.trans_eq, Bot.bot, SimpleGraph.lovaszThetaFunction_anti, bot_le, SimpleGraph.lovaszThetaFunction_bot

    15 instances, coercions and auxiliary constants left out.

    theorem lovaszThetaFunction_le_card (G : SimpleGraph α) [DecidableRel G.Adj] :
    lovaszThetaFunction G ≤ Fintype.card α :=
…

    Mentions: SimpleGraph.lovaszThetaFunction