OAI/Combinatorics/MatchingPSD/Model.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectMatchingPSD.Edge line 7

    Also declared: ComparatorChallenges/MatchingAffineLift.lean:7 (same declaration text), ComparatorChallenges/MatchingPSD.lean:7 (same declaration text).

  2. def OAI.PerfectMatchingPSD.IsPerfectMatching line 9

    Also declared: ComparatorChallenges/MatchingAffineLift.lean:9 (same declaration text), ComparatorChallenges/MatchingPSD.lean:9 (same declaration text).

  3. abbrev OAI.PerfectMatchingPSD.PerfectMatching line 12

    Also declared: ComparatorChallenges/MatchingAffineLift.lean:12 (same declaration text), ComparatorChallenges/MatchingPSD.lean:12 (same declaration text).

  4. abbrev OAI.PerfectMatchingPSD.OddCut line 15

    Also declared: ComparatorChallenges/MatchingPSD.lean:15 (same declaration text).

  5. abbrev OAI.PerfectMatchingPSD.Row line 17

    Also declared: ComparatorChallenges/MatchingPSD.lean:17 (same declaration text).

  6. def OAI.PerfectMatchingPSD.Crosses line 19

    Also declared: ComparatorChallenges/MatchingPSD.lean:19 (same declaration text).

  7. def OAI.PerfectMatchingPSD.crossingCount line 22

    Also declared: ComparatorChallenges/MatchingPSD.lean:22 (same declaration text).

  8. def OAI.PerfectMatchingPSD.slack line 27

    Also declared: ComparatorChallenges/MatchingPSD.lean:27 (same declaration text).

  9. def OAI.PerfectMatchingPSD.HasFactorization line 34

    Source documentation

    Real PSD factors of order r, without equivariance or rank-one restrictions.

    Also declared: ComparatorChallenges/MatchingPSD.lean:34 (same declaration text).

    def HasFactorization (n r : ℕ) : Prop :=
…
  10. def OAI.PerfectMatchingPSD.psdRank line 41

    Source documentation

    The least positive order of a real PSD factorization.

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

    noncomputable def psdRank (n : ℕ) : ℕ :=
…
  11. def OAI.PerfectMatchingPSD.MainClaim line 46

    Source documentation

    Every positive real power is eventually smaller than the PSD rank, uniformly over all even vertex counts. The exponentiation is real rpow.

    Also declared: ComparatorChallenges/MatchingPSD.lean:46 (same declaration text).

    def MainClaim : Prop :=
…