OAI/Combinatorics/SharpRamsey/Entropy/ShiftKernelSum.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.SingletonEnumeration.shift_le_kernel_sum line 27
  2. theorem OAI.SharpRamseyFive.SingletonEnumeration.actual_shift_bad_enumeration line 81
  3. lemma OAI.SharpRamseyFive.DyadicMoments.dyadic_cover line 134
  4. theorem OAI.SharpRamseyFive.DyadicMoments.moment_le_of_cover line 156
  5. theorem OAI.SharpRamseyFive.DyadicMoments.higher_moment_le_of_cover line 197
  6. theorem OAI.SharpRamseyFive.DyadicMoments.integer_strength_moment line 219
  7. def OAI.SharpRamseyFive.WeightedPrograms.DistinctPairs line 253
  8. instance OAI.SharpRamseyFive.WeightedPrograms.flat_HighMomentRecovered_7 line 255
  9. def OAI.SharpRamseyFive.WeightedPrograms.strength line 257
  10. lemma OAI.SharpRamseyFive.WeightedPrograms.strength_nonneg line 261
  11. theorem OAI.SharpRamseyFive.WeightedPrograms.pairMoment_dyadic line 267
  12. theorem OAI.SharpRamseyFive.WeightedPrograms.branchingBound_dyadic line 302
  13. lemma OAI.SharpRamseyFive.SingletonEnumeration.sum_split_diagonal line 336
  14. lemma OAI.SharpRamseyFive.SingletonEnumeration.sum_pairs_split_diagonal line 342
  15. theorem OAI.SharpRamseyFive.SingletonEnumeration.shift_row_dyadic line 352
  16. theorem OAI.SharpRamseyFive.SingletonEnumeration.shift_pairs_dyadic line 381
  17. theorem OAI.SharpRamseyFive.SingletonEnumeration.pairMoment_labelled_le line 409
  18. def OAI.SharpRamseyFive.ResidualElimination.patch line 454
  19. lemma OAI.SharpRamseyFive.ResidualElimination.patch_mem line 458