OAI/Computability/UniqueGames/PCP/SourceNoiseParameterLemmas.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

An executable finite-noise denominator for a positive rational target error. Using the stored rational denominator avoids rounding, searches, and choice.

  1. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator line 27

    Source documentation

    A positive rational has numerator at least one, so its reciprocal denominator is no larger than the rational itself. Adding two also ensures the noise parameter is at most one half for every input.

    def noiseDenominator (ξ : ℚ) : ℕ := ξ.den + 2
  2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_ge_two line 29
  3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_pos line 33
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_pos line 36
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le_half line 41
  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le line 48

    Source documentation

    The actual computed reciprocal noise is below every positive target.

    theorem noiseDenominator_inv_le {ξ : ℚ} (hξ : 0 < ξ) :
    (noiseDenominator ξ : ℚ)⁻¹ ≤ ξ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceNoiseParameter.noiseDenominator

  7. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.Cube line 81
  8. def OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign line 83
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign_sq line 85
  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign_xor line 88
  11. def OAI.UniqueGamesTheorem.Foundations.Hastad.cubeXor line 92
  12. def OAI.UniqueGamesTheorem.Foundations.Hastad.walsh line 94
  13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_symm line 97
  14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_sq line 101
  15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_xor line 105
  16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.coordinate_orthogonality line 113
  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_sum_orthogonality line 118
  18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_orthogonality line 135
  19. def OAI.UniqueGamesTheorem.Foundations.Hastad.coefficient line 142
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_inversion line 145
  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_inner line 162
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_parseval line 179
  23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.sign_parseval line 183
  24. def OAI.UniqueGamesTheorem.Foundations.Hastad.support line 205
  25. def OAI.UniqueGamesTheorem.Foundations.Hastad.noiseWeight line 207
  26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.noiseWeight_nonneg line 211
  27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.noiseWeight_sum line 217
  28. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.noise_walsh line 222
  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.thirdQuery line 237

    Source documentation

    The third queried Boolean table is g * (f ∘ π) * μ in sign notation.

    def thirdQuery (π : J → I) (f : Cube I) (g μ : Cube J) : Cube J :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_autocorrelation line 241

    Source documentation

    Walsh autocorrelation, proved by expanding the explicit basis.

    theorem walsh_autocorrelation (B : Cube J → ℝ) (h : Cube J) :
    (𝔼 g, B g * B (cubeXor g h)) =
      ∑ s, coefficient B s ^ 2 * walsh s h := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.cubeXor, OAI.UniqueGamesTheorem.Foundations.Hastad.coefficient, OAI.UniqueGamesTheorem.Foundations.Hastad.walsh

  31. def OAI.UniqueGamesTheorem.Foundations.Hastad.projectedCoefficient line 259
  32. def OAI.UniqueGamesTheorem.Foundations.Hastad.testBias line 262
  33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testBias_fourier line 266
  34. def OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance line 294
  35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.threeBit_indicator line 299
  36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance_eq line 305

    Source documentation

    Actual acceptance is one half plus one half of the three-answer correlation.

    theorem testAcceptance_eq (ε : ℝ) (π : J → I)
    (A : Cube I → Bool) (B : Cube J → Bool) :
    testAcceptance ε π A B =
      (1 + testBias ε π (fun f => bitSign (A f)) (fun g => bitSign (B g))) / 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance, OAI.UniqueGamesTheorem.Foundations.Hastad.testBias, OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign

  37. def OAI.UniqueGamesTheorem.Foundations.Hastad.cubeFlip line 344
  38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.cubeFlip_cubeFlip line 347
  39. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign_not line 351
  40. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.sum_cubeFlip line 354
  41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.coefficient_zero_of_odd line 366
  42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.coefficient_sign_zero_of_folded line 375
  43. def OAI.UniqueGamesTheorem.Foundations.Hastad.representative line 382
  44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.representative_at line 386
  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.representative_flip line 391
  46. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube line 395
  47. def OAI.UniqueGamesTheorem.Foundations.Hastad.canonicalInput line 397
  48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.canonicalInput_flip line 401
  49. def OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer line 407

    Source documentation

    One stored bit and one explicit sign correction for every queried table.

    def foldedAnswer (i₀ : I) (table : HalfCube i₀ → Bool) (f : Cube I) : Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer_flip line 411
  51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer_zero_coefficient line 419
  52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer_dictator line 424
  53. def OAI.UniqueGamesTheorem.Foundations.Hastad.coordinateMask line 429
  54. def OAI.UniqueGamesTheorem.Foundations.Hastad.cubeToggle line 431
  55. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.cubeToggle_twice line 435
  56. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_coordinateMask line 441
  57. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_cubeToggle line 451
  58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.sum_cubeToggle line 456
  59. def OAI.UniqueGamesTheorem.Foundations.Hastad.restrictQuery line 469
  60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.restrictQuery_cubeToggle line 473
  61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditioned_coefficient_zero_invalid line 484
  62. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditioned_coefficient_support line 496

    Source documentation

    Every coordinate returned from a nonzero conditioned Fourier mask is an actual valid local assignment, proved from the concrete restriction map.

    theorem conditioned_coefficient_support (valid : I → Bool)
    (B : Cube {i : I // valid i = true} → ℝ) (s : Cube I)
    (hne : coefficient (fun f => B (restrictQuery valid f)) s ≠ 0) :
    ∀ i ∈ support s, valid i = true := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.coefficient, OAI.UniqueGamesTheorem.Foundations.Hastad.restrictQuery, OAI.UniqueGamesTheorem.Foundations.Hastad.support

  63. def OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer line 506
  64. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer_flip line 511
  65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 518
  66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer_dictator line 525
  67. def OAI.UniqueGamesTheorem.Foundations.Hastad.parityProjection line 550
  68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_support line 553
  69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.sign_power_parity line 561
  70. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.walsh_pullback line 571
  71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.projectedCoefficient_eq line 581
  72. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.projection_has_preimage line 586
  73. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.scaled_geometric_power_le_one line 599

    Source documentation

    A purely algebraic decay estimate used instead of exponential bounds.

    theorem scaled_geometric_power_le_one {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1) (n : Nat) :
    (n : ℝ) * (1 - t) * t ^ n ≤ 1 := by
…
  74. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.noise_decay_bound line 613
  75. def OAI.UniqueGamesTheorem.Foundations.Hastad.zeroMask line 626
  76. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.support_eq_empty_iff line 629
  77. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.parityProjection_zero line 641
  78. def OAI.UniqueGamesTheorem.Foundations.Hastad.agreementProbability line 648

    Source documentation

    Choose uniform coordinates in the two masks and check the projection. An empty support contributes zero.

    def agreementProbability (π : J → I) (a : Cube I) (b : Cube J) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  79. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.agreementProbability_nonneg line 653
  80. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.agreementProbability_projection line 661
  81. def OAI.UniqueGamesTheorem.Foundations.Hastad.decoderSuccess line 689

    Source documentation

    Select independent Walsh masks by squared coefficients and uniform points in each support. The two selections use only the respective private tables.

    def decoderSuccess (π : J → I) (A : Cube I → Bool) (B : Cube J → Bool) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  82. def OAI.UniqueGamesTheorem.Foundations.Hastad.decodingEnergy line 693
  83. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.decodingEnergy_le_success line 696
  84. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.bias_sq_le_weighted_energy line 730
  85. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.decoder_four_epsilon_bias_sq line 747
  86. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.folded_decoder_bound line 774

    Source documentation

    A concrete folded half-table discharges the zero-coefficient condition.

    theorem folded_decoder_bound (ε : ℝ) (π : J → I)
    (i₀ : I) (table : HalfCube i₀ → Bool) (B : Cube J → Bool)
    (hε : 0 < ε) (hε' : ε ≤ 1 / 2) :
    4 * ε * testBias ε π (fun f => bitSign (foldedAnswer i₀ table f))
      (fun g => bitSign (B g)) ^ 2 ≤ decoderSuccess π (foldedAnswer i₀ table) B := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.testBias, OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.decoderSuccess

  87. def OAI.UniqueGamesTheorem.Foundations.Hastad.validAgreementProbability line 782
  88. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.validAgreementProbability_eq line 789
  89. def OAI.UniqueGamesTheorem.Foundations.Hastad.validDecoderSuccess line 802
  90. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditioned_validDecoderSuccess line 810

    Source documentation

    Clause validity in the decoded game follows from the concrete conditioned table; no Fourier-support hypothesis is passed to this theorem.

    theorem conditioned_validDecoderSuccess (valid : J → Bool) (π : J → I)
    (A : Cube I → Bool) (j₀ : {j : J // valid j = true})
    (table : HalfCube j₀ → Bool) :
    validDecoderSuccess valid π A (conditionedFoldedAnswer valid j₀ table) =
      decoderSuccess π A (conditionedFoldedAnswer valid j₀ table) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.validDecoderSuccess, OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.decoderSuccess

  91. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditioned_folded_decoder_bound line 828