OAI/Combinatorics/SharpRamsey/Entropy/HighMoments.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.SharpRamseyFive.PoissonScore.batchMeasure line 15
  2. instance OAI.SharpRamseyFive.PoissonScore.flat_HighMomentRecovered_1 line 18
  3. def OAI.SharpRamseyFive.PoissonScore.emptyEvent line 22
  4. def OAI.SharpRamseyFive.PoissonScore.emptyIndicator line 25
  5. def OAI.SharpRamseyFive.PoissonScore.mass line 28
  6. lemma OAI.SharpRamseyFive.PoissonScore.measurableSet_emptyEvent line 32
  7. lemma OAI.SharpRamseyFive.PoissonScore.measure_emptyEvent line 36
  8. lemma OAI.SharpRamseyFive.PoissonScore.integral_emptyIndicator line 46
  9. lemma OAI.SharpRamseyFive.PoissonScore.integrable_emptyIndicator line 54
  10. lemma OAI.SharpRamseyFive.PoissonScore.emptyIndicator_mul line 59
  11. lemma OAI.SharpRamseyFive.PoissonScore.mass_union_inter line 69
  12. def OAI.SharpRamseyFive.PoissonScore.centeredFactor line 73
  13. lemma OAI.SharpRamseyFive.PoissonScore.integrable_centeredFactor line 77
  14. lemma OAI.SharpRamseyFive.PoissonScore.integral_centeredFactor line 82
  15. lemma OAI.SharpRamseyFive.PoissonScore.integral_centeredFactor_mul line 89
  16. lemma OAI.SharpRamseyFive.PoissonScore.emptyIndicator_nonneg line 128
  17. lemma OAI.SharpRamseyFive.PoissonScore.abs_centeredFactor_le_one line 135
  18. lemma OAI.SharpRamseyFive.PoissonScore.centeredFactor_of_hit line 141
  19. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_centeredFactor_le line 149
  20. lemma OAI.SharpRamseyFive.PoissonScore.abs_exp_neg_sub_exp_neg_le line 163
  21. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_centeredFactor_le line 188
  22. lemma OAI.SharpRamseyFive.PoissonScore.integral_abs_centeredFactor_exp_le line 201
  23. lemma OAI.SharpRamseyFive.PoissonScore.integrable_centeredFactor_mul line 214
  24. lemma OAI.SharpRamseyFive.PoissonScore.mass_nonneg line 228
  25. lemma OAI.SharpRamseyFive.PoissonScore.mass_mono line 232
  26. lemma OAI.SharpRamseyFive.PoissonScore.one_sub_exp_neg_le line 236
  27. lemma OAI.SharpRamseyFive.PoissonScore.covariance_le line 242
  28. lemma OAI.SharpRamseyFive.PoissonScore.covariance_nonneg line 264
  29. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_centeredFactor_mul_le_mass line 270
  30. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_centeredFactor_mul_exp_le line 284
  31. def OAI.SharpRamseyFive.PoissonScore.scheduleMeasure line 321
  32. instance OAI.SharpRamseyFive.PoissonScore.flat_HighMomentRecovered_2 line 325
  33. def OAI.SharpRamseyFive.PoissonScore.scoreTerm line 329
  34. lemma OAI.SharpRamseyFive.PoissonScore.integrable_scoreTerm line 334
  35. lemma OAI.SharpRamseyFive.PoissonScore.integral_scoreTerm line 343
  36. def OAI.SharpRamseyFive.PoissonScore.pairMean line 353
  37. lemma OAI.SharpRamseyFive.PoissonScore.integrable_scoreTerm_mul line 358
  38. lemma OAI.SharpRamseyFive.PoissonScore.integral_scoreTerm_mul line 372
  39. lemma OAI.SharpRamseyFive.PoissonScore.abs_integral_scoreTerm_mul_le line 383
  40. def OAI.SharpRamseyFive.PoissonScore.typicalScore line 397
  41. lemma OAI.SharpRamseyFive.PoissonScore.integral_typicalScore_sq line 401