OAI/Combinatorics/PerfectMatching/Basic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite loopless multigraphs, perfect matching indicators, and their convex hull. The edge type distinguishes parallel edges. Feasible laws are probability vectors on perfect matchings with a prescribed mean.

  1. instance OAI.MatchingEntropy.LooplessGraph.incidentDecidable line 23
  2. def OAI.MatchingEntropy.LooplessGraph.indicator line 26

    Also declared: ComparatorChallenges/MatchingEntropy.lean:35 (same declaration text).

  3. def OAI.MatchingEntropy.LooplessGraph.polytope line 29

    Also declared: ComparatorChallenges/MatchingEntropy.lean:38 (same declaration text).

  4. def OAI.MatchingEntropy.LooplessGraph.mean line 32

    Also declared: ComparatorChallenges/MatchingEntropy.lean:41 (same declaration text).

  5. def OAI.MatchingEntropy.LooplessGraph.feasibleLaws line 35

    Distinct definitions of this name: ComparatorChallenges/MatchingEntropy.lean:44 (same statement text; different proof or body). Qualify references as OAI.MatchingEntropy.LooplessGraph.feasibleLaws@path.

  6. theorem OAI.MatchingEntropy.LooplessGraph.indicator_nonneg line 39
  7. theorem OAI.MatchingEntropy.LooplessGraph.indicator_le_one line 45
  8. theorem OAI.MatchingEntropy.LooplessGraph.continuous_mean line 51
  9. def OAI.MatchingEntropy.LooplessGraph.meanLinear line 55
  10. theorem OAI.MatchingEntropy.LooplessGraph.mean_mem_polytope line 65
  11. theorem OAI.MatchingEntropy.LooplessGraph.mean_single line 76
  12. theorem OAI.MatchingEntropy.LooplessGraph.mem_polytope_iff line 84

    Source documentation

    Exact equivalence between the convex hull of matching indicators and feasible finite laws.

    theorem mem_polytope_iff (G : LooplessGraph V E) (y : E → ℝ) :
    y ∈ G.polytope ↔ (G.feasibleLaws y).Nonempty := by
…
  13. theorem OAI.MatchingEntropy.LooplessGraph.compact_feasibleLaws line 100
  14. theorem OAI.MatchingEntropy.LooplessGraph.compact_polytope line 106