OAI/Combinatorics/SharpRamsey/Marking/CardVectorLifts.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. theorem OAI.SharpLogRamsey.RichUnion.card_vectorLifts line 17
  2. def OAI.SharpLogRamsey.RichUnion.projectiveIn line 31
  3. theorem OAI.SharpLogRamsey.RichUnion.mem_projectiveIn line 37
  4. theorem OAI.SharpLogRamsey.RichUnion.vectorLifts_projectiveIn line 43
  5. def OAI.SharpLogRamsey.RichUnion.projectivePoints line 51
  6. theorem OAI.SharpLogRamsey.RichUnion.mem_projectivePoints line 57
  7. def OAI.SharpLogRamsey.RichUnion.projectiveUnion line 63
  8. theorem OAI.SharpLogRamsey.RichUnion.mem_projectiveUnion line 69
  9. def OAI.SharpLogRamsey.RichUnion.projectiveSubmoduleEquiv line 75
  10. theorem OAI.SharpLogRamsey.RichUnion.card_projectivePoints line 99
  11. theorem OAI.SharpLogRamsey.RichUnion.card_projectivePoints_mul line 107
  12. theorem OAI.SharpLogRamsey.RichUnion.rich_union_projective line 112
  13. lemma OAI.SharpLogRamsey.HighRankGeometry.sum_powers_le_twice line 155
  14. lemma OAI.SharpLogRamsey.HighRankGeometry.projective_card_le line 169
  15. lemma OAI.SharpLogRamsey.HighRankGeometry.subspace_mass_le line 176
  16. theorem OAI.SharpLogRamsey.HighRankGeometry.threshold_rich line 197
  17. theorem OAI.SharpLogRamsey.HighRankGeometry.high_rank_tail line 230
  18. def OAI.SharpLogRamsey.FiniteSamplingBounds.rowTail line 276
  19. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowTail_nonneg line 279
  20. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowTail_le_one line 287
  21. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowTail_moment line 295
  22. theorem OAI.SharpLogRamsey.FiniteSamplingBounds.rowTail_small line 308
  23. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowTail_zero line 351
  24. lemma OAI.SharpLogRamsey.DyadicTail.exists_band line 381
  25. lemma OAI.SharpLogRamsey.DyadicTail.finite_geometric line 396
  26. theorem OAI.SharpLogRamsey.DyadicTail.small_tail_sum line 405