OAI/Combinatorics/SharpRamsey/Entropy/ForcedHits.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.PoissonScore.forcedHits_le_one line 15
  2. lemma OAI.SharpRamseyFive.PoissonScore.abs_maskedTerm_mul_forcedHits line 20
  3. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_maskedTerm_forcedHits_le line 29
  4. def OAI.SharpRamseyFive.PoissonScore.hitBatches line 62
  5. def OAI.SharpRamseyFive.PoissonScore.overloaded line 65
  6. lemma OAI.SharpRamseyFive.PoissonScore.overloaded_eq_empty line 70
  7. lemma OAI.SharpRamseyFive.PoissonScore.forcedHits_eq_one_of_subset line 81
  8. lemma OAI.SharpRamseyFive.PoissonScore.overload_indicator_le_certificates line 90
  9. lemma OAI.SharpRamseyFive.PoissonScore.integrable_abs_maskedTerm_forcedHits line 113
  10. lemma OAI.SharpRamseyFive.PoissonScore.truncation_error_raw line 126
  11. lemma OAI.SharpRamseyFive.PoissonScore.truncation_error line 181
  12. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_compl_indicator_le line 202
  13. lemma OAI.SharpRamseyFive.PoissonScore.simple_singleton_truncated line 231
  14. lemma OAI.SharpRamseyFive.PoissonScore.measurePreserving_uncurry_schedule line 252
  15. def OAI.SharpRamseyFive.PoissonScore.partitionEquiv line 261
  16. lemma OAI.SharpRamseyFive.PoissonScore.partitionEquiv_apply line 267
  17. lemma OAI.SharpRamseyFive.PoissonScore.measurePreserving_partition line 271
  18. lemma OAI.SharpRamseyFive.PoissonScore.integral_partition_prod line 287
  19. def OAI.SharpRamseyFive.PoissonScore.externalEquiv line 298
  20. lemma OAI.SharpRamseyFive.PoissonScore.measurePreserving_external line 305
  21. lemma OAI.SharpRamseyFive.PoissonScore.integral_external_components line 325
  22. def OAI.SharpRamseyFive.PoissonScore.strongGraph line 366
  23. lemma OAI.SharpRamseyFive.PoissonScore.cross_component_overlap line 375
  24. def OAI.SharpRamseyFive.PoissonScore.External line 384
  25. lemma OAI.SharpRamseyFive.PoissonScore.external_iff_other line 390
  26. def OAI.SharpRamseyFive.PoissonScore.externalPart line 405
  27. def OAI.SharpRamseyFive.PoissonScore.internalPart line 410
  28. lemma OAI.SharpRamseyFive.PoissonScore.internal_external_mass line 416
  29. def OAI.SharpRamseyFive.PoissonScore.otherComponents line 423
  30. lemma OAI.SharpRamseyFive.PoissonScore.external_mass_le_sum line 432