OAI/Combinatorics/SharpRamsey/Entropy/LargeCard.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

High moments, finite-field subspaces, and incidence bounds.

  1. lemma OAI.SharpRamseyFive.AmbientEnumeration.large_card line 26
  2. def OAI.SharpRamseyFive.AmbientEnumeration.vertexExpansion line 46
  3. lemma OAI.SharpRamseyFive.AmbientEnumeration.vertexExpansion_nonneg line 54
  4. lemma OAI.SharpRamseyFive.AmbientEnumeration.designated_le_partition line 66
  5. theorem OAI.SharpRamseyFive.AmbientEnumeration.designation_sum_enumerated line 84
  6. lemma OAI.SharpRamseyFive.MomentBudgets.block_cost line 137
  7. lemma OAI.SharpRamseyFive.MomentBudgets.singleton_cost line 183
  8. lemma OAI.SharpRamseyFive.MomentBudgets.partition_cost line 196
  9. theorem OAI.SharpRamseyFive.AmbientEnumeration.ambient_refined_truncated_moment line 223
  10. lemma OAI.SharpRamseyFive.AmbientEnumeration.allTrunc_eq_one line 273
  11. theorem OAI.SharpRamseyFive.AmbientEnumeration.ambient_untruncated_moment line 283
  12. def OAI.SharpLogRamsey.MomentBudgetBridge.anchorBudget line 325
  13. def OAI.SharpLogRamsey.MomentBudgetBridge.certificateOverhead line 327
  14. lemma OAI.SharpLogRamsey.MomentBudgetBridge.anchorBudget_nonneg line 332
  15. lemma OAI.SharpLogRamsey.MomentBudgetBridge.certificateOverhead_nonneg line 337
  16. theorem OAI.SharpLogRamsey.MomentBudgetBridge.labelled_branching_bound line 343
  17. theorem OAI.SharpLogRamsey.MomentBudgetBridge.absorb_certificate line 392
  18. theorem OAI.SharpLogRamsey.MomentBudgetBridge.singleton_budget line 400
  19. def OAI.SharpLogRamsey.MomentBudgetBridge.shiftOverhead line 413
  20. lemma OAI.SharpLogRamsey.MomentBudgetBridge.shifted_dyadic_budget line 415
  21. lemma OAI.SharpLogRamsey.MomentBudgetBridge.strong_dyadic_budget line 432