Analysis of Boolean Functions in Lean

7.4. Håstad’s hardness theorems🔗

Proposition7.4.1
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 7.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 7.5.20
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4fidelity-exact

Proposition 7.36. A uniformly random Boolean assignment satisfies each three-literal clause with probability 7/8. Hence it is a randomized (7/8,\beta)-approximation for Max-E3-Sat for every \beta.

Lean code for Proposition7.4.1●4 theorems
  • theoremdefined in FABL/Chapter07/CSP.lean
    complete
    theorem FABL.expect_e3SatPredicate (negated : Fin 3 → Bool) :
  (Finset.univ.expect fun values =>
      if FABL.e3SatPredicate negated values = true then 1 else 0) =
    7 / 8
    theorem FABL.expect_e3SatPredicate
  (negated : Fin 3 → Bool) :
  (Finset.univ.expect fun values =>
      if
          FABL.e3SatPredicate negated
              values =
            true then
        1
      else 0) =
    7 / 8
    A uniformly random assignment satisfies each fixed exact-three-literal clause with
probability `7/8`.
  • theoremdefined in FABL/Chapter07/CSP.lean
    complete
    theorem FABL.expect_satisfiedIndicator_maxE3Sat.{v} {V : Type v} [Fintype V]
  [DecidableEq V] (c : FABL.CSPConstraint FABL.maxE3SatTemplate V) :
  (Finset.univ.expect fun assignment =>
      ↑(c.satisfiedIndicator assignment)) =
    7 / 8
    theorem FABL.expect_satisfiedIndicator_maxE3Sat.{v}
  {V : Type v} [Fintype V] [DecidableEq V]
  (c :
    FABL.CSPConstraint
      FABL.maxE3SatTemplate V) :
  (Finset.univ.expect fun assignment =>
      ↑(c.satisfiedIndicator
          assignment)) =
    7 / 8
    The expected satisfaction indicator of one E3-Sat constraint under a uniform assignment is
`7/8`. Distinctness of the three coordinates is supplied by the constraint's embedded scope.
  • theoremdefined in FABL/Chapter07/CSP.lean
    complete
    theorem FABL.expect_value_maxE3Sat.{v} {V : Type v} [Fintype V] [DecidableEq V]
  (P : FABL.CSPInstance FABL.maxE3SatTemplate V) :
  (Finset.univ.expect fun assignment => P.value assignment) = 7 / 8
    theorem FABL.expect_value_maxE3Sat.{v}
  {V : Type v} [Fintype V] [DecidableEq V]
  (P :
    FABL.CSPInstance FABL.maxE3SatTemplate
      V) :
  (Finset.univ.expect fun assignment =>
      P.value assignment) =
    7 / 8
    O'Donnell, Proposition 7.36: the expected value of an E3-Sat instance under a uniformly
random assignment is `7/8`.
  • theoremdefined in FABL/Chapter07/CSP.lean
    complete
    theorem FABL.seven_eighths_le_optimum_maxE3Sat.{v} {V : Type v} [Finite V]
  (P : FABL.CSPInstance FABL.maxE3SatTemplate V) : 7 / 8 ≤ P.optimum
    theorem FABL.seven_eighths_le_optimum_maxE3Sat.{v}
  {V : Type v} [Finite V]
  (P :
    FABL.CSPInstance FABL.maxE3SatTemplate
      V) :
  7 / 8 ≤ P.optimum
    In particular, every E3-Sat instance has an assignment satisfying at least a `7/8`
fraction of its constraints.
Theorem7.4.2
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 7.3.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagssection-7-4external-dependencystatement-only

Håstad's 3-Sat Hardness Theorem. For every constant \delta>0, an (7/8+\delta,1)-approximation for Max-E3-Sat is NP-hard.

This external hardness theorem supplies no assumption to the production library.

Theorem7.4.3
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 7.3.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N
Tagssection-7-4external-dependencystatement-only

Håstad's 3-Lin Hardness Theorem. For every constant \delta>0, an (1/2+\delta,1-\delta)-approximation for Max-E3-Lin is NP-hard.

This external hardness theorem supplies no assumption to the production library.

Lemma7.4.4
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0XL∃∀N
Tagssection-7-4external-dependencystatement-only

Bellare, Goldreich, and Sudan established the explicit Max-E3-Sat hardness gap \delta_0=.026. This quoted historical bound is external and supplies no assumption to the production library.

Definition7.4.5
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 6.1.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 11
Reverse dependency previews
Preview
Lemma 7.4.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4fidelity-explicit-randomized-assignment

Definition 7.37. Let \Psi be a finite set of Boolean predicates, let 0<\alpha<\beta\le1, and let \lambda:[0,1]\to[0,1] satisfy \lambda(\epsilon)\to0 as \epsilon\to0. An (\alpha,\beta) Dictator-vs.-No-Notables test using \Psi is a family, for every n>0, of function testers such that:

  1. every dictator is accepted with probability at least \beta;

  2. every f:\{-1,1\}^n\to[-1,1] satisfying \operatorname{Inf}^{(1-\epsilon)}_i[f]\le\epsilon \quad\text{for every }i is accepted with probability at most \alpha+\lambda(\epsilon); and

  3. every acceptance predicate used by the tester belongs to \Psi.

For real-valued f, a query answer is an independent random sign whose mean is the queried value of f; the predicate is evaluated on those signs. Query positions may repeat.

Lean code for Definition7.4.5●12 declarations
  • structure(2 fields)defined in FABL/Chapter07/HastadTests.lean
    complete
    structure FABL.SignPredicate : Type
    structure FABL.SignPredicate : Type
    A Boolean predicate over the sign domain, with its arity retained in the data.

    Fields

    arity : ℕ
    Number of predicate inputs. 
    accepts : (Fin self.arity → FABL.Sign) → Bool
    Boolean acceptance decision.
  • structure(2 fields)defined in FABL/Chapter07/HastadTests.lean
    complete
    structure FABL.SignQueryCheck (n : ℕ) : Type
    structure FABL.SignQueryCheck (n : ℕ) : Type
    A predicate together with the query string occupying each of its input positions.

No injectivity condition is imposed on `queries`: this is the repeated-query amendment in
Remark 7.38.

    Fields

    predicate : FABL.SignPredicate
    Predicate used by this check. 
    queries : Fin self.predicate.arity → FABL.SignCube n
    Query at each predicate input position.
  • structure(4 fields)defined in FABL/Chapter07/HastadTests.lean
    complete
    structure FABL.SignTester (n : ℕ) : Type 1
    structure FABL.SignTester (n : ℕ) : Type 1
    A finite randomized, nonadaptive tester.  Its random seed may have an arbitrary finite PMF.

    Fields

    Seed : Type
    Finite random-seed type. 
    seedFintype : Fintype self.Seed
    Finiteness of the random-seed type. 
    seedLaw : PMF self.Seed
    Tester randomness. 
    check : self.Seed → FABL.SignQueryCheck n
    Deterministic check selected by a seed.
  • structure(2 fields)defined in FABL/Chapter07/HastadTests.lean
    complete
    structure FABL.BoundedCubeFunction (n : ℕ) : Type
    structure FABL.BoundedCubeFunction (n : ℕ) : Type
    A real-valued cube function whose values are valid means of random signs.

    Fields

    toFun : FABL.SignCube n → ℝ
    Underlying real-valued function. 
    mem_Icc : ∀ (x : FABL.SignCube n), self.toFun x ∈ Set.Icc (-1) 1
    Every value lies in `[-1,1]`.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.BoundedCubeFunction.ofBoolean {n : ℕ}
  (f : FABL.BooleanFunction n) : FABL.BoundedCubeFunction n
    def FABL.BoundedCubeFunction.ofBoolean {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.BoundedCubeFunction n
    A Boolean function regarded as a bounded real-valued cube function.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.signPMFOfMean (μ : ℝ) (hμ : μ ∈ Set.Icc (-1) 1) : PMF FABL.Sign
    def FABL.signPMFOfMean (μ : ℝ)
  (hμ : μ ∈ Set.Icc (-1) 1) :
  PMF FABL.Sign
    The sign distribution with prescribed mean `μ ∈ [-1,1]`.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.pmfExpectation_signPMFOfMean (μ : ℝ) (hμ : μ ∈ Set.Icc (-1) 1) :
  FABL.pmfExpectation (FABL.signPMFOfMean μ hμ) FABL.signValue = μ
    theorem FABL.pmfExpectation_signPMFOfMean (μ : ℝ)
  (hμ : μ ∈ Set.Icc (-1) 1) :
  FABL.pmfExpectation
      (FABL.signPMFOfMean μ hμ)
      FABL.signValue =
    μ
    The prescribed-mean sign distribution has expectation `μ`.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.SignPredicate.randomizedValue (P : FABL.SignPredicate)
  (μ : Fin P.arity → ℝ)
  (hμ : ∀ (i : Fin P.arity), μ i ∈ Set.Icc (-1) 1) : ℝ
    def FABL.SignPredicate.randomizedValue
  (P : FABL.SignPredicate)
  (μ : Fin P.arity → ℝ)
  (hμ :
    ∀ (i : Fin P.arity),
      μ i ∈ Set.Icc (-1) 1) :
  ℝ
    Randomized-assignment value of a predicate at a vector of means in `[-1,1]`.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.SignQueryCheck.randomizedValue {n : ℕ} (C : FABL.SignQueryCheck n)
  (f : FABL.BoundedCubeFunction n) : ℝ
    def FABL.SignQueryCheck.randomizedValue
  {n : ℕ} (C : FABL.SignQueryCheck n)
  (f : FABL.BoundedCubeFunction n) : ℝ
    Acceptance value of one query check on a bounded real-valued function.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.SignTester.acceptanceProbability {n : ℕ} (T : FABL.SignTester n)
  (f : FABL.BoundedCubeFunction n) : ℝ
    def FABL.SignTester.acceptanceProbability
  {n : ℕ} (T : FABL.SignTester n)
  (f : FABL.BoundedCubeFunction n) : ℝ
    Acceptance probability of a finite tester on a bounded real-valued function.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.SignTester.UsesPredicates {n : ℕ} (T : FABL.SignTester n)
  (Ψ : Set FABL.SignPredicate) : Prop
    def FABL.SignTester.UsesPredicates {n : ℕ}
  (T : FABL.SignTester n)
  (Ψ : Set FABL.SignPredicate) : Prop
    A tester uses only predicates from `Ψ`.
  • structure(9 fields)defined in FABL/Chapter07/HastadTests.lean
    complete
    structure FABL.IsDictatorVsNoNotablesTest (Ψ : Set FABL.SignPredicate) (α β : ℝ)
  (error : ℝ → ℝ) (T : (n : ℕ) → 0 < n → FABL.SignTester n) : Prop
    structure FABL.IsDictatorVsNoNotablesTest
  (Ψ : Set FABL.SignPredicate) (α β : ℝ)
  (error : ℝ → ℝ)
  (T :
    (n : ℕ) → 0 < n → FABL.SignTester n) :
  Prop
    O'Donnell, Definition 7.37 with both amendments from Remark 7.38.

Soundness is required for all functions into `[-1,1]`, interpreted by independent randomized
signs at predicate input positions, and query tuples need not be injective.

    Fields

    predicateSet_finite : Ψ.Finite
    The allowed predicate set is finite. 
    alpha_pos : 0 < α
    The lower distinguishing parameter is positive. 
    alpha_lt_beta : α < β
    The distinguishing gap is nontrivial. 
    beta_le_one : β ≤ 1
    Acceptance targets are probabilities. 
    error_mem_Icc : ∀ ε ∈ Set.Icc 0 1, error ε ∈ Set.Icc 0 1
    The error function maps `[0,1]` to `[0,1]`. 
    error_tendsto_zero : Filter.Tendsto error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
    The soundness error tends to zero with the notable-coordinate threshold. 
    usesPredicates : ∀ (n : ℕ) (hn : 0 < n), (T n hn).UsesPredicates Ψ
    Every check uses an allowed predicate. 
    dictator_complete : ∀ (n : ℕ) (hn : 0 < n) (i : Fin n),
  β ≤ (T n hn).acceptanceProbability (FABL.BoundedCubeFunction.ofBoolean (FABL.dictator i))
    Every dictator is accepted with probability at least `β`. 
    noNotables_sound : ∀ (n : ℕ) (hn : 0 < n),
  ∀ ε ∈ Set.Icc 0 1,
    ∀ (f : FABL.BoundedCubeFunction n),
      FABL.HasSmallStableInfluences ε ε f.toFun → (T n hn).acceptanceProbability f ≤ α + error ε
    Functions with no `(ε,ε)`-notable coordinate have acceptance at most `α + λ(ε)`.
Lemma7.4.6
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 7.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-7-4fidelity-exact

Remark 7.38. Soundness in Definition 7.37 must hold on the full range [-1,1], with the randomized-answer interpretation proved in Exercise 7.22. The tester may repeat query strings; Exercise 7.31 reconciles this with the injective-scope convention for CSP instances.

Lean code for Lemma7.4.6●3 theorems
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.SignPredicate.randomizedValue_mem_Icc (P : FABL.SignPredicate)
  (μ : Fin P.arity → ℝ)
  (hμ : ∀ (i : Fin P.arity), μ i ∈ Set.Icc (-1) 1) :
  P.randomizedValue μ hμ ∈ Set.Icc 0 1
    theorem FABL.SignPredicate.randomizedValue_mem_Icc
  (P : FABL.SignPredicate)
  (μ : Fin P.arity → ℝ)
  (hμ :
    ∀ (i : Fin P.arity),
      μ i ∈ Set.Icc (-1) 1) :
  P.randomizedValue μ hμ ∈ Set.Icc 0 1
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.SignQueryCheck.randomizedValue_mem_Icc {n : ℕ}
  (C : FABL.SignQueryCheck n) (f : FABL.BoundedCubeFunction n) :
  C.randomizedValue f ∈ Set.Icc 0 1
    theorem FABL.SignQueryCheck.randomizedValue_mem_Icc
  {n : ℕ} (C : FABL.SignQueryCheck n)
  (f : FABL.BoundedCubeFunction n) :
  C.randomizedValue f ∈ Set.Icc 0 1
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.SignTester.acceptanceProbability_mem_Icc {n : ℕ}
  (T : FABL.SignTester n) (f : FABL.BoundedCubeFunction n) :
  T.acceptanceProbability f ∈ Set.Icc 0 1
    theorem FABL.SignTester.acceptanceProbability_mem_Icc
  {n : ℕ} (T : FABL.SignTester n)
  (f : FABL.BoundedCubeFunction n) :
  T.acceptanceProbability f ∈ Set.Icc 0 1
Lemma7.4.7
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
Tagssection-7-4fidelity-exact

Remark 7.39. The error term \lambda(\epsilon)=o_\epsilon(1) is uniform in the dimension n.

Lean code for Lemma7.4.7●3 declarations
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.hastadSoundnessError (noise ε : ℝ) : ℝ
    def FABL.hastadSoundnessError (noise ε : ℝ) :
  ℝ
    Soundness error used for Theorem 7.42.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastadSoundnessError_mem_Icc (noise ε : ℝ) (hε : ε ∈ Set.Icc 0 1) :
  FABL.hastadSoundnessError noise ε ∈ Set.Icc 0 1
    theorem FABL.hastadSoundnessError_mem_Icc
  (noise ε : ℝ) (hε : ε ∈ Set.Icc 0 1) :
  FABL.hastadSoundnessError noise ε ∈
    Set.Icc 0 1
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastadSoundnessError_tendsto_zero (noise : ℝ)
  (hnoise : 0 < noise) :
  Filter.Tendsto (FABL.hastadSoundnessError noise)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
    theorem FABL.hastadSoundnessError_tendsto_zero
  (noise : ℝ) (hnoise : 0 < noise) :
  Filter.Tendsto
    (FABL.hastadSoundnessError noise)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Theorem7.4.8
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 7.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Corollary 7.4.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4complexity-boundaryfidelity-partial-explicit-machine-and-refinement-witnesses

Theorem 7.40. If an (\alpha,\beta) Dictator-vs.-No-Notables test using \Psi exists, then, for every \delta>0, the promise problem of (\alpha+\delta,\beta-\delta)-approximating Max-CSP(\Psi) is UG-hard.

Here UG-hardness is polynomial-time promise reducibility from sufficiently small-gap Unique-Games instances; it is not ordinary computable reducibility. The production theorem proves the finite completeness and soundness implications, real-threshold budget, predicate transport, and promise-reduction composition. Its machine-level endpoint is deliberately conditional on an explicit regular-UG optimum encoding, a uniform refinement of the tester law, a target codec with the proved optimum law, a CSLib PolytimeMap satisfying the canonical output equation, and an external source-to-UG gap witness. None of these witnesses is manufactured as an axiom or hidden inside the correctness conclusion.

Lean code for Theorem7.4.8●2 theorems
  • theoremdefined in FABL/Chapter07/UniqueGamesReduction.lean
    complete
    theorem FABL.EncodedRegularUniqueGamesFamily.longCodeFiniteTransform_reducesGap.{u_1,
    u_2}
  {q : ℕ} (family : FABL.EncodedRegularUniqueGamesFamily q)
  [Nonempty (Fin q)] {Ψ : Set FABL.SignPredicate} {α β : ℝ}
  {error : ℝ → ℝ} {T : (n : ℕ) → 0 < n → FABL.SignTester n}
  (hTest : FABL.IsDictatorVsNoNotablesTest Ψ α β error T) (hq : 0 < q)
  (encoding : family.OptimizationEncoding)
  (transform : family.LongCodeFiniteTransform ⋯)
  (codec : family.LongCodeOutputCodec transform)
  (machine : family.LongCodeTransformMachine codec)
  (ugSoundness ugCompleteness targetSoundness targetCompleteness : ℝ)
  (hugGap : ugSoundness < ugCompleteness)
  (htargetGap : targetSoundness < targetCompleteness) (δUG ε τ : ℝ)
  (hε : ε ∈ Set.Ioc 0 1) (hugCompleteness : 1 - δUG ≤ ugCompleteness)
  (hugSoundness : ugSoundness < τ * ε ^ 5 / 18)
  (htargetCompleteness :
    targetCompleteness ≤
      β - ↑transform.r * δUG - ↑transform.r ^ 2 / ↑transform.M)
  (htargetSoundness :
    α + error ε + τ + ↑transform.r ^ 2 / ↑transform.M ≤
      targetSoundness) :
  FABL.PromiseKarpReducible
    (encoding.problem.gapPromiseReal ugSoundness ugCompleteness hugGap)
    (codec.target.gapPromiseReal targetSoundness targetCompleteness
      htargetGap)
    theorem FABL.EncodedRegularUniqueGamesFamily.longCodeFiniteTransform_reducesGap.{u_1,
    u_2}
  {q : ℕ}
  (family :
    FABL.EncodedRegularUniqueGamesFamily
      q)
  [Nonempty (Fin q)]
  {Ψ : Set FABL.SignPredicate} {α β : ℝ}
  {error : ℝ → ℝ}
  {T :
    (n : ℕ) → 0 < n → FABL.SignTester n}
  (hTest :
    FABL.IsDictatorVsNoNotablesTest Ψ α β
      error T)
  (hq : 0 < q)
  (encoding : family.OptimizationEncoding)
  (transform :
    family.LongCodeFiniteTransform ⋯)
  (codec :
    family.LongCodeOutputCodec transform)
  (machine :
    family.LongCodeTransformMachine codec)
  (ugSoundness ugCompleteness
    targetSoundness targetCompleteness :
    ℝ)
  (hugGap : ugSoundness < ugCompleteness)
  (htargetGap :
    targetSoundness < targetCompleteness)
  (δUG ε τ : ℝ) (hε : ε ∈ Set.Ioc 0 1)
  (hugCompleteness :
    1 - δUG ≤ ugCompleteness)
  (hugSoundness :
    ugSoundness < τ * ε ^ 5 / 18)
  (htargetCompleteness :
    targetCompleteness ≤
      β - ↑transform.r * δUG -
        ↑transform.r ^ 2 / ↑transform.M)
  (htargetSoundness :
    α + error ε + τ +
        ↑transform.r ^ 2 / ↑transform.M ≤
      targetSoundness) :
  FABL.PromiseKarpReducible
    (encoding.problem.gapPromiseReal
      ugSoundness ugCompleteness hugGap)
    (codec.target.gapPromiseReal
      targetSoundness targetCompleteness
      htargetGap)
    Theorem 7.40's stable-influence specialization of the finite long-code reduction.
  • theoremdefined in FABL/Chapter07/UniqueGamesReduction.lean
    complete
    theorem FABL.EncodedRegularUniqueGamesFamily.conditional_uniqueGames_hardness.{u_1,
    u_2}
  {q : ℕ} (family : FABL.EncodedRegularUniqueGamesFamily q)
  [Nonempty (Fin q)] {source : FABL.BinaryPromiseProblem}
  {Ψ : Set FABL.SignPredicate} {α β : ℝ} {error : ℝ → ℝ}
  {T : (n : ℕ) → 0 < n → FABL.SignTester n}
  (hTest : FABL.IsDictatorVsNoNotablesTest Ψ α β error T) (hq : 0 < q)
  (encoding : family.OptimizationEncoding)
  (UG : family.GapHypothesis source encoding)
  (transform : family.LongCodeFiniteTransform ⋯)
  (codec : family.LongCodeOutputCodec transform)
  (machine : family.LongCodeTransformMachine codec)
  (targetSoundness targetCompleteness : ℝ)
  (htargetGap : targetSoundness < targetCompleteness) (δUG ε τ : ℝ)
  (hε : ε ∈ Set.Ioc 0 1) (hugCompleteness : 1 - δUG ≤ UG.completeness)
  (hugSoundness : UG.soundness < τ * ε ^ 5 / 18)
  (htargetCompleteness :
    targetCompleteness ≤
      β - ↑transform.r * δUG - ↑transform.r ^ 2 / ↑transform.M)
  (htargetSoundness :
    α + error ε + τ + ↑transform.r ^ 2 / ↑transform.M ≤
      targetSoundness) :
  FABL.PromiseKarpReducible source
    (codec.target.gapPromiseReal targetSoundness targetCompleteness
      htargetGap)
    theorem FABL.EncodedRegularUniqueGamesFamily.conditional_uniqueGames_hardness.{u_1,
    u_2}
  {q : ℕ}
  (family :
    FABL.EncodedRegularUniqueGamesFamily
      q)
  [Nonempty (Fin q)]
  {source : FABL.BinaryPromiseProblem}
  {Ψ : Set FABL.SignPredicate} {α β : ℝ}
  {error : ℝ → ℝ}
  {T :
    (n : ℕ) → 0 < n → FABL.SignTester n}
  (hTest :
    FABL.IsDictatorVsNoNotablesTest Ψ α β
      error T)
  (hq : 0 < q)
  (encoding : family.OptimizationEncoding)
  (UG :
    family.GapHypothesis source encoding)
  (transform :
    family.LongCodeFiniteTransform ⋯)
  (codec :
    family.LongCodeOutputCodec transform)
  (machine :
    family.LongCodeTransformMachine codec)
  (targetSoundness targetCompleteness : ℝ)
  (htargetGap :
    targetSoundness < targetCompleteness)
  (δUG ε τ : ℝ) (hε : ε ∈ Set.Ioc 0 1)
  (hugCompleteness :
    1 - δUG ≤ UG.completeness)
  (hugSoundness :
    UG.soundness < τ * ε ^ 5 / 18)
  (htargetCompleteness :
    targetCompleteness ≤
      β - ↑transform.r * δUG -
        ↑transform.r ^ 2 / ↑transform.M)
  (htargetSoundness :
    α + error ε + τ +
        ↑transform.r ^ 2 / ↑transform.M ≤
      targetSoundness) :
  FABL.PromiseKarpReducible source
    (codec.target.gapPromiseReal
      targetSoundness targetCompleteness
      htargetGap)
    Honest conditional form of Theorem 7.40: compose an explicit UGC-style source witness with
the proved finite long-code reduction.
Theorem7.4.9
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 7.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-7-4fidelity-exact

Theorem 7.41. For every 0<\delta<1/8, there is a (7/8+\delta,1) Dictator-vs.-No-Notables test all of whose predicates are three-literal OR predicates.

Lean code for Theorem7.4.9●2 declarations
  • defdefined in FABL/Chapter07/HastadThreeSat.lean
    complete
    def FABL.hastadThreeSatTesterFamily (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 (1 / 8))
  (n : ℕ) (hn : 0 < n) : FABL.SignTester n
    def FABL.hastadThreeSatTesterFamily (δ : ℝ)
  (hδ : δ ∈ Set.Ioo 0 (1 / 8)) (n : ℕ)
  (hn : 0 < n) : FABL.SignTester n
    The E3-Sat tester family obtained from the OXR family by the exact two-clause replacement.
  • theoremdefined in FABL/Chapter07/HastadThreeSat.lean
    complete
    theorem FABL.hastadThreeSat_dictatorVsNoNotables (δ : ℝ)
  (hδ : δ ∈ Set.Ioo 0 (1 / 8)) :
  FABL.IsDictatorVsNoNotablesTest FABL.maxE3SatSignPredicates
    (7 / 8 + δ) 1
    (FABL.oxrE3SatReplacementError
      (FABL.hastadThreeSatOXRError (FABL.hastadThreeSatDegree δ hδ)))
    (FABL.hastadThreeSatTesterFamily δ hδ)
    theorem FABL.hastadThreeSat_dictatorVsNoNotables
  (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 (1 / 8)) :
  FABL.IsDictatorVsNoNotablesTest
    FABL.maxE3SatSignPredicates
    (7 / 8 + δ) 1
    (FABL.oxrE3SatReplacementError
      (FABL.hastadThreeSatOXRError
        (FABL.hastadThreeSatDegree δ hδ)))
    (FABL.hastadThreeSatTesterFamily δ hδ)
    O'Donnell, Theorem 7.41: for every `0 < δ < 1/8`, there is a
`(7/8+δ,1)` Dictator-vs.-No-Notables test using only three-literal OR predicates.
Theorem7.4.10
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Definition 7.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Corollary 7.4.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4fidelity-exact

Theorem 7.42. For every 0<\delta<1/2, there is a (1/2,1-\delta) Dictator-vs.-No-Notables test whose predicates are three-variable linear equations over \mathbb F_2.

Lean code for Theorem7.4.10●2 declarations
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.hastadDictatorTestFamily (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 (1 / 2))
  (n : ℕ) (_hn : 0 < n) : FABL.SignTester n
    def FABL.hastadDictatorTestFamily (δ : ℝ)
  (hδ : δ ∈ Set.Ioo 0 (1 / 2)) (n : ℕ)
  (_hn : 0 < n) : FABL.SignTester n
    The family of Håstad tests used in Theorem 7.42; the test noise is twice the theorem's
completeness-loss parameter.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastad_dictatorVsNoNotables (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 (1 / 2)) :
  FABL.IsDictatorVsNoNotablesTest FABL.maxE3LinPredicates (1 / 2)
    (1 - δ) (FABL.hastadSoundnessError (2 * δ))
    (FABL.hastadDictatorTestFamily δ hδ)
    theorem FABL.hastad_dictatorVsNoNotables (δ : ℝ)
  (hδ : δ ∈ Set.Ioo 0 (1 / 2)) :
  FABL.IsDictatorVsNoNotablesTest
    FABL.maxE3LinPredicates (1 / 2)
    (1 - δ)
    (FABL.hastadSoundnessError (2 * δ))
    (FABL.hastadDictatorTestFamily δ hδ)
    O'Donnell, Theorem 7.42: the noisy Håstad family is a
`(1/2, 1-δ)` Dictator-vs.-No-Notables test using Max-E3-Lin predicates.
Corollary7.4.11
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 7.4.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-7-4complexity-boundaryfidelity-partial-explicit-machine-and-refinement-witnesses

Corollary 7.43. For every \delta>0, an (7/8+\delta,1-\delta)-approximation for Max-E3-Sat is UG-hard.

The compiled endpoint specializes the proved long-code reduction and is conditional on the same explicit gap, refinement, codec, runtime, and numerical-budget witnesses recorded at Theorem 7.40.

Lean code for Corollary7.4.11●1 theorem
  • theoremdefined in FABL/Chapter07/UniqueGamesReduction.lean
    complete
    theorem FABL.maxE3Sat_conditional_uniqueGames_hardness.{u_1, u_2} {q : ℕ}
  [Nonempty (Fin q)] {source : FABL.BinaryPromiseProblem}
  (family : FABL.EncodedRegularUniqueGamesFamily q)
  (encoding : family.OptimizationEncoding) (δ : ℝ)
  (hδ : δ ∈ Set.Ioo 0 (1 / 8)) (hq : 0 < q)
  (UG : family.GapHypothesis source encoding)
  (transform : family.LongCodeFiniteTransform ⋯)
  (codec : family.LongCodeOutputCodec transform)
  (machine : family.LongCodeTransformMachine codec) (δUG ε τ : ℝ)
  (hε : ε ∈ Set.Ioc 0 1) (hgap : 7 / 8 + δ < 1 - δ)
  (hugCompleteness : 1 - δUG ≤ UG.completeness)
  (hugSoundness : UG.soundness < τ * ε ^ 5 / 18)
  (hcompleteness :
    1 - δ ≤ 1 - ↑transform.r * δUG - ↑transform.r ^ 2 / ↑transform.M)
  (hsoundness :
    7 / 8 + δ / 2 +
            FABL.oxrE3SatReplacementError
              (FABL.hastadThreeSatOXRError
                (FABL.hastadThreeSatDegree (δ / 2) ⋯))
              ε +
          τ +
        ↑transform.r ^ 2 / ↑transform.M ≤
      7 / 8 + δ) :
  FABL.PromiseKarpReducible source
    (codec.target.gapPromiseReal (7 / 8 + δ) (1 - δ) hgap)
    theorem FABL.maxE3Sat_conditional_uniqueGames_hardness.{u_1,
    u_2}
  {q : ℕ} [Nonempty (Fin q)]
  {source : FABL.BinaryPromiseProblem}
  (family :
    FABL.EncodedRegularUniqueGamesFamily
      q)
  (encoding : family.OptimizationEncoding)
  (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 (1 / 8))
  (hq : 0 < q)
  (UG :
    family.GapHypothesis source encoding)
  (transform :
    family.LongCodeFiniteTransform ⋯)
  (codec :
    family.LongCodeOutputCodec transform)
  (machine :
    family.LongCodeTransformMachine codec)
  (δUG ε τ : ℝ) (hε : ε ∈ Set.Ioc 0 1)
  (hgap : 7 / 8 + δ < 1 - δ)
  (hugCompleteness :
    1 - δUG ≤ UG.completeness)
  (hugSoundness :
    UG.soundness < τ * ε ^ 5 / 18)
  (hcompleteness :
    1 - δ ≤
      1 - ↑transform.r * δUG -
        ↑transform.r ^ 2 / ↑transform.M)
  (hsoundness :
    7 / 8 + δ / 2 +
            FABL.oxrE3SatReplacementError
              (FABL.hastadThreeSatOXRError
                (FABL.hastadThreeSatDegree
                  (δ / 2) ⋯))
              ε +
          τ +
        ↑transform.r ^ 2 / ↑transform.M ≤
      7 / 8 + δ) :
  FABL.PromiseKarpReducible source
    (codec.target.gapPromiseReal
      (7 / 8 + δ) (1 - δ) hgap)
    Corollary 7.43, conditional on the explicit regular-UG gap, uniform refinement, codecs, and
polynomial-time implementation witnesses.
Corollary7.4.12
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 7.4.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-7-4complexity-boundaryfidelity-partial-explicit-machine-and-refinement-witnesses

Corollary 7.44. For every \delta>0, an (1/2+\delta,1-\delta)-approximation for Max-E3-Lin is UG-hard.

The compiled endpoint specializes the proved long-code reduction and is conditional on the same explicit gap, refinement, codec, runtime, and numerical-budget witnesses recorded at Theorem 7.40.

Lean code for Corollary7.4.12●1 theorem
  • theoremdefined in FABL/Chapter07/UniqueGamesReduction.lean
    complete
    theorem FABL.maxE3Lin_conditional_uniqueGames_hardness.{u_1, u_2} {q : ℕ}
  [Nonempty (Fin q)] {source : FABL.BinaryPromiseProblem}
  (family : FABL.EncodedRegularUniqueGamesFamily q)
  (encoding : family.OptimizationEncoding) (δ : ℝ)
  (hδ : δ ∈ Set.Ioo 0 (1 / 2)) (hq : 0 < q)
  (UG : family.GapHypothesis source encoding)
  (transform : family.LongCodeFiniteTransform ⋯)
  (codec : family.LongCodeOutputCodec transform)
  (machine : family.LongCodeTransformMachine codec) (δUG ε τ : ℝ)
  (hε : ε ∈ Set.Ioc 0 1) (hgap : 1 / 2 + δ < 1 - δ)
  (hugCompleteness : 1 - δUG ≤ UG.completeness)
  (hugSoundness : UG.soundness < τ * ε ^ 5 / 18)
  (hcompleteness :
    1 - δ ≤
      1 - δ / 2 - ↑transform.r * δUG - ↑transform.r ^ 2 / ↑transform.M)
  (hsoundness :
    1 / 2 + FABL.hastadSoundnessError δ ε + τ +
        ↑transform.r ^ 2 / ↑transform.M ≤
      1 / 2 + δ) :
  FABL.PromiseKarpReducible source
    (codec.target.gapPromiseReal (1 / 2 + δ) (1 - δ) hgap)
    theorem FABL.maxE3Lin_conditional_uniqueGames_hardness.{u_1,
    u_2}
  {q : ℕ} [Nonempty (Fin q)]
  {source : FABL.BinaryPromiseProblem}
  (family :
    FABL.EncodedRegularUniqueGamesFamily
      q)
  (encoding : family.OptimizationEncoding)
  (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 (1 / 2))
  (hq : 0 < q)
  (UG :
    family.GapHypothesis source encoding)
  (transform :
    family.LongCodeFiniteTransform ⋯)
  (codec :
    family.LongCodeOutputCodec transform)
  (machine :
    family.LongCodeTransformMachine codec)
  (δUG ε τ : ℝ) (hε : ε ∈ Set.Ioc 0 1)
  (hgap : 1 / 2 + δ < 1 - δ)
  (hugCompleteness :
    1 - δUG ≤ UG.completeness)
  (hugSoundness :
    UG.soundness < τ * ε ^ 5 / 18)
  (hcompleteness :
    1 - δ ≤
      1 - δ / 2 - ↑transform.r * δUG -
        ↑transform.r ^ 2 / ↑transform.M)
  (hsoundness :
    1 / 2 +
            FABL.hastadSoundnessError δ
              ε +
          τ +
        ↑transform.r ^ 2 / ↑transform.M ≤
      1 / 2 + δ) :
  FABL.PromiseKarpReducible source
    (codec.target.gapPromiseReal
      (1 / 2 + δ) (1 - δ) hgap)
    Corollary 7.44, conditional on the explicit regular-UG gap, uniform refinement, codecs, and
polynomial-time implementation witnesses.
Lemma7.4.13
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 7.4.10
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-7-4fidelity-exact

Remark 7.45. The completeness 1-\delta in the Max-E3-Lin test of Theorem 7.42 cannot be replaced by 1: no (\alpha,1) Dictator-vs.-No-Notables test using only Max-E3-Lin predicates exists for \alpha<1.

Lean code for Lemma7.4.13●1 theorem
  • theoremdefined in FABL/Chapter07/HastadLimitations.lean
    complete
    theorem FABL.e3LinTester_accepts_oddParity_of_accepts_dictators (k : ℕ)
  (T : FABL.SignTester (2 * k + 1))
  (huses : T.UsesPredicates FABL.maxE3LinPredicates)
  (hcomplete :
    ∀ (i : Fin (2 * k + 1)),
      T.acceptanceProbability
          (FABL.BoundedCubeFunction.ofBoolean (FABL.dictator i)) =
        1) :
  T.acceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        (FABL.parityFunction Finset.univ)) =
    1
    theorem FABL.e3LinTester_accepts_oddParity_of_accepts_dictators
  (k : ℕ)
  (T : FABL.SignTester (2 * k + 1))
  (huses :
    T.UsesPredicates
      FABL.maxE3LinPredicates)
  (hcomplete :
    ∀ (i : Fin (2 * k + 1)),
      T.acceptanceProbability
          (FABL.BoundedCubeFunction.ofBoolean
            (FABL.dictator i)) =
        1) :
  T.acceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        (FABL.parityFunction
          Finset.univ)) =
    1
    A perfect-completeness E3-Lin tester accepts every parity of odd cardinality.
Definition7.4.14
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 7.4.15
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4fidelity-exact

The Odd BLR Test for f:\mathbb F_2^n\to\mathbb F_2 independently samples uniform x,y, samples uniform b\in\mathbb F_2, sets z=x+y+(b,\ldots,b), and accepts exactly when f(x)+f(y)+f(z)=b.

Lean code for Definition7.4.14●2 definitions
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.oddBLRTester (n : ℕ) : FABL.SignTester n
    def FABL.oddBLRTester (n : ℕ) :
  FABL.SignTester n
    The Odd BLR Test is the zero-noise Håstad test.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.oddBLRAcceptanceProbability {n : ℕ}
  (f : FABL.BoundedCubeFunction n) : ℝ
    def FABL.oddBLRAcceptanceProbability {n : ℕ}
  (f : FABL.BoundedCubeFunction n) : ℝ
    Acceptance probability of the Odd BLR Test.
Proposition7.4.15
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-7-4erratumfidelity-corrected-false-book-claim

Proposition 7.46. The Odd BLR acceptance probability is \frac12+ \frac12\sum_{\substack{S\subseteq[n]\\|S|\text{ odd}}} \widehat f(S)^3.

The book additionally prints the upper bound \frac12+ \frac12\max_{\substack{S\subseteq[n]\\|S|\text{ odd}}}\widehat f(S), but this is false without a nonnegativity guard. For n=2, take f(1,1)=-1 and f=1 on the other three inputs. Both odd Fourier coefficients are -1/2, so the acceptance probability is 3/8 while the printed upper bound is 1/4.

The production theorem proves the minimal valid correction \Pr[\text{Odd BLR accepts }f] \le \frac12+ \frac12\max\!\left( 0, \max_{\substack{S\subseteq[n]\\|S|\text{ odd}}}\widehat f(S) \right), with the maximum over an empty odd-frequency set interpreted as 0.

Lean code for Proposition7.4.15●14 declarations
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.oddFourierFrequencies (n : ℕ) : Finset (Finset (Fin n))
    def FABL.oddFourierFrequencies (n : ℕ) :
  Finset (Finset (Fin n))
    Odd Fourier frequencies occurring in the Odd BLR formula.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.oddFourierFrequencies_nonempty (n : ℕ) (hn : 0 < n) :
  (FABL.oddFourierFrequencies n).Nonempty
    theorem FABL.oddFourierFrequencies_nonempty
  (n : ℕ) (hn : 0 < n) :
  (FABL.oddFourierFrequencies n).Nonempty
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.oddFourierMaximum {n : ℕ} (hn : 0 < n)
  (f : FABL.BooleanFunction n) : ℝ
    def FABL.oddFourierMaximum {n : ℕ}
  (hn : 0 < n)
  (f : FABL.BooleanFunction n) : ℝ
    The maximum odd Fourier coefficient appearing in the printed Proposition 7.46.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.nonnegativeOddFourierMaximum {n : ℕ} (f : FABL.BooleanFunction n) :
  ℝ
    def FABL.nonnegativeOddFourierMaximum {n : ℕ}
  (f : FABL.BooleanFunction n) : ℝ
    Corrected maximum for Proposition 7.46: the maximum of zero and all odd coefficients.

The inserted zero makes the empty-dimensional endpoint explicit and repairs the false printed
inequality when every odd coefficient is negative.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.nonnegativeOddFourierMaximum_eq_max {n : ℕ} (hn : 0 < n)
  (f : FABL.BooleanFunction n) :
  FABL.nonnegativeOddFourierMaximum f =
    max 0 (FABL.oddFourierMaximum hn f)
    theorem FABL.nonnegativeOddFourierMaximum_eq_max
  {n : ℕ} (hn : 0 < n)
  (f : FABL.BooleanFunction n) :
  FABL.nonnegativeOddFourierMaximum f =
    max 0 (FABL.oddFourierMaximum hn f)
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.nonnegativeOddFourierMaximum_dimension_zero
  (f : FABL.BooleanFunction 0) : FABL.nonnegativeOddFourierMaximum f = 0
    theorem FABL.nonnegativeOddFourierMaximum_dimension_zero
  (f : FABL.BooleanFunction 0) :
  FABL.nonnegativeOddFourierMaximum f = 0
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.oddBLRAcceptanceProbability_eq_fourierSum {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean f) =
    1 / 2 +
      1 / 2 * ∑ S with Odd S.card, FABL.fourierCoeff f.toReal S ^ 3
    theorem FABL.oddBLRAcceptanceProbability_eq_fourierSum
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        f) =
    1 / 2 +
      1 / 2 *
        ∑ S with Odd S.card,
          FABL.fourierCoeff f.toReal S ^ 3
    The equality in O'Donnell, Proposition 7.46.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.oddBLRAcceptanceProbability_le_correctedMaximum {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean f) ≤
    1 / 2 + 1 / 2 * FABL.nonnegativeOddFourierMaximum f
    theorem FABL.oddBLRAcceptanceProbability_le_correctedMaximum
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        f) ≤
    1 / 2 +
      1 / 2 *
        FABL.nonnegativeOddFourierMaximum
          f
    Corrected inequality accompanying Proposition 7.46.

The book's printed right-hand side omits `max 0`; that claim is false already in dimension two.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.oddBLRBookBoundCounterexample : FABL.BooleanFunction 2
    def FABL.oddBLRBookBoundCounterexample :
  FABL.BooleanFunction 2
    The two-variable Boolean function which is `-1` only at the all-`+1` input.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.fourierCoeff_oddBLRBookBoundCounterexample_zero :
  FABL.fourierCoeff FABL.oddBLRBookBoundCounterexample.toReal {0} =
    -1 / 2
    theorem FABL.fourierCoeff_oddBLRBookBoundCounterexample_zero :
  FABL.fourierCoeff
      FABL.oddBLRBookBoundCounterexample.toReal
      {0} =
    -1 / 2
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.fourierCoeff_oddBLRBookBoundCounterexample_one :
  FABL.fourierCoeff FABL.oddBLRBookBoundCounterexample.toReal {1} =
    -1 / 2
    theorem FABL.fourierCoeff_oddBLRBookBoundCounterexample_one :
  FABL.fourierCoeff
      FABL.oddBLRBookBoundCounterexample.toReal
      {1} =
    -1 / 2
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.oddBLRBookBoundCounterexample_acceptance :
  FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        FABL.oddBLRBookBoundCounterexample) =
    3 / 8
    theorem FABL.oddBLRBookBoundCounterexample_acceptance :
  FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        FABL.oddBLRBookBoundCounterexample) =
    3 / 8
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.oddBLRBookBoundCounterexample_printed_rhs :
  1 / 2 +
      1 / 2 *
        FABL.oddFourierMaximum
          FABL.oddBLRBookBoundCounterexample_oddMaximum._proof_1
          FABL.oddBLRBookBoundCounterexample =
    1 / 4
    theorem FABL.oddBLRBookBoundCounterexample_printed_rhs :
  1 / 2 +
      1 / 2 *
        FABL.oddFourierMaximum
          FABL.oddBLRBookBoundCounterexample_oddMaximum._proof_1
          FABL.oddBLRBookBoundCounterexample =
    1 / 4
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.oddBLRBookBoundCounterexample_refutes_printed_inequality :
  1 / 2 +
      1 / 2 *
        FABL.oddFourierMaximum
          FABL.oddBLRBookBoundCounterexample_oddMaximum._proof_1
          FABL.oddBLRBookBoundCounterexample <
    FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        FABL.oddBLRBookBoundCounterexample)
    theorem FABL.oddBLRBookBoundCounterexample_refutes_printed_inequality :
  1 / 2 +
      1 / 2 *
        FABL.oddFourierMaximum
          FABL.oddBLRBookBoundCounterexample_oddMaximum._proof_1
          FABL.oddBLRBookBoundCounterexample <
    FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        FABL.oddBLRBookBoundCounterexample)
    Strict counterexample to the uncorrected inequality printed in Proposition 7.46.
Definition7.4.16
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 2.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 7.4.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4fidelity-exact

For 0<\delta<1, the Håstad_\delta Test independently samples uniform x,y\in\{-1,1\}^n and uniform b\in\{-1,1\}, sets z=b(x\circ y), samples z' from the noise distribution N_{1-\delta}(z), and accepts exactly when f(x)f(y)f(z')=b. For f valued in [-1,1], the three queried answers are independent random signs with the corresponding means.

Lean code for Definition7.4.16●10 declarations
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.e3LinPredicate (b : FABL.Sign) : FABL.SignPredicate
    def FABL.e3LinPredicate (b : FABL.Sign) :
  FABL.SignPredicate
    The two Max-E3-Lin predicates, expressed in sign notation.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.e3LinPredicate_indicator_eq (b : FABL.Sign)
  (y : Fin 3 → FABL.Sign) :
  (if (FABL.e3LinPredicate b).accepts y = true then 1 else 0) =
    (1 + FABL.signValue b * ∏ i, FABL.signValue (y i)) / 2
    theorem FABL.e3LinPredicate_indicator_eq
  (b : FABL.Sign)
  (y : Fin 3 → FABL.Sign) :
  (if
        (FABL.e3LinPredicate b).accepts
            y =
          true then
      1
    else 0) =
    (1 +
        FABL.signValue b *
          ∏ i, FABL.signValue (y i)) /
      2
    The indicator of a three-variable sign equation is its affine character expansion.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.e3LinPredicate_randomizedValue (b : FABL.Sign) (μ : Fin 3 → ℝ)
  (hμ : ∀ (i : Fin 3), μ i ∈ Set.Icc (-1) 1) :
  (FABL.e3LinPredicate b).randomizedValue μ hμ =
    (1 + FABL.signValue b * μ 0 * μ 1 * μ 2) / 2
    theorem FABL.e3LinPredicate_randomizedValue
  (b : FABL.Sign) (μ : Fin 3 → ℝ)
  (hμ :
    ∀ (i : Fin 3), μ i ∈ Set.Icc (-1) 1) :
  (FABL.e3LinPredicate b).randomizedValue
      μ hμ =
    (1 +
        FABL.signValue b * μ 0 * μ 1 *
          μ 2) /
      2
    Multilinear value of a Max-E3-Lin predicate under independent randomized signs.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.maxE3LinPredicates : Set FABL.SignPredicate
    def FABL.maxE3LinPredicates :
  Set FABL.SignPredicate
    Predicate set of three-variable binary linear equations.
  • structure(4 fields)defined in FABL/Chapter07/HastadTests.lean
    complete
    structure FABL.HastadSeed (n : ℕ) : Type
    structure FABL.HastadSeed (n : ℕ) : Type
    One random outcome of the noisy Håstad test.

    Fields

    x : FABL.SignCube n
    First uniform query. 
    y : FABL.SignCube n
    Second uniform query. 
    rhs : FABL.Sign
    Random equation right-hand side. 
    noisyProduct : FABL.SignCube n
    Noisy version of `rhs · (x ∘ y)`.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.hastadSeedPMF {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1) :
  PMF (FABL.HastadSeed n)
    def FABL.hastadSeedPMF {n : ℕ} (δ : ℝ)
  (hδ : δ ∈ Set.Icc 0 1) :
  PMF (FABL.HastadSeed n)
    Random-seed law of the `δ`-noisy Håstad test.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.hastadTester (n : ℕ) (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1) :
  FABL.SignTester n
    def FABL.hastadTester (n : ℕ) (δ : ℝ)
  (hδ : δ ∈ Set.Icc 0 1) :
  FABL.SignTester n
    The three-query `δ`-noisy Håstad test.
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.hastadAcceptanceProbability {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BoundedCubeFunction n) : ℝ
    def FABL.hastadAcceptanceProbability {n : ℕ}
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BoundedCubeFunction n) : ℝ
    Acceptance probability of the noisy Håstad test under the amended real-valued semantics.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastadAcceptanceProbability_eq_expect {n : ℕ} (δ : ℝ)
  (hδ : δ ∈ Set.Icc 0 1) (f : FABL.BoundedCubeFunction n) :
  FABL.hastadAcceptanceProbability δ hδ f =
    Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        Finset.univ.expect fun b =>
          (1 +
              FABL.signValue b * f.toFun x * f.toFun y *
                (FABL.noiseOperator (1 - δ)) f.toFun
                  (FABL.scaledPointwiseProduct b x y)) /
            2
    theorem FABL.hastadAcceptanceProbability_eq_expect
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BoundedCubeFunction n) :
  FABL.hastadAcceptanceProbability δ hδ
      f =
    Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        Finset.univ.expect fun b =>
          (1 +
              FABL.signValue b *
                    f.toFun x *
                  f.toFun y *
                (FABL.noiseOperator
                    (1 - δ))
                  f.toFun
                  (FABL.scaledPointwiseProduct
                    b x y)) /
            2
    The operational tester semantics is the expected multilinear E3-Lin value.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastadAcceptanceProbability_dictator {n : ℕ} (δ : ℝ)
  (hδ : δ ∈ Set.Icc 0 1) (i : Fin n) :
  FABL.hastadAcceptanceProbability δ hδ
      (FABL.BoundedCubeFunction.ofBoolean (FABL.dictator i)) =
    1 - δ / 2
    theorem FABL.hastadAcceptanceProbability_dictator
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (i : Fin n) :
  FABL.hastadAcceptanceProbability δ hδ
      (FABL.BoundedCubeFunction.ofBoolean
        (FABL.dictator i)) =
    1 - δ / 2
    A dictator passes the `δ`-noisy Håstad test with probability `1 - δ / 2`.
Lemma7.4.17
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Proposition 1.5.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 7.4.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-7-4supportfidelity-exact

Equation (7.4). For every f:\{-1,1\}^n\to[-1,1], \Pr[\operatorname{Håstad}_\delta\text{ accepts }f] =\frac12+ \frac12\sum_{\substack{S\subseteq[n]\\|S|\text{ odd}}} (1-\delta)^{|S|}\widehat f(S)^3. \tag{7.4}

Lean code for Lemma7.4.17●4 declarations
  • defdefined in FABL/Chapter07/HastadTests.lean
    complete
    def FABL.scaledPointwiseProduct {n : ℕ} (b : FABL.Sign)
  (x y : FABL.SignCube n) : FABL.SignCube n
    def FABL.scaledPointwiseProduct {n : ℕ}
  (b : FABL.Sign)
  (x y : FABL.SignCube n) :
  FABL.SignCube n
    Coordinatewise product, followed by a global sign.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.monomial_scaledPointwiseProduct {n : ℕ} (b : FABL.Sign)
  (x y : FABL.SignCube n) (S : Finset (Fin n)) :
  FABL.monomial S (FABL.scaledPointwiseProduct b x y) =
    FABL.signValue b ^ S.card * FABL.monomial S x * FABL.monomial S y
    theorem FABL.monomial_scaledPointwiseProduct
  {n : ℕ} (b : FABL.Sign)
  (x y : FABL.SignCube n)
  (S : Finset (Fin n)) :
  FABL.monomial S
      (FABL.scaledPointwiseProduct b x
        y) =
    FABL.signValue b ^ S.card *
        FABL.monomial S x *
      FABL.monomial S y
    Walsh monomials turn a globally signed pointwise product into an ordinary product.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.expect_hastadCore_eq_fourierSum {n : ℕ} (ρ : ℝ)
  (f : FABL.SignCube n → ℝ) (b : FABL.Sign) :
  (Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        f x * f y *
          (FABL.noiseOperator ρ) f
            (FABL.scaledPointwiseProduct b x y)) =
    ∑ S,
      FABL.signValue b ^ S.card * ρ ^ S.card * FABL.fourierCoeff f S ^ 3
    theorem FABL.expect_hastadCore_eq_fourierSum
  {n : ℕ} (ρ : ℝ)
  (f : FABL.SignCube n → ℝ)
  (b : FABL.Sign) :
  (Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        f x * f y *
          (FABL.noiseOperator ρ) f
            (FABL.scaledPointwiseProduct b
              x y)) =
    ∑ S,
      FABL.signValue b ^ S.card *
          ρ ^ S.card *
        FABL.fourierCoeff f S ^ 3
    Core Fourier calculation for the two uniform queries and the noisy product query.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastadAcceptanceProbability_eq_fourierSum {n : ℕ} (δ : ℝ)
  (hδ : δ ∈ Set.Icc 0 1) (f : FABL.BoundedCubeFunction n) :
  FABL.hastadAcceptanceProbability δ hδ f =
    1 / 2 +
      1 / 2 *
        ∑ S with Odd S.card,
          (1 - δ) ^ S.card * FABL.fourierCoeff f.toFun S ^ 3
    theorem FABL.hastadAcceptanceProbability_eq_fourierSum
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BoundedCubeFunction n) :
  FABL.hastadAcceptanceProbability δ hδ
      f =
    1 / 2 +
      1 / 2 *
        ∑ S with Odd S.card,
          (1 - δ) ^ S.card *
            FABL.fourierCoeff f.toFun S ^
              3
    O'Donnell, equation (7.4): exact Fourier acceptance formula for the Håstad test.
Lemma7.4.18
Group: Chapter 7: Property testing, PCPPs, and CSPs (103)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-7-4supportfidelity-exact

Equations (7.5)--(7.6). Suppose 0\le\epsilon\le\delta and \operatorname{Inf}^{(1-\epsilon)}_i[f] =\sum_{S\ni i}(1-\epsilon)^{|S|-1}\widehat f(S)^2 \le\epsilon \quad\text{for every }i. \tag{7.5} Then \Pr[\operatorname{Håstad}_\delta\text{ accepts }f] \le\frac12+\frac12\sqrt\epsilon. \tag{7.6} Thus one may take \lambda(\epsilon)= \begin{cases} \tfrac12\sqrt\epsilon,&\epsilon\le\delta,\\ \tfrac12,&\epsilon>\delta. \end{cases}

Lean code for Lemma7.4.18●3 theorems
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hasSmallStableInfluences_iff_equation_7_5 {n : ℕ} (ε : ℝ)
  (f : FABL.BoundedCubeFunction n) :
  FABL.HasSmallStableInfluences ε ε f.toFun ↔
    ∀ (i : Fin n),
      ∑ S with i ∈ S,
          (1 - ε) ^ (S.card - 1) * FABL.fourierCoeff f.toFun S ^ 2 ≤
        ε
    theorem FABL.hasSmallStableInfluences_iff_equation_7_5
  {n : ℕ} (ε : ℝ)
  (f : FABL.BoundedCubeFunction n) :
  FABL.HasSmallStableInfluences ε ε
      f.toFun ↔
    ∀ (i : Fin n),
      ∑ S with i ∈ S,
          (1 - ε) ^ (S.card - 1) *
            FABL.fourierCoeff f.toFun S ^
              2 ≤
        ε
    O'Donnell, equation (7.5), exposed through the Chapter 6 stable-influence predicate.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.BoundedCubeFunction.sum_sq_fourierCoeff_le_one {n : ℕ}
  (f : FABL.BoundedCubeFunction n) :
  ∑ S, FABL.fourierCoeff f.toFun S ^ 2 ≤ 1
    theorem FABL.BoundedCubeFunction.sum_sq_fourierCoeff_le_one
  {n : ℕ}
  (f : FABL.BoundedCubeFunction n) :
  ∑ S, FABL.fourierCoeff f.toFun S ^ 2 ≤ 1
    Parseval mass of a function bounded pointwise by one is at most one.
  • theoremdefined in FABL/Chapter07/HastadTests.lean
    complete
    theorem FABL.hastadAcceptanceProbability_le_half_add_half_sqrt {n : ℕ} (δ ε : ℝ)
  (hδ : δ ∈ Set.Icc 0 1) (hε : ε ∈ Set.Icc 0 1) (hεδ : ε ≤ δ)
  (f : FABL.BoundedCubeFunction n)
  (hsmall : FABL.HasSmallStableInfluences ε ε f.toFun) :
  FABL.hastadAcceptanceProbability δ hδ f ≤ 1 / 2 + 1 / 2 * √ε
    theorem FABL.hastadAcceptanceProbability_le_half_add_half_sqrt
  {n : ℕ} (δ ε : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (hε : ε ∈ Set.Icc 0 1) (hεδ : ε ≤ δ)
  (f : FABL.BoundedCubeFunction n)
  (hsmall :
    FABL.HasSmallStableInfluences ε ε
      f.toFun) :
  FABL.hastadAcceptanceProbability δ hδ
      f ≤
    1 / 2 + 1 / 2 * √ε
    O'Donnell, equation (7.6): Håstad soundness under small stable influences.