OAI/Computability/MaxCut/Analysis/CubePerm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OptimalMaxCut.LongCode.cubePerm line 11
2. theorem OAI.OptimalMaxCut.LongCode.cubePerm_apply line 17
3. theorem OAI.OptimalMaxCut.LongCode.degree_cubePerm line 20
4. theorem OAI.OptimalMaxCut.LongCode.walsh_cubePerm line 26
5. def OAI.OptimalMaxCut.LongCode.reindex line 31
6. theorem OAI.OptimalMaxCut.LongCode.coefficient_reindex line 34
7. theorem OAI.OptimalMaxCut.LongCode.mean_reindex line 41
8. theorem OAI.OptimalMaxCut.LongCode.cutoffInfluence_reindex line 45
9. theorem OAI.OptimalMaxCut.LongCode.cutoffInfluence_nonneg line 55
10. def OAI.OptimalMaxCut.LongCode.Game.averageCode line 64

    Source documentation

    A real weighted averaging of all pulled-back odd long codes at a right question. The graph/test itself uses only rational probabilities.

    noncomputable def averageCode (G : Game X Y E q) (f : X → Cube (Fin q) → ℝ)
        (y : Y) (z : Cube (Fin q)) : ℝ :=
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game

11. theorem OAI.OptimalMaxCut.LongCode.Game.averageCode_bounded line 68
12. theorem OAI.OptimalMaxCut.LongCode.Game.averageCode_mean line 73
13. theorem OAI.OptimalMaxCut.LongCode.Game.averageCode_influence line 80
14. theorem OAI.OptimalMaxCut.LongCode.Game.decoding_bound line 89

    Source documentation

    Low-degree Fourier influence decodes an actual labeling. There is no assumed decoder or hardness assertion in this inequality.

     theorem decoding_bound (G : Game X Y E q) (hq : 0 < q) (K : ℕ)
        (f : X → Cube (Fin q) → ℝ) (hf : ∀ x z, f x z ∈ Set.Icc (-1 : ℝ) 1)
        (δ : ℝ) (hsound : G.Sound δ) (ly : Y → Fin q) :
        G.rightLaw.avg (fun y => (G.edgeLaw y).avg (fun e =>
          cutoffInfluence K ((G.permutation e).symm (ly y)) (f (G.source e)))) ≤ (K : ℝ) * δ := by
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game