OAI/Combinatorics/MatchingPSD/Parameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PerfectMatchingPSD.blockSize line 9
2. def OAI.PerfectMatchingPSD.vertexSize line 10
3. lemma OAI.PerfectMatchingPSD.index_le_vertexSize line 12
4. lemma OAI.PerfectMatchingPSD.vertexSize_succ_bound line 22
5. lemma OAI.PerfectMatchingPSD.vertexSize_succ_le_pow6 line 33
6. lemma OAI.PerfectMatchingPSD.bracket_vertexSize line 40
7. lemma OAI.PerfectMatchingPSD.exists_padded_global_equiv line 53
8. lemma OAI.PerfectMatchingPSD.eventually_pow_lt_half_exp line 63