OAI/Computability/VertexCover/PCP/SpectralReturn.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean line 15
  2. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.energy line 17
  3. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.correlation line 19
  4. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.averagingOperator line 22
  5. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.iterateOperator line 25
  6. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeProfile line 30
  7. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeDensity line 33
  8. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.markedStep line 36
  9. def OAI.UniqueGames.Foundations.PCP.SpectralReturn.returnMass line 40
  10. structure OAI.UniqueGames.Foundations.PCP.SpectralReturn.SpectralCertificate line 44
  11. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 55
  12. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_equiv line 59
  13. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_prod line 63
  14. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_const line 68
  15. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_add line 71
  16. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_sub line 75
  17. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_mul_left line 79
  18. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_mul_right line 83
  19. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_nonnegative line 87
  20. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_mono line 90
  21. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.energy_nonnegative line 93
  22. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.correlation_sq_le line 96
  23. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.energy_sub_const line 100
  24. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.correlation_sub_const line 109
  25. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_operator line 127
  26. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.operator_sub_const line 137
  27. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_iterate line 145
  28. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.iterate_sub_const line 151
  29. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.mean_markedStep line 159
  30. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 187
  31. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.iterate_energy_bound line 194
  32. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 209
  33. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.correlation_centered line 224
  34. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 239
  35. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 245
  36. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 253
  37. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 257
  38. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 265
  39. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 268
  40. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 274
  41. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 281
  42. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 290
  43. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.returnMass_le line 306
  44. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 316
  45. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.geometric_sum_le line 326
  46. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.sum_returnMass_le line 339
  47. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 359
  48. theorem OAI.UniqueGames.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 377