OAI/Combinatorics/SharpRamsey/Entropy/ComponentLabelWitness.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.TupleComponents.componentLabel_witness line 21
  2. lemma OAI.SharpRamseyFive.TupleComponents.simple_inside_univ line 30
  3. lemma OAI.SharpRamseyFive.TupleComponents.blockTrunc_eq_indicator line 42
  4. lemma OAI.SharpRamseyFive.TupleComponents.componentFactor_eq_single line 66
  5. lemma OAI.SharpRamseyFive.TupleComponents.simple_component_integral line 88
  6. lemma OAI.SharpRamseyFive.TupleComponents.simple_component_attenuation line 104
  7. lemma OAI.SharpRamseyFive.TupleComponents.nonsimple_component_attenuation line 125
  8. abbrev OAI.SharpRamseyFive.TupleMultiplicity.RepresentativeMap line 152
  9. abbrev OAI.SharpRamseyFive.TupleMultiplicity.Representatives line 153
  10. def OAI.SharpRamseyFive.TupleMultiplicity.chosen line 155
  11. lemma OAI.SharpRamseyFive.TupleMultiplicity.chosen_spec line 159
  12. lemma OAI.SharpRamseyFive.TupleMultiplicity.chosen_eq line 163
  13. lemma OAI.SharpRamseyFive.TupleMultiplicity.chosen_idempotent line 171
  14. def OAI.SharpRamseyFive.TupleMultiplicity.representatives line 175
  15. def OAI.SharpRamseyFive.TupleMultiplicity.assignment line 178
  16. def OAI.SharpRamseyFive.TupleMultiplicity.decode line 188
  17. lemma OAI.SharpRamseyFive.TupleMultiplicity.decode_assignment line 192
  18. def OAI.SharpRamseyFive.TupleMultiplicity.encode line 197
  19. lemma OAI.SharpRamseyFive.TupleMultiplicity.encode_injective line 202
  20. lemma OAI.SharpRamseyFive.TupleMultiplicity.representativeMap_card_le line 208
  21. lemma OAI.SharpRamseyFive.TupleMultiplicity.representatives_card_le line 214
  22. theorem OAI.SharpRamseyFive.TupleMultiplicity.sum_tuples_le_representative_assignments line 217
  23. lemma OAI.SharpRamseyFive.TupleMultiplicity.range_decode line 235
  24. lemma OAI.SharpRamseyFive.TupleMultiplicity.fiber_decode line 247
  25. lemma OAI.SharpRamseyFive.TupleComponents.mass_inside_eq line 265
  26. lemma OAI.SharpRamseyFive.TupleComponents.mass_scaled line 284
  27. lemma OAI.SharpRamseyFive.TupleComponents.source_inside_mass_lower line 288
  28. lemma OAI.SharpRamseyFive.TupleComponents.repeats_same_component line 299
  29. def OAI.SharpRamseyFive.TupleComponents.hitBatches line 311
  30. def OAI.SharpRamseyFive.TupleComponents.BAD line 314
  31. lemma OAI.SharpRamseyFive.TupleComponents.batches_partition line 316
  32. lemma OAI.SharpRamseyFive.TupleComponents.untouched_of_not_bad line 321
  33. theorem OAI.SharpRamseyFive.TupleComponents.simple_component_designations_raw line 329
  34. theorem OAI.SharpRamseyFive.TupleComponents.simple_component_designations line 371
  35. def OAI.SharpRamseyFive.HighMoment.allTrunc line 429
  36. lemma OAI.SharpRamseyFive.HighMoment.allTrunc_range line 433
  37. lemma OAI.SharpRamseyFive.HighMoment.scoreTerm_abs_le line 442
  38. lemma OAI.SharpRamseyFive.HighMoment.truncated_tuple_abs_le line 449