CircuitSemiExact.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite algebraic steps of Braverman's Lemmas 11–12. A polynomial that vanishes off a Boolean event gives a pointwise minorant after applying p ↦ 1 - (1-p)^2; the uniform squared error is exactly the minorant gap. Only the approximation construction, not this expectation argument, needs the circuit-depth estimates.

def OAI.TwoPointCorrelations.semiExactMinorant line 15
lemma OAI.TwoPointCorrelations.semiExactMinorant_le line 18
lemma OAI.TwoPointCorrelations.semiExactMinorant_gap line 28
lemma OAI.TwoPointCorrelations.WalshDegreeLE.minorant line 37

theorem OAI.TwoPointCorrelations.TWiseUniformDensity.semiExact_lower line 47

Source documentation

A small exceptional set and a semi-exact low-degree approximation give the required one-sided comparison of the original Boolean expectation.

theorem TWiseUniformDensity.semiExact_lower {t : ℕ}
    {g F F₀ P : BooleanCube n → ℝ}
    (hg : TWiseUniformDensity g t) (hn : ∀ x, 0 ≤ g x)
    (hF₀ : ∀ x, F₀ x = 0 ∨ F₀ x = 1)
    (hzero : ∀ x, F₀ x = 0 → P x = 0)
    (hdeg : WalshDegreeLE (semiExactMinorant P) t)
    {δu δg ε : ℝ}
    (hu : cubeAverage (fun x => |F x - F₀ x|) ≤ δu)
    (hmu : cubeAverage (fun x => g x * |F x - F₀ x|) ≤ δg)
    (herr : cubeAverage (fun x => (F₀ x - P x) ^ 2) ≤ ε) :
    cubeAverage F - (δu + δg + ε) ≤ cubeAverage (fun x => g x * F x) := by
…

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