OAI/Combinatorics/SharpRamsey/Entropy/TruncatedTupleIntegrable.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.HighMoment.truncated_tuple_integrable line 19
  2. theorem OAI.SharpRamseyFive.HighMoment.integral_truncated_score_pow line 30
  3. def OAI.SharpRamseyFive.HighMoment.absSplit line 49
  4. lemma OAI.SharpRamseyFive.HighMoment.integral_abs_component_le_one line 60
  5. lemma OAI.SharpRamseyFive.HighMoment.absSplit_nonneg line 80
  6. lemma OAI.SharpRamseyFive.HighMoment.strongSplit_abs_le line 88
  7. theorem OAI.SharpRamseyFive.HighMoment.truncated_moment_le_tuple_sum line 102
  8. theorem OAI.SharpRamseyFive.HighMoment.truncated_moment_le_representative_sum line 113
  9. def OAI.SharpRamseyFive.Designations.badIndicator line 136
  10. lemma OAI.SharpRamseyFive.Designations.badIndicator_range line 140
  11. lemma OAI.SharpRamseyFive.Designations.product_expansion line 145
  12. def OAI.SharpRamseyFive.Designations.badMass line 168
  13. lemma OAI.SharpRamseyFive.Designations.badTerm_range line 173
  14. lemma OAI.SharpRamseyFive.Designations.badTerm_integrable line 185
  15. lemma OAI.SharpRamseyFive.Designations.badMass_nonneg line 196
  16. lemma OAI.SharpRamseyFive.Designations.majorant_integrable line 200
  17. lemma OAI.SharpRamseyFive.Designations.integral_expansion line 208
  18. theorem OAI.SharpRamseyFive.Designations.integral_product_le line 220
  19. abbrev OAI.SharpRamseyFive.AmbientDesignations.Components line 259
  20. def OAI.SharpRamseyFive.AmbientDesignations.vertex line 260
  21. lemma OAI.SharpRamseyFive.AmbientDesignations.vertex_color line 262
  22. def OAI.SharpRamseyFive.AmbientDesignations.simpleSet line 266
  23. def OAI.SharpRamseyFive.AmbientDesignations.alpha line 270
  24. def OAI.SharpRamseyFive.AmbientDesignations.delta line 271
  25. lemma OAI.SharpRamseyFive.AmbientDesignations.alpha_nonneg line 275
  26. lemma OAI.SharpRamseyFive.AmbientDesignations.source_alpha_le line 278
  27. lemma OAI.SharpRamseyFive.AmbientDesignations.internal_mass_eq line 288
  28. lemma OAI.SharpRamseyFive.AmbientDesignations.source_local_data line 296
  29. def OAI.SharpRamseyFive.AmbientDesignations.extraWeight line 310
  30. def OAI.SharpRamseyFive.AmbientDesignations.isBad line 317
  31. def OAI.SharpRamseyFive.AmbientDesignations.componentAbs line 321
  32. lemma OAI.SharpRamseyFive.AmbientDesignations.scaled_internal line 328
  33. lemma OAI.SharpRamseyFive.AmbientDesignations.componentAbs_range line 337
  34. lemma OAI.SharpRamseyFive.AmbientDesignations.simple_bound line 352
  35. lemma OAI.SharpRamseyFive.AmbientDesignations.nonsimple_bound line 380
  36. def OAI.SharpRamseyFive.AmbientDesignations.designatedBound line 404
  37. lemma OAI.SharpRamseyFive.AmbientDesignations.extraWeight_nonneg line 414
  38. lemma OAI.SharpRamseyFive.AmbientDesignations.designatedBound_nonneg line 420
  39. theorem OAI.SharpRamseyFive.AmbientDesignations.component_product_designated line 429
  40. theorem OAI.SharpRamseyFive.AmbientDesignations.truncated_power_designated line 448