OAI/Combinatorics/SharpRamsey/Marking/HighRank.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. theorem OAI.SharpLogRamsey.RichUnion.rank_le_of_ker_le line 26
  2. theorem OAI.SharpLogRamsey.RichUnion.finrank_finset_sup_le line 34
  3. def OAI.SharpLogRamsey.RichUnion.evalOn line 49
  4. theorem OAI.SharpLogRamsey.RichUnion.evalOn_apply line 54
  5. def OAI.SharpLogRamsey.RichUnion.evalSpace line 58
  6. def OAI.SharpLogRamsey.RichUnion.diagonal line 61
  7. theorem OAI.SharpLogRamsey.RichUnion.evalSpace_full line 66
  8. theorem OAI.SharpLogRamsey.RichUnion.evalSpace_box_partition line 82
  9. theorem OAI.SharpLogRamsey.RichUnion.card_le_boxes_mul_eval_rank line 125
  10. theorem OAI.SharpLogRamsey.RichUnion.totalDegree_aeval_linear line 145
  11. def OAI.SharpLogRamsey.RichUnion.linearCoordinates line 166
  12. theorem OAI.SharpLogRamsey.RichUnion.totalDegree_linearCoordinates line 170
  13. theorem OAI.SharpLogRamsey.RichUnion.eval_linearCoordinates line 178
  14. theorem OAI.SharpLogRamsey.RichUnion.eval_aeval_linearCoordinates line 192
  15. theorem OAI.SharpLogRamsey.RichUnion.totalDegree_le_of_restrictDegree line 205
  16. theorem OAI.SharpLogRamsey.RichUnion.card_roots_mul_le line 218
  17. def OAI.SharpLogRamsey.RichUnion.inSubspace line 230
  18. theorem OAI.SharpLogRamsey.RichUnion.mem_inSubspace line 235
  19. theorem OAI.SharpLogRamsey.RichUnion.vanish_on_rich_subspace line 241
  20. theorem OAI.SharpLogRamsey.RichUnion.evalSpace_rank_le_of_rich line 293
  21. theorem OAI.SharpLogRamsey.RichUnion.card_union_le_boxes line 320
  22. theorem OAI.SharpLogRamsey.RichUnion.exists_box_parameters line 330
  23. theorem OAI.SharpLogRamsey.RichUnion.rich_union_vector line 366
  24. def OAI.SharpLogRamsey.RichUnion.vectorLifts line 407
  25. theorem OAI.SharpLogRamsey.RichUnion.mem_vectorLifts line 412