OAI/Combinatorics/SharpRamsey/Entropy/StrongDegreeBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpLogRamsey.MomentBudgetBridge.strong_degree_budget line 17
  2. theorem OAI.SharpLogRamsey.HighMoment.labelled_pair_bound line 47
  3. theorem OAI.SharpLogRamsey.HighMoment.full_branching_bound line 81
  4. lemma OAI.SharpLogRamsey.HighMoment.relation_row_card line 111
  5. lemma OAI.SharpLogRamsey.HighMoment.relation_pairs_card line 122
  6. lemma OAI.SharpLogRamsey.HighMoment.strong_pairs_markov line 135
  7. lemma OAI.SharpLogRamsey.HighMoment.deviation_sum line 151
  8. theorem OAI.SharpLogRamsey.HighMoment.dyadic_shift_bounds line 167
  9. theorem OAI.SharpLogRamsey.HighMoment.strong_relation_pairs line 212
  10. theorem OAI.SharpLogRamsey.HighMoment.strong_relation_degree line 255
  11. theorem OAI.SharpLogRamsey.HighMoment.prepared_pencil_high_moment line 285