OAI/Combinatorics/SharpRamsey/Marking/RawLowerTail.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. lemma OAI.SharpLogRamsey.HighRankCoverageProbability.raw_lower_tail line 19
  2. theorem OAI.SharpLogRamsey.HighRankCoverageProbability.fixed_query_bound line 31
  3. theorem OAI.SharpLogRamsey.HighRankAveraged.excess_average line 78
  4. theorem OAI.SharpLogRamsey.HighRankAveraged.averaged_coverage line 115
  5. theorem OAI.SharpLogRamsey.Incidence.low_incidence_target_mass line 208
  6. theorem OAI.SharpLogRamsey.ProjectiveDuality.low_incidence_dual_mass line 291
  7. lemma OAI.SharpLogRamsey.HighRankLowHit.hit_mass line 320
  8. theorem OAI.SharpLogRamsey.HighRankLowHit.low_hit_mass line 337
  9. def OAI.SharpLogRamsey.HighRankBudgets.beta line 363
  10. def OAI.SharpLogRamsey.HighRankBudgets.scaleK line 364
  11. lemma OAI.SharpLogRamsey.HighRankBudgets.eventually_monomial_le_linear line 366
  12. lemma OAI.SharpLogRamsey.HighRankBudgets.K_upper line 380
  13. lemma OAI.SharpLogRamsey.HighRankBudgets.eventually_K_linear line 387
  14. theorem OAI.SharpLogRamsey.HighRankBudgets.eventually_exp_K_over_q line 394
  15. lemma OAI.SharpLogRamsey.HighRankBudgets.row_size line 412
  16. lemma OAI.SharpLogRamsey.HighRankBudgets.block_size line 417
  17. lemma OAI.SharpLogRamsey.HighRankBudgets.block_embedding line 426
  18. theorem OAI.SharpLogRamsey.HighRankBudgets.growth_tail line 431