OAI/Combinatorics/SharpRamsey/Marking/AtomEscape.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. lemma OAI.SharpLogRamsey.HighRankBudgets.atom_escape line 15
  2. lemma OAI.SharpLogRamsey.HighRankBudgets.low_hit_budget line 28
  3. theorem OAI.SharpLogRamsey.HighRankBudgets.eventually_polynomial_exp_neg_rpow_lt line 45
  4. def OAI.SharpLogRamsey.HighRankBudgets.error line 70
  5. theorem OAI.SharpLogRamsey.HighRankBudgets.eventually_error line 78
  6. lemma OAI.SharpLogRamsey.SimultaneousExtraction.markov_complement line 113
  7. theorem OAI.SharpLogRamsey.SimultaneousExtraction.simultaneous_mass line 138
  8. def OAI.SharpLogRamsey.SimultaneousExtraction.retained line 148
  9. lemma OAI.SharpLogRamsey.SimultaneousExtraction.retained_mem line 151
  10. theorem OAI.SharpLogRamsey.SimultaneousExtraction.coverage_selection line 155
  11. theorem OAI.SharpLogRamsey.HighRankAssembly.low_hit_with_cutoff line 188
  12. theorem OAI.SharpLogRamsey.HighRankAssembly.coverage_source line 224
  13. theorem OAI.SharpLogRamsey.HighRankAssembly.size_source line 276
  14. lemma OAI.SharpLogRamsey.HighRankAssembly.domain_raw_rows line 309
  15. def OAI.SharpLogRamsey.SimultaneousExtraction.independentWeight line 323
  16. lemma OAI.SharpLogRamsey.SimultaneousExtraction.independent_total line 325
  17. def OAI.SharpLogRamsey.SimultaneousExtraction.missed line 330
  18. lemma OAI.SharpLogRamsey.SimultaneousExtraction.missed_mean line 334
  19. lemma OAI.SharpLogRamsey.SimultaneousExtraction.domain_size_mean line 350
  20. theorem OAI.SharpLogRamsey.SimultaneousExtraction.tuple_extraction line 359
  21. lemma OAI.SharpLogRamsey.HighRankAssembly.row_pair_total line 416
  22. lemma OAI.SharpLogRamsey.HighRankAssembly.decoder_miss_mean line 423
  23. lemma OAI.SharpLogRamsey.HighRankAssembly.row_pair_size line 438
  24. theorem OAI.SharpLogRamsey.HighRankAssembly.extraction_source line 459