OAI/Combinatorics/MatchingEntropy/SharpRank.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingEntropyBounds.Refined.quotient_finrank_shared line 19
  2. def OAI.MatchingEntropyBounds.Refined.lowerObjective line 61
  3. theorem OAI.MatchingEntropyBounds.Refined.positiveExtension_self line 66
  4. def OAI.MatchingEntropyBounds.Refined.boundaryLinear line 73
  5. theorem OAI.MatchingEntropyBounds.Refined.boundaryLinear_restriction line 79
  6. theorem OAI.MatchingEntropyBounds.Refined.boundaryLinear_face line 86
  7. theorem OAI.MatchingEntropyBounds.Refined.faceCodimension_le_sides_shared line 91
  8. theorem OAI.MatchingEntropyBounds.Refined.incident_of_card_two line 114
  9. theorem OAI.MatchingEntropyBounds.Refined.faceCodimension_two line 124
  10. theorem OAI.MatchingEntropyBounds.Refined.sharp_face_rank_aux line 144
  11. theorem OAI.MatchingEntropyBounds.Refined.sharp_face_rank line 188