OAI/Combinatorics/SharpRamsey/Entropy/TwoAnchorCrossCost.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.SharpRamseyFive.StaticCertificates.two_anchor_cross_cost line 20
  2. lemma OAI.SharpRamseyFive.StaticCertificates.one_anchor_subtype_sum line 60
  3. lemma OAI.SharpRamseyFive.StaticCertificates.two_anchor_subtype_sum line 71
  4. def OAI.SharpRamseyFive.CertificateEnumeration.Word line 100
  5. instance OAI.SharpRamseyFive.CertificateEnumeration.flat_HighMomentRecovered_4 line 104
  6. def OAI.SharpRamseyFive.CertificateEnumeration.finish line 111
  7. def OAI.SharpRamseyFive.CertificateEnumeration.pathWeight line 115
  8. def OAI.SharpRamseyFive.CertificateEnumeration.charge line 120
  9. lemma OAI.SharpRamseyFive.CertificateEnumeration.pathWeight_nonneg line 124
  10. theorem OAI.SharpRamseyFive.CertificateEnumeration.sum_pathWeight_le line 131
  11. lemma OAI.SharpRamseyFive.CertificateEnumeration.reweighted_path line 154
  12. theorem OAI.SharpRamseyFive.CertificateEnumeration.constrained_path_sum_le line 164
  13. lemma OAI.SharpRamseyFive.CertificateEnumeration.root_charge_nonneg line 186
  14. def OAI.SharpRamseyFive.CertificateEnumeration.DWord line 192
  15. instance OAI.SharpRamseyFive.CertificateEnumeration.flat_HighMomentRecovered_5 line 196
  16. def OAI.SharpRamseyFive.CertificateEnumeration.dFinish line 203
  17. def OAI.SharpRamseyFive.CertificateEnumeration.dWeight line 207
  18. def OAI.SharpRamseyFive.CertificateEnumeration.dCharge line 212
  19. lemma OAI.SharpRamseyFive.CertificateEnumeration.dWeight_nonneg line 217
  20. theorem OAI.SharpRamseyFive.CertificateEnumeration.sum_dWeight_le line 224
  21. lemma OAI.SharpRamseyFive.CertificateEnumeration.dReweighted line 247
  22. theorem OAI.SharpRamseyFive.CertificateEnumeration.constrained_dSum_le line 258
  23. abbrev OAI.SharpRamseyFive.WeightedPrograms.State line 294
  24. abbrev OAI.SharpRamseyFive.WeightedPrograms.RootChoice line 298
  25. abbrev OAI.SharpRamseyFive.WeightedPrograms.OneChoice line 299
  26. abbrev OAI.SharpRamseyFive.WeightedPrograms.TwoChoice line 302
  27. abbrev OAI.SharpRamseyFive.WeightedPrograms.PairDirections line 307
  28. abbrev OAI.SharpRamseyFive.WeightedPrograms.PairChoice line 309
  29. abbrev OAI.SharpRamseyFive.WeightedPrograms.Action line 313
  30. instance OAI.SharpRamseyFive.WeightedPrograms.actionFintype line 316
  31. def OAI.SharpRamseyFive.WeightedPrograms.oneCost line 325
  32. def OAI.SharpRamseyFive.WeightedPrograms.twoCost line 328
  33. def OAI.SharpRamseyFive.WeightedPrograms.pairCost line 331
  34. def OAI.SharpRamseyFive.WeightedPrograms.anchorBudget line 337
  35. lemma OAI.SharpRamseyFive.WeightedPrograms.anchorBudget_nonneg line 341
  36. theorem OAI.SharpRamseyFive.WeightedPrograms.sum_oneCost_le line 350
  37. theorem OAI.SharpRamseyFive.WeightedPrograms.sum_twoCost_le line 375
  38. def OAI.SharpRamseyFive.WeightedPrograms.pairMoment line 408
  39. lemma OAI.SharpRamseyFive.WeightedPrograms.pairMoment_nonneg line 413
  40. lemma OAI.SharpRamseyFive.WeightedPrograms.sum_pair_choices_le line 420
  41. theorem OAI.SharpRamseyFive.WeightedPrograms.sum_pairCost_le line 440