OAI/Combinatorics/SharpRamsey/Entropy/ExternalMass.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.external_mass_le line 18
  2. lemma OAI.SharpRamseyFive.PoissonScore.internal_mass_lower line 45
  3. lemma OAI.SharpRamseyFive.PoissonScore.internal_parts_disjoint line 54
  4. def OAI.SharpRamseyFive.PoissonScore.componentLabel line 64
  5. lemma OAI.SharpRamseyFive.PoissonScore.componentLabel_external line 73
  6. lemma OAI.SharpRamseyFive.PoissonScore.componentLabel_internal line 81
  7. lemma OAI.SharpRamseyFive.PoissonScore.internalPart_iff_label line 95
  8. lemma OAI.SharpRamseyFive.PoissonScore.direction_internal_or_external line 112
  9. lemma OAI.SharpRamseyFive.PoissonScore.source_internal_mass_lower line 122
  10. abbrev OAI.SharpRamseyFive.TupleComponents.Block line 150
  11. def OAI.SharpRamseyFive.TupleComponents.fill line 151
  12. lemma OAI.SharpRamseyFive.TupleComponents.fill_restrict line 157
  13. def OAI.SharpRamseyFive.TupleComponents.lineTrunc line 162
  14. def OAI.SharpRamseyFive.TupleComponents.blockTrunc line 165
  15. lemma OAI.SharpRamseyFive.TupleComponents.lineTrunc_range line 168
  16. lemma OAI.SharpRamseyFive.TupleComponents.blockTrunc_range line 172
  17. lemma OAI.SharpRamseyFive.TupleComponents.prod_fibers line 179
  18. lemma OAI.SharpRamseyFive.TupleComponents.trunc_split line 193
  19. lemma OAI.SharpRamseyFive.TupleComponents.emptyIndicator_congr line 201
  20. lemma OAI.SharpRamseyFive.TupleComponents.scoreTerm_congr line 211
  21. def OAI.SharpRamseyFive.TupleComponents.componentFactor line 221
  22. lemma OAI.SharpRamseyFive.TupleComponents.componentFactor_bound line 229
  23. lemma OAI.SharpRamseyFive.TupleComponents.tuple_pointwise_split line 246
  24. theorem OAI.SharpRamseyFive.TupleComponents.tuple_integral_split line 270
  25. def OAI.SharpRamseyFive.TupleComponents.strongSplit line 290
  26. lemma OAI.SharpRamseyFive.TupleComponents.strong_tuple_integral_split line 299
  27. abbrev OAI.SharpRamseyFive.TupleComponents.IntDir line 311
  28. def OAI.SharpRamseyFive.TupleComponents.inside line 313
  29. def OAI.SharpRamseyFive.TupleComponents.touched line 316
  30. def OAI.SharpRamseyFive.TupleComponents.unblock line 320
  31. lemma OAI.SharpRamseyFive.TupleComponents.fill_empty_iff line 324
  32. lemma OAI.SharpRamseyFive.TupleComponents.scoreTerm_eq_masked line 354
  33. def OAI.SharpRamseyFive.TupleComponents.blockCoords line 372
  34. def OAI.SharpRamseyFive.TupleComponents.unblockEquiv line 378
  35. lemma OAI.SharpRamseyFive.TupleComponents.unblockEquiv_apply line 384
  36. lemma OAI.SharpRamseyFive.TupleComponents.measurePreserving_unblock line 389
  37. lemma OAI.SharpRamseyFive.TupleComponents.integrable_block_bounded line 399
  38. lemma OAI.SharpRamseyFive.TupleComponents.componentFactor_abs_le_term line 407
  39. lemma OAI.SharpRamseyFive.TupleComponents.component_integral_abs_le line 435