OAI/Combinatorics/MatchingEntropy/Simplex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatchingEntropyBounds.probabilitySimplex_eq_range line 13
2. theorem OAI.MatchingEntropyBounds.convex_probabilitySimplex line 20
3. theorem OAI.MatchingEntropyBounds.single_mem_probabilitySimplex line 31
4. theorem OAI.MatchingEntropyBounds.mem_Icc_of_mem_probabilitySimplex line 39
5. theorem OAI.MatchingEntropyBounds.isCompact_probabilitySimplex line 46