OAI/Combinatorics/SharpRamsey/Entropy/NewEvents.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.SharpRamseyFive.WeightedPrograms.newEvents line 22
  2. def OAI.SharpRamseyFive.WeightedPrograms.newValues line 29
  3. def OAI.SharpRamseyFive.WeightedPrograms.advance line 36
  4. def OAI.SharpRamseyFive.WeightedPrograms.degree line 39
  5. def OAI.SharpRamseyFive.WeightedPrograms.actionCharge line 43
  6. def OAI.SharpRamseyFive.WeightedPrograms.rawCost line 48
  7. def OAI.SharpRamseyFive.WeightedPrograms.programCost line 55
  8. lemma OAI.SharpRamseyFive.WeightedPrograms.newEvents_fresh line 61
  9. lemma OAI.SharpRamseyFive.WeightedPrograms.rawCost_nonneg line 76
  10. lemma OAI.SharpRamseyFive.WeightedPrograms.programCost_nonneg line 93
  11. def OAI.SharpRamseyFive.WeightedPrograms.uniformAnchorBudget line 101
  12. def OAI.SharpRamseyFive.WeightedPrograms.branchingBound line 104
  13. lemma OAI.SharpRamseyFive.WeightedPrograms.branchingBound_nonneg line 115
  14. lemma OAI.SharpRamseyFive.WeightedPrograms.discounted_raw_sum line 124
  15. theorem OAI.SharpRamseyFive.WeightedPrograms.discounted_row_bound line 143
  16. theorem OAI.SharpRamseyFive.WeightedPrograms.program_enumeration line 185
  17. def OAI.SharpRamseyFive.ResidualCertificate.rootProbability line 215
  18. def OAI.SharpRamseyFive.ResidualCertificate.rootMeasure line 217
  19. instance OAI.SharpRamseyFive.ResidualCertificate.flat_HighMomentRecovered_6 line 220
  20. def OAI.SharpRamseyFive.ResidualCertificate.selected line 224
  21. def OAI.SharpRamseyFive.ResidualCertificate.voidEvent line 227
  22. def OAI.SharpRamseyFive.ResidualCertificate.voidIndicator line 230
  23. def OAI.SharpRamseyFive.ResidualCertificate.badIndicator line 233
  24. lemma OAI.SharpRamseyFive.ResidualCertificate.integrable_bounded line 237
  25. lemma OAI.SharpRamseyFive.ResidualCertificate.integrable_voidIndicator line 243
  26. lemma OAI.SharpRamseyFive.ResidualCertificate.integrable_badIndicator line 248
  27. lemma OAI.SharpRamseyFive.ResidualCertificate.voidIndicator_nonneg line 255
  28. lemma OAI.SharpRamseyFive.ResidualCertificate.badIndicator_nonneg line 258
  29. lemma OAI.SharpRamseyFive.ResidualCertificate.integral_voidIndicator line 263
  30. lemma OAI.SharpRamseyFive.ResidualCertificate.erase_void_witness line 278
  31. lemma OAI.SharpRamseyFive.ResidualCertificate.badIndicator_le_erase_void line 305
  32. lemma OAI.SharpRamseyFive.ResidualCertificate.integral_badIndicator_le line 315
  33. lemma OAI.SharpRamseyFive.ResidualCertificate.indicator_selected line 331
  34. lemma OAI.SharpRamseyFive.ResidualCertificate.integrable_selected_card line 337
  35. lemma OAI.SharpRamseyFive.ResidualCertificate.integral_selected_card line 347
  36. theorem OAI.SharpRamseyFive.ResidualCertificate.exists_small_root_set line 364
  37. theorem OAI.SharpRamseyFive.ResidualCertificate.exists_distinct_witnesses line 428