OAI/Combinatorics/SharpRamsey/Entropy/CompleteProgramWeight.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.SharpRamseyFive.CertificateCover.complete_program_weight line 28
  2. lemma OAI.SharpRamseyFive.CertificateCover.complete_program_sum line 39
  3. def OAI.SharpRamseyFive.CertificateCover.badEvent line 85
  4. lemma OAI.SharpRamseyFive.CertificateCover.bad_event_cover line 94
  5. theorem OAI.SharpRamseyFive.CertificateCover.bad_completion_bound line 126
  6. def OAI.SharpRamseyFive.CertificateCover.selectedBadEvent line 152
  7. lemma OAI.SharpRamseyFive.CertificateCover.selected_bad_event_cover line 162
  8. theorem OAI.SharpRamseyFive.CertificateCover.selected_bad_completion_bound line 194
  9. lemma OAI.SharpRamseyFive.SelectionBridge.restriction_preserving line 233
  10. lemma OAI.SharpRamseyFive.SelectionBridge.integral_restriction line 242
  11. lemma OAI.SharpRamseyFive.SelectionBridge.label_none_external line 251
  12. def OAI.SharpRamseyFive.SelectionBridge.selectedHit line 259
  13. lemma OAI.SharpRamseyFive.SelectionBridge.touched_equals_shared line 263
  14. lemma OAI.SharpRamseyFive.SelectionBridge.selected_trunc line 284
  15. def OAI.SharpRamseyFive.SelectionBridge.vertexBadMass line 299
  16. lemma OAI.SharpRamseyFive.SelectionBridge.empty_coherent line 307
  17. lemma OAI.SharpRamseyFive.SelectionBridge.bad_mass_le_selected_event line 317
  18. lemma OAI.SharpRamseyFive.SelectionBridge.vertex_injective line 378
  19. lemma OAI.SharpRamseyFive.SelectionBridge.component_bad_mass_eq_vertex line 383
  20. theorem OAI.SharpRamseyFive.SelectionBridge.bad_residual_sum_le line 399
  21. def OAI.SharpRamseyFive.SelectionBridge.labelled line 447
  22. lemma OAI.SharpRamseyFive.SelectionBridge.labelled_injective line 450
  23. lemma OAI.SharpRamseyFive.SelectionBridge.labelled_map_injective line 455