OAI/Computability/MinUncut/PCP/CayleySampling.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.CayleySampling.FalseFiber line 17
  2. def OAI.MinUncutGames.Foundations.PCP.CayleySampling.falseRepresentative line 19
  3. def OAI.MinUncutGames.Foundations.PCP.CayleySampling.booleanSplitEquiv line 24
  4. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.booleanSplitEquiv_fst line 40
  5. def OAI.MinUncutGames.Foundations.PCP.CayleySampling.sampleSplitEquiv line 44
  6. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.sampleSplitEquiv_fst line 50
  7. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.card_boolean_split line 54
  8. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.expect_boolean_samples line 59
  9. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.exists_true_of_ne_zero line 81
  10. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.expect_parity_samples line 90
  11. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.expect_walsh_samples line 99
  12. theorem OAI.MinUncutGames.Foundations.PCP.CayleySampling.expect_walsh_mean line 106
  13. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.upperMasks line 125
  14. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.lowerMasks line 128
  15. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.badMasks line 131
  16. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.upperMasks_weight line 136
  17. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 153
  18. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 176
  19. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.ratio_le_of_weight line 190
  20. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 204
  21. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 209
  22. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 214
  23. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 229
  24. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.trueMask line 239
  25. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.countTrue line 242
  26. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.badWord line 244
  27. instance OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.(instance at line 247) line 247
  28. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 250
  29. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.not_badWord_bias line 266
  30. def OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 286
  31. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.twoTail_probability line 296
  32. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.union_bound_le_half line 317
  33. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.fixed_parameters line 334
  34. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.fixed_union_bound line 337
  35. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.seventh_power_size line 341
  36. theorem OAI.MinUncutGames.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 344
  37. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean line 361
  38. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.energy line 363
  39. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.correlation line 365
  40. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.averagingOperator line 368
  41. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.iterateOperator line 371
  42. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeProfile line 376
  43. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeDensity line 379
  44. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.markedStep line 382
  45. def OAI.MinUncutGames.Foundations.PCP.SpectralReturn.returnMass line 386
  46. structure OAI.MinUncutGames.Foundations.PCP.SpectralReturn.SpectralCertificate line 390
  47. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 401
  48. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_equiv line 405
  49. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_prod line 409
  50. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_const line 414
  51. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_add line 417
  52. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_sub line 421
  53. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_mul_left line 425
  54. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_mul_right line 429
  55. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_nonnegative line 433
  56. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_mono line 436
  57. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.energy_nonnegative line 439
  58. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.correlation_sq_le line 442
  59. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.energy_sub_const line 446
  60. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.correlation_sub_const line 455
  61. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_operator line 473
  62. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.operator_sub_const line 483
  63. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_iterate line 491
  64. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.iterate_sub_const line 497
  65. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.mean_markedStep line 504
  66. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 532
  67. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.iterate_energy_bound line 539
  68. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 554
  69. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.correlation_centered line 569
  70. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 583
  71. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 588
  72. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 596
  73. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 600
  74. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 608
  75. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 611
  76. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 617
  77. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 624
  78. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 633
  79. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.returnMass_le line 649
  80. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 659
  81. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.geometric_sum_le line 669
  82. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.sum_returnMass_le line 684
  83. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 704
  84. theorem OAI.MinUncutGames.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 722