OAI/Computability/MaxCut/Encoding/ThreeBitTest.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Hastad.support line 15
2. def OAI.MaxCutGames.Foundations.Hastad.noiseWeight line 17
3. theorem OAI.MaxCutGames.Foundations.Hastad.noiseWeight_nonneg line 21
4. theorem OAI.MaxCutGames.Foundations.Hastad.noiseWeight_sum line 27
5. theorem OAI.MaxCutGames.Foundations.Hastad.noise_walsh line 32
6. def OAI.MaxCutGames.Foundations.Hastad.thirdQuery line 46

   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.MaxCutGames.Foundations.Hastad.Cube

7. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_autocorrelation line 50

   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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.cubeXor, OAI.MaxCutGames.Foundations.Hastad.coefficient, OAI.MaxCutGames.Foundations.Hastad.walsh

8. def OAI.MaxCutGames.Foundations.Hastad.projectedCoefficient line 68
9. def OAI.MaxCutGames.Foundations.Hastad.testBias line 71
10. theorem OAI.MaxCutGames.Foundations.Hastad.testBias_fourier line 75
11. def OAI.MaxCutGames.Foundations.Hastad.testAcceptance line 103
12. theorem OAI.MaxCutGames.Foundations.Hastad.threeBit_indicator line 108
13. theorem OAI.MaxCutGames.Foundations.Hastad.testAcceptance_eq line 114

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.testAcceptance, OAI.MaxCutGames.Foundations.Hastad.testBias, OAI.MaxCutGames.Foundations.Hastad.bitSign