OAI/Computability/MaxCut/Graphs/TestCut.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OptimalMaxCut.LongCode.stability_nonneg line 12
2. theorem OAI.OptimalMaxCut.LongCode.stability_le_one line 16
3. theorem OAI.OptimalMaxCut.LongCode.corrAverage_sub line 24
4. theorem OAI.OptimalMaxCut.LongCode.corrAverage_swap line 30
5. theorem OAI.OptimalMaxCut.LongCode.correlation_antipode line 48
6. theorem OAI.OptimalMaxCut.LongCode.Game.oddPart_averageCode line 67
7. def OAI.OptimalMaxCut.LongCode.Game.testCut line 75

   Source documentation

   Value of the usual correlated long-code Max-Cut test, before aggregating its finite rational outcomes into graph weights.

   noncomputable def testCut (G : Game X Y E q) (t : ℝ) (f : X → Cube (Fin q) → ℝ) : ℝ :=
   …

   Mentions: OAI.OptimalMaxCut.LongCode.Game

8. theorem OAI.OptimalMaxCut.LongCode.Game.testCut_stability line 79
9. theorem OAI.OptimalMaxCut.LongCode.Game.testCut_le_stability line 88
10. theorem OAI.OptimalMaxCut.LongCode.Game.stability_soundness line 99

    Source documentation

    Dimension-uniform soundness, with an actual Fourier-influence decoding proof. Every input game soundness bound feeds the finite long-code cut test.

     theorem stability_soundness (G : Game X Y E q) (hq : 0 < q)
        {t ξ τ : ℝ} {K : ℕ} (ht : 0 < t) (ht1 : t < 1) (hξ : 0 < ξ) (hτ : 0 < τ)
        (hMIS : ∀ (n : ℕ) (h : Cube (Fin n) → ℝ),
          (∀ x, -1 ≤ h x ∧ h x ≤ 1) → (𝔼 x, h x) = 0 →
          (∀ i, cutoffInfluence K i h < τ) → stability t h ≤ 2 / Real.pi * Real.arcsin t + ξ)
        (f : X → Cube (Fin q) → ℝ) (hf : ∀ x z, f x z ∈ Set.Icc (-1 : ℝ) 1)
        (hm : ∀ x, (𝔼 z, f x z) = 0) (δ : ℝ) (hsound : G.Sound δ) :
        G.rightLaw.avg (fun y => stability t (G.averageCode f y)) ≤
          2 / Real.pi * Real.arcsin t + ξ + (K : ℝ) * δ / τ := by
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game

11. theorem OAI.OptimalMaxCut.LongCode.Game.exists_test_soundness line 150

    Source documentation

    The MIS threshold and low-degree cutoff are actually proved, not supplied as assumptions. This theorem is the soundness component of the main reduction.

     theorem exists_test_soundness (t ξ : ℝ) (ht : 0 < t) (ht1 : t < 1) (hξ : 0 < ξ) :
        ∃ δ : ℝ, 0 < δ ∧ ∀ {X Y E : Type} [Fintype X] [Fintype Y] [Fintype E]
          (q : ℕ) (_hq : 0 < q) (G : Game X Y E q), G.Sound δ →
          ∀ f : X → Cube (Fin q) → ℝ, (∀ x z, f x z ∈ Set.Icc (-1 : ℝ) 1) →
            G.testCut t f ≤ (1 + 2 / Real.pi * Real.arcsin t) / 2 + ξ := by
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game