OAI/Combinatorics/SharpRamsey/Entropy/IntegralTypicalScoreSq.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.PoissonScore.integral_typicalScore_sq_le line 14
  2. lemma OAI.SharpRamseyFive.PoissonScore.prod_emptyIndicator line 32
  3. lemma OAI.SharpRamseyFive.PoissonScore.prod_centeredFactor line 41
  4. lemma OAI.SharpRamseyFive.PoissonScore.integrable_prod_centeredFactor line 52
  5. def OAI.SharpRamseyFive.PoissonScore.tupleMean line 59
  6. lemma OAI.SharpRamseyFive.PoissonScore.integral_prod_centeredFactor line 63
  7. lemma OAI.SharpRamseyFive.PoissonScore.prod_scoreTerm line 73
  8. lemma OAI.SharpRamseyFive.PoissonScore.integrable_prod_scoreTerm line 83
  9. lemma OAI.SharpRamseyFive.PoissonScore.integral_prod_scoreTerm line 95
  10. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_prod_scoreTerm_le line 107
  11. lemma OAI.SharpRamseyFive.PoissonScore.integral_typicalScore_pow line 121
  12. def OAI.SharpRamseyFive.PoissonScore.maskedFactor line 136
  13. def OAI.SharpRamseyFive.PoissonScore.maskedTerm line 140
  14. lemma OAI.SharpRamseyFive.PoissonScore.abs_maskedFactor_le_one line 145
  15. lemma OAI.SharpRamseyFive.PoissonScore.abs_maskedTerm_le_one line 151
  16. lemma OAI.SharpRamseyFive.PoissonScore.integrable_schedule_of_abs_le line 158
  17. lemma OAI.SharpRamseyFive.PoissonScore.integrable_maskedFactor line 165
  18. lemma OAI.SharpRamseyFive.PoissonScore.integral_maskedFactor line 174
  19. lemma OAI.SharpRamseyFive.PoissonScore.integral_maskedTerm line 181
  20. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_maskedFactor_exp_le line 190
  21. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_maskedTerm_exp_le line 207
  22. lemma OAI.SharpRamseyFive.PoissonScore.abs_prod_maskedTerm_le line 223
  23. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_component_indicator_le line 236
  24. def OAI.SharpRamseyFive.PoissonScore.untouchedBatches line 265
  25. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_maskedTerm_le_untouched line 270
  26. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_maskedTerm_le_designations line 308
  27. lemma OAI.SharpRamseyFive.PoissonScore.two_mul_le_exp_small line 333
  28. lemma OAI.SharpRamseyFive.PoissonScore.two_mul_score_attenuation line 340
  29. lemma OAI.SharpRamseyFive.PoissonScore.simple_singleton_attenuation line 358
  30. def OAI.SharpRamseyFive.PoissonScore.hitIndicator line 373
  31. lemma OAI.SharpRamseyFive.PoissonScore.hitIndicator_eq line 377
  32. lemma OAI.SharpRamseyFive.PoissonScore.hitIndicator_nonneg line 384
  33. lemma OAI.SharpRamseyFive.PoissonScore.hitIndicator_le_one line 388
  34. lemma OAI.SharpRamseyFive.PoissonScore.integrable_hitIndicator line 392
  35. lemma OAI.SharpRamseyFive.PoissonScore.integral_hitIndicator line 397
  36. lemma OAI.SharpRamseyFive.PoissonScore.maskedFactor_mul_hit line 405
  37. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_maskedFactor_hit_le line 419
  38. def OAI.SharpRamseyFive.PoissonScore.forcedHits line 440
  39. lemma OAI.SharpRamseyFive.PoissonScore.forcedHits_nonneg line 444