OAI/Combinatorics/SharpRamsey/Marking/TailSum.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. theorem OAI.SharpLogRamsey.DyadicTail.tail_sum line 17
  2. theorem OAI.SharpLogRamsey.HighRankSampling.high_rank_expected line 82
  3. lemma OAI.SharpLogRamsey.HighRankSampling.mean_admitted_eq line 143
  4. def OAI.SharpLogRamsey.HighRankDecoder.hitSpan line 169
  5. lemma OAI.SharpLogRamsey.HighRankDecoder.center_le line 174
  6. lemma OAI.SharpLogRamsey.HighRankDecoder.hit_le line 177
  7. lemma OAI.SharpLogRamsey.HighRankDecoder.line_le_ker line 184
  8. lemma OAI.SharpLogRamsey.HighRankDecoder.annihilates_hitSpan line 189
  9. def OAI.SharpLogRamsey.HighRankDecoder.Admitted line 201
  10. lemma OAI.SharpLogRamsey.HighRankDecoder.admitted_incident line 209
  11. theorem OAI.SharpLogRamsey.HighRankDecoder.coverage line 216
  12. def OAI.SharpLogRamsey.HighRankExcess.projectiveSubmoduleEquiv line 255
  13. lemma OAI.SharpLogRamsey.HighRankExcess.projective_card line 283
  14. lemma OAI.SharpLogRamsey.HighRankExcess.geom_sum_le_twice line 292
  15. lemma OAI.SharpLogRamsey.HighRankExcess.small_span_card line 302
  16. def OAI.SharpLogRamsey.HighRankExcess.partners line 316
  17. lemma OAI.SharpLogRamsey.HighRankExcess.partners_eq line 320
  18. lemma OAI.SharpLogRamsey.HighRankExcess.excess_partners_card line 329
  19. lemma OAI.SharpLogRamsey.HighRankExcess.full_rank_no_partners line 338
  20. def OAI.SharpLogRamsey.HighRankExcess.excessCarrier line 349
  21. lemma OAI.SharpLogRamsey.HighRankExcess.excessCarrier_card line 355
  22. theorem OAI.SharpLogRamsey.HighRankExcess.target_excess_mass line 389
  23. lemma OAI.SharpLogRamsey.HighRankExcess.excessCarrier_full_rank line 414
  24. lemma OAI.SharpLogRamsey.HighRankExcess.target_excess_mass_le line 424