OAI/Computability/UniqueGames/PCP/FourierResponseLemmas.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The Fourier decoder is an actual finite law of private answers. Empty Fourier supports use an explicit fallback answer, making every response law normalized even before folding has been imposed.

  1. def OAI.UniqueGamesTheorem.Foundations.Hastad.supportResponse line 23
  2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.supportResponse_expectation line 36
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.fourierResponse line 49

    Source documentation

    Squared Fourier coefficients select a mask; a uniform support coordinate selects the actual answer. Both stages use only this player's private table.

    def fourierResponse (fallback : I) (F : Cube I → Bool) : FiniteDistribution I where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.fourierResponse_expectation line 59
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.response_expectation_nonnegative line 74
  6. def OAI.UniqueGamesTheorem.Foundations.Hastad.responseAgreement line 79
  7. def OAI.UniqueGamesTheorem.Foundations.Hastad.validResponseAgreement line 84
  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.supportResponse_validAgreement line 91
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.validAgreement_le_supportResponses line 105
  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.validDecoderSuccess_le_response line 131
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditioned_folded_response_bound line 150

    Source documentation

    Local soundness now bounds the success of two genuine normalized answer laws. No assumption about randomized decoding or its normalization remains.

    theorem conditioned_folded_response_bound (ε : ℝ) (π : J → I) (valid : J → Bool)
    (i₀ : I) (tableA : HalfCube i₀ → Bool)
    (j₀ : {j : J // valid j = true}) (tableB : HalfCube j₀ → Bool)
    (hε : 0 < ε) (hε' : ε ≤ 1 / 2) :
    4 * ε * testBias ε π (fun f => bitSign (foldedAnswer i₀ tableA f))
      (fun g => bitSign (conditionedFoldedAnswer valid j₀ tableB g)) ^ 2 ≤
      validResponseAgreement valid π i₀ j₀.val (foldedAnswer i₀ tableA)
        (conditionedFoldedAnswer valid j₀ tableB) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.testBias, OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.validResponseAgreement

  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.distribution_sq_expectation_le line 180
  13. def OAI.UniqueGamesTheorem.Foundations.Hastad.projectionGame line 210
  14. def OAI.UniqueGamesTheorem.Foundations.Hastad.questionBias line 215
  15. def OAI.UniqueGamesTheorem.Foundations.Hastad.questionAcceptance line 219
  16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.questionAcceptance_eq line 224
  17. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.ConditionedOracle line 237

    Source documentation

    Storage distinguishes an actually empty legal domain from a folded table over its legal assignments. The empty case needs no nonexistent fold point.

    inductive ConditionedOracle (valid : J → Bool) where
…
  18. def OAI.UniqueGamesTheorem.Foundations.Hastad.ConditionedOracle.answer line 241
  19. def OAI.UniqueGamesTheorem.Foundations.Hastad.ConditionedOracle.fallback line 245
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testBias_constant_right line 251
  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.empty_conditioned_bias line 258
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedOracle_response_bound line 268
  23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.folded_game_decoder_bound line 288
  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedOracle_game_decoder_bound line 328

    Source documentation

    The game bound includes inconsistent clause tuples, whose legal local domain is empty and whose implemented right oracle is constant.

    theorem conditionedOracle_game_decoder_bound
    (questions : FiniteDistribution (Q₁ × Q₂))
    (ε : ℝ) (π : Q₁ → Q₂ → J → I) (valid : Q₂ → J → Bool)
    (i₀ : Q₁ → I) (tableA : ∀ q, HalfCube (i₀ q) → Bool)
    (default : J) (right : ∀ q, ConditionedOracle (valid q))
    (hε : 0 < ε) (hε' : ε ≤ 1 / 2) :
    4 * ε * questions.expectation (questionBias ε π
      (fun q => foldedAnswer (i₀ q) (tableA q)) (fun q => (right q).answer)) ^ 2 ≤
      (projectionGame questions π valid).value := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.ConditionedOracle, OAI.UniqueGamesTheorem.Foundations.Hastad.questionBias, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.projectionGame

  25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedOracle_acceptance_bound line 364