OAI/Combinatorics/PerfectMatching/Simplex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Probability vectors on finite types, with their convexity and compactness properties. The function-space simplex is the range of the weights of Convexity.StdSimplex.

  1. def OAI.MatchingEntropy.probabilitySimplex line 17

    Source documentation

    Nonnegative real weights with total mass one.

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

    def probabilitySimplex (Index : Type*) [Fintype Index] : Set (Index → ℝ) :=
…
  2. theorem OAI.MatchingEntropy.probabilitySimplex_eq_range line 20
  3. theorem OAI.MatchingEntropy.convex_probabilitySimplex line 27
  4. theorem OAI.MatchingEntropy.single_mem_probabilitySimplex line 38
  5. theorem OAI.MatchingEntropy.probabilitySimplex_le_one line 46
  6. theorem OAI.MatchingEntropy.isCompact_probabilitySimplex line 51