OAI/Combinatorics/SharpRamsey/Entropy/PoissonLaw.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.SharpRamseyFive.StaticCertificates.poissonLaw line 14
  2. instance OAI.SharpRamseyFive.StaticCertificates.flat_HighMomentRecovered_3 line 17
  3. def OAI.SharpRamseyFive.StaticCertificates.positiveEvent line 21
  4. def OAI.SharpRamseyFive.StaticCertificates.certificateIndicator line 24
  5. def OAI.SharpRamseyFive.StaticCertificates.weight line 27
  6. lemma OAI.SharpRamseyFive.StaticCertificates.measurableSet_positiveEvent line 31
  7. lemma OAI.SharpRamseyFive.StaticCertificates.integrable_certificateIndicator line 35
  8. lemma OAI.SharpRamseyFive.StaticCertificates.indicator_nonneg line 40
  9. lemma OAI.SharpRamseyFive.StaticCertificates.integral_certificateIndicator line 45
  10. lemma OAI.SharpRamseyFive.StaticCertificates.integral_certificateIndicator_le line 61
  11. lemma OAI.SharpRamseyFive.StaticCertificates.weight_nonneg line 73
  12. lemma OAI.SharpRamseyFive.StaticCertificates.weight_union line 78
  13. lemma OAI.SharpRamseyFive.StaticCertificates.positiveEvent_union line 88
  14. theorem OAI.SharpRamseyFive.StaticCertificates.static_union_bound line 95
  15. def OAI.SharpRamseyFive.StaticCertificates.witnessRequirements line 123
  16. lemma OAI.SharpRamseyFive.StaticCertificates.witnessRequirements_card line 127
  17. lemma OAI.SharpRamseyFive.StaticCertificates.witness_weight line 135
  18. lemma OAI.SharpRamseyFive.StaticCertificates.sum_witness_weight line 145
  19. theorem OAI.SharpRamseyFive.StaticCertificates.pair_certificate_weight line 155
  20. theorem OAI.SharpRamseyFive.StaticCertificates.pair_certificate_weight_le line 170
  21. theorem OAI.SharpRamseyFive.StaticCertificates.pair_witness_exists line 181
  22. def OAI.SharpRamseyFive.StaticCertificates.dictionary line 194
  23. lemma OAI.SharpRamseyFive.StaticCertificates.direction_mem_dictionary line 197
  24. lemma OAI.SharpRamseyFive.StaticCertificates.witnessRequirements_disjoint line 201
  25. lemma OAI.SharpRamseyFive.StaticCertificates.weight_union_fresh line 212
  26. theorem OAI.SharpRamseyFive.StaticCertificates.pair_dictionary_extension line 218
  27. def OAI.SharpRamseyFive.StaticCertificates.anchorRequirements line 224
  28. lemma OAI.SharpRamseyFive.StaticCertificates.anchorRequirements_disjoint line 228
  29. lemma OAI.SharpRamseyFive.StaticCertificates.anchorRequirements_weight line 237
  30. lemma OAI.SharpRamseyFive.StaticCertificates.anchor_dictionary_extension line 245
  31. lemma OAI.SharpRamseyFive.StaticCertificates.anchor_dictionary_subset line 253
  32. lemma OAI.SharpRamseyFive.StaticCertificates.old_reference_has_hit line 268
  33. theorem OAI.SharpRamseyFive.StaticCertificates.anchor_choice_weight_le line 277
  34. lemma OAI.SharpRamseyFive.StaticCertificates.dictionary_card_le line 290
  35. lemma OAI.SharpRamseyFive.StaticCertificates.anchorRequirements_card_le line 294
  36. lemma OAI.SharpRamseyFive.StaticCertificates.anchor_extension_card line 300
  37. lemma OAI.SharpRamseyFive.StaticCertificates.pair_extension_card line 305
  38. abbrev OAI.SharpRamseyFive.StaticCertificates.AnchorChoice line 309
  39. def OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.direction line 312
  40. def OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.requirements line 316
  41. def OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.cost line 321
  42. lemma OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.cost_nonneg line 327
  43. lemma OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.direction_mem line 332
  44. lemma OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.fresh line 339
  45. lemma OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.weight line 349
  46. lemma OAI.SharpRamseyFive.StaticCertificates.AnchorChoice.distinct_events line 355
  47. lemma OAI.SharpRamseyFive.StaticCertificates.two_anchor_extension_weight line 371
  48. lemma OAI.SharpRamseyFive.StaticCertificates.sum_anchor_cost line 380
  49. theorem OAI.SharpRamseyFive.StaticCertificates.sum_anchor_cost_le line 390
  50. theorem OAI.SharpRamseyFive.StaticCertificates.one_anchor_geometric_cost line 407
  51. theorem OAI.SharpRamseyFive.StaticCertificates.two_anchor_geometric_cost line 426