OAI/Combinatorics/RamseyFive/Trees/TreeOriginalTrims.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.TreeCodec.capLeft line 18
  2. def OAI.SharpRamseyFive.TreeCodec.capRight line 20
  3. theorem OAI.SharpRamseyFive.TreeCodec.first_context_eviction line 23
  4. theorem OAI.SharpRamseyFive.TreeCodec.second_context_eviction line 51
  5. theorem OAI.SharpRamseyFive.TreeCodec.first_original_trim line 79
  6. theorem OAI.SharpRamseyFive.TreeCodec.second_original_trim line 92
  7. def OAI.SharpRamseyFive.TreeCodec.pathSum line 112
  8. lemma OAI.SharpRamseyFive.TreeCodec.pathSum_zero line 118
  9. lemma OAI.SharpRamseyFive.TreeCodec.pathSum_mono line 127
  10. lemma OAI.SharpRamseyFive.TreeCodec.pathSum_const_le_height line 137
  11. lemma OAI.SharpRamseyFive.TreeCodec.mean_pathSum line 157
  12. def OAI.SharpRamseyFive.TreeCodec.abortAt line 173
  13. def OAI.SharpRamseyFive.TreeCodec.successAt line 175
  14. theorem OAI.SharpRamseyFive.TreeCodec.missing_path_eq line 179
  15. lemma OAI.SharpRamseyFive.TreeCodec.missing_mass_path line 201
  16. theorem OAI.SharpRamseyFive.TreeCodec.missing_mass_le line 210