OAI/NumberTheory/TwoPoint/Circuits/CircuitPolynomialMean.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The polynomial-expectation step in Braverman's proof (Proposition 6, author version https://www.cs.toronto.edu/~mbraverm/FoolAC0v7.pdf). On the Boolean cube, multilinear degree is represented by Walsh support. Preservation of low-degree expectations gives a sandwich criterion for bounded-independence comparison.

  1. def OAI.TwoPointCorrelations.cubeRestrict line 18
  2. def OAI.TwoPointCorrelations.cubeExtend line 20
  3. lemma OAI.TwoPointCorrelations.cubePattern_extend line 23
  4. lemma OAI.TwoPointCorrelations.cube_function_partition line 35
  5. lemma OAI.TwoPointCorrelations.TWiseUniformDensity.restricted_mean line 41
  6. lemma OAI.TwoPointCorrelations.uniformDensity_tWise line 57
  7. lemma OAI.TwoPointCorrelations.TWiseUniformDensity.restricted_expectation line 62
  8. lemma OAI.TwoPointCorrelations.TWiseUniformDensity.walsh_expectation line 70
  9. def OAI.TwoPointCorrelations.WalshDegreeLE line 83

    Source documentation

    A concrete finite representation of a real multilinear polynomial of degree at most t, restricted to the Boolean cube.

    def WalshDegreeLE (F : BooleanCube n → ℝ) (t : ℕ) : Prop :=
…

    Mentions: OAI.TwoPointCorrelations.BooleanCube

  10. lemma OAI.TwoPointCorrelations.TWiseUniformDensity.polynomial_expectation line 88
  11. theorem OAI.TwoPointCorrelations.TWiseUniformDensity.sandwich_error line 107

    Source documentation

    Two low-degree pointwise bounds with small uniform gap also bound every t-wise independent law. This criterion supplies the finite probability interface for the analytic polynomial construction.

    theorem TWiseUniformDensity.sandwich_error {t : ℕ} {g F P Q : BooleanCube n → ℝ}
    (hg : TWiseUniformDensity g t) (hn : ∀ x, 0 ≤ g x)
    (hP : WalshDegreeLE P t) (hQ : WalshDegreeLE Q t)
    (hPF : ∀ x, P x ≤ F x) (hFQ : ∀ x, F x ≤ Q x)
    {ε : ℝ} (hgap : cubeAverage (fun x => Q x - P x) ≤ ε) :
    |cubeAverage (fun x => g x * F x) - cubeAverage F| ≤ ε := by
…

    Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.TWiseUniformDensity, OAI.TwoPointCorrelations.WalshDegreeLE, OAI.TwoPointCorrelations.cubeAverage