OAI/Computability/DirectedFeedback/Games/CayleySampling.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.CayleySampling.FalseFiber line 16
  2. def OAI.DFVSGames.Foundations.PCP.CayleySampling.falseRepresentative line 18
  3. def OAI.DFVSGames.Foundations.PCP.CayleySampling.booleanSplitEquiv line 23
  4. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.booleanSplitEquiv_fst line 39
  5. def OAI.DFVSGames.Foundations.PCP.CayleySampling.sampleSplitEquiv line 43
  6. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.sampleSplitEquiv_fst line 49
  7. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.card_boolean_split line 53
  8. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.expect_boolean_samples line 58
  9. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.exists_true_of_ne_zero line 78
  10. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.expect_parity_samples line 87
  11. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.expect_walsh_samples line 96
  12. theorem OAI.DFVSGames.Foundations.PCP.CayleySampling.expect_walsh_mean line 103
  13. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.upperMasks line 119
  14. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.lowerMasks line 122
  15. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.badMasks line 125
  16. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.upperMasks_weight line 130
  17. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 147
  18. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 170
  19. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.ratio_le_of_weight_inline_CayleyTailCount line 184
  20. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 198
  21. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 203
  22. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 208
  23. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 223
  24. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.trueMask line 233
  25. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.countTrue line 236
  26. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.badWord line 238
  27. instance OAI.DFVSGames.Foundations.PCP.CayleyTailCount.(instance at line 241) line 241
  28. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 244
  29. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.not_badWord_bias line 260
  30. def OAI.DFVSGames.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 280
  31. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.twoTail_probability line 290
  32. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.union_bound_le_half line 311
  33. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.fixed_parameters line 328
  34. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.fixed_union_bound line 331
  35. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.seventh_power_size line 335
  36. theorem OAI.DFVSGames.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 338
  37. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean line 353
  38. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.energy line 355
  39. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.correlation line 357
  40. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.averagingOperator line 360
  41. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.iterateOperator line 363
  42. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeProfile line 368
  43. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeDensity line 371
  44. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.markedStep line 374
  45. def OAI.DFVSGames.Foundations.PCP.SpectralReturn.returnMass line 378
  46. structure OAI.DFVSGames.Foundations.PCP.SpectralReturn.SpectralCertificate line 382
  47. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 393
  48. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_equiv line 397
  49. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_prod line 401
  50. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_const line 406
  51. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_add line 409
  52. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_sub line 413
  53. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_mul_left line 417
  54. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_mul_right line 421
  55. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_nonnegative line 425
  56. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_mono line 428
  57. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.energy_nonnegative line 431
  58. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.correlation_sq_le line 434
  59. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.energy_sub_const line 438
  60. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.correlation_sub_const line 447
  61. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_operator line 465
  62. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.operator_sub_const line 475
  63. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_iterate line 483
  64. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.iterate_sub_const line 489
  65. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.mean_markedStep line 497
  66. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 525
  67. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.iterate_energy_bound line 532
  68. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 547
  69. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.correlation_centered line 562
  70. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 577
  71. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 583
  72. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 591
  73. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 595
  74. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 603
  75. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 606
  76. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 612
  77. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 619
  78. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 628
  79. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.returnMass_le line 644
  80. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 654
  81. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.geometric_sum_le line 664
  82. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.sum_returnMass_le line 677
  83. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 697
  84. theorem OAI.DFVSGames.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 715