OAI/Computability/PerfectCompleteness/Foundations/GlobalityLemmas.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Appendix.Globality.energy line 24
  2. theorem OAI.UniqueGamesTheorem.Appendix.Globality.energy_nonnegative line 27
  3. theorem OAI.UniqueGamesTheorem.Appendix.Globality.sq_average_le_average_sq line 31
  4. theorem OAI.UniqueGamesTheorem.Appendix.Globality.energy_average_le line 35
  5. theorem OAI.UniqueGamesTheorem.Appendix.Globality.energy_average_le_of_bound line 42
  6. theorem OAI.UniqueGamesTheorem.Appendix.Globality.energy_weighted_sum_le line 47
  7. def OAI.UniqueGamesTheorem.Appendix.Globality.restrictionEnergy line 71
  8. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionEnergy_translate line 75
  9. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionEnergy_average_translate_le line 80
  10. def OAI.UniqueGamesTheorem.Appendix.Globality.RestrictionGlobal line 97
  11. def OAI.UniqueGamesTheorem.Appendix.Globality.averageTranslates line 101
  12. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_averageTranslates line 105
  13. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_neg line 112
  14. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_weighted_sum line 117
  15. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_three_terms line 125
  16. def OAI.UniqueGamesTheorem.Appendix.Globality.quadraticFilter line 149
  17. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_quadraticFilter line 155
  18. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_deleted_indicator line 167
  19. abbrev OAI.UniqueGamesTheorem.Appendix.Globality.LineIndex line 175
  20. instance OAI.UniqueGamesTheorem.Appendix.Globality.lineIndexFintype line 177
  21. def OAI.UniqueGamesTheorem.Appendix.Globality.lineShift line 185
  22. def OAI.UniqueGamesTheorem.Appendix.Globality.lineAverage line 188
  23. theorem OAI.UniqueGamesTheorem.Appendix.Globality.lineIndex_nonempty line 192
  24. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_lineAverage line 196
  25. abbrev OAI.UniqueGamesTheorem.Appendix.Globality.HyperplaneIndex line 202
  26. instance OAI.UniqueGamesTheorem.Appendix.Globality.hyperplaneIndexFintype line 204
  27. def OAI.UniqueGamesTheorem.Appendix.Globality.hyperplaneShift line 213
  28. def OAI.UniqueGamesTheorem.Appendix.Globality.hyperplaneAverage line 216
  29. theorem OAI.UniqueGamesTheorem.Appendix.Globality.hyperplaneIndex_nonempty line 221
  30. theorem OAI.UniqueGamesTheorem.Appendix.Globality.restrictionGlobal_hyperplaneAverage line 231
  31. def OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node line 257
  32. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node_pos line 261
  33. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node_eq_inv_pow line 266
  34. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node_add_le line 271
  35. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node_antitone line 278
  36. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node_le_one line 282
  37. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.node_gap line 285
  38. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.step_coefficient_bound line 291
  39. def OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.multiplier line 307
  40. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.multiplier_succ line 310
  41. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.multiplier_target line 315
  42. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.multiplier_below line 322
  43. def OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.linearMapFintype line 326
  44. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.linearNoiseEigenvalue_uniform line 340
  45. def OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.rankNoise line 370
  46. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.rankNoise_eq_average line 377
  47. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.global_average_family line 388
  48. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.rankNoise_global line 397
  49. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.global_nonneg line 413
  50. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.global_mono_bound line 423
  51. def OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.step line 428
  52. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.step_global line 432
  53. def OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.iterateFilter line 471
  54. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.iterateFilter_global line 476
  55. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.rankNoise_coeff line 489
  56. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.coefficient_linearCombination line 500
  57. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.step_coeff line 507
  58. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.iterateFilter_coeff line 520
  59. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.iterateFilter_coeff_low line 527
  60. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.rankLevel_eq_projector line 540
  61. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.filtered_compression_projector line 547
  62. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.hybridDerivative_rankLevel_eq_local_projection line 583
  63. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.hybridDerivative_rankLevel_energy_le_strong line 593
  64. theorem OAI.UniqueGamesTheorem.Appendix.RankLevelFilter.hybridDerivative_rankLevel_energy_le line 609
  65. theorem OAI.UniqueGamesTheorem.Appendix.SelectorEnergy.hybridSelectorEnergy_le line 647
  66. theorem OAI.UniqueGamesTheorem.Appendix.SelectorEnergy.hybridMomentSum_rankLevel_le line 669
  67. theorem OAI.UniqueGamesTheorem.Appendix.LevelTheorem.rankLevel_fourth_moment_le line 723
  68. theorem OAI.UniqueGamesTheorem.Appendix.LevelTheorem.theorem23 line 743
  69. def OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.levelCutoffConstant line 770
  70. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.levelCutoffConstant_nonneg line 774
  71. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.sum_rank_le line 784
  72. def OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.unrestrictedEquiv line 799
  73. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.order_bot_top line 806
  74. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.expect_unrestricted line 810
  75. def OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.rankCutoffEnergy line 830
  76. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.rankCutoffEnergy_eq_sum_exactRankMass line 834
  77. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.rankCutoffEnergy_eq_sum_rankLevel line 840
  78. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.frequencyRank_eq_zero_iff line 846
  79. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.linearCoeff_zero_frequency line 850
  80. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.rankZero_energy line 854
  81. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.fullSecondMoment_le_of_global line 863
  82. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.fullMean_le_of_boolean_global line 869
  83. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.remainder_isRestrictionGlobal_of_le line 876
  84. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.rankCutoffEnergy_le_of_theorem23 line 884
  85. theorem OAI.UniqueGamesTheorem.Fourier.MatrixLevelBridge.remainder_rankCutoff_le line 913