CircuitComparison.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded-independence circuit comparison after Fourier correction

The comparison uses the fixed-depth specialization of Mark Braverman, Polylogarithmic independence fools AC⁰ circuits, J. ACM 57 (2010), Article 28, Corollary 2 in the author's version. We use depth 22, with absolute constants and natural logarithms. Circuits below have actual finite syntax: literals and arbitrary finite-fan-in AND/OR gates. They are tree circuits, a subclass of the circuits covered by Braverman's theorem. The size counts both input occurrences and gates; the depth counts AND/OR levels.

inductive OAI.TwoPointCorrelations.AC0Circuit line 23
Source documentation
Finite AC⁰ syntax in negation normal form. Sharing is not needed for the finite residue tests; literals can have either polarity.
```
inductive AC0Circuit (n : ℕ) where
…
```

def OAI.TwoPointCorrelations.AC0Circuit.eval line 31

Source documentation

Evaluation on a Boolean input vector. Empty AND/OR gates are true/false.

def eval {n : ℕ} : AC0Circuit n → BooleanCube n → Bool
  | .literal i positive, x => if positive then x i else !(x i)
  | .andGate children, x => decide (∀ i, eval (children i) x = true)
  | .orGate children, x => decide (∃ i, eval (children i) x = true)

/-- AND/OR depth, with literals at depth zero. -/

Mentions: OAI.TwoPointCorrelations.AC0Circuit, OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.AC0Circuit.depth

def OAI.TwoPointCorrelations.AC0Circuit.depth line 37

Source documentation

AND/OR depth, with literals at depth zero.

def depth {n : ℕ} : AC0Circuit n → ℕ
  | .literal _ _ => 0
  | .andGate children => 1 + Finset.univ.sup (fun i => depth (children i))
  | .orGate children => 1 + Finset.univ.sup (fun i => depth (children i))

/-- Gates plus input occurrences. -/

Mentions: OAI.TwoPointCorrelations.AC0Circuit

def OAI.TwoPointCorrelations.AC0Circuit.size line 43

Source documentation

Gates plus input occurrences.

def size {n : ℕ} : AC0Circuit n → ℕ
  | .literal _ _ => 1
  | .andGate children => 1 + ∑ i, size (children i)
  | .orGate children => 1 + ∑ i, size (children i)

Mentions: OAI.TwoPointCorrelations.AC0Circuit

lemma OAI.TwoPointCorrelations.AC0Circuit.size_pos line 48
def OAI.TwoPointCorrelations.AC0Circuit.indicator line 52
Source documentation
Real indicator of the circuit accepting its input.
```
noncomputable def indicator {n : ℕ} (c : AC0Circuit n) (x : BooleanCube n) : ℝ :=
…
```
Mentions: OAI.TwoPointCorrelations.AC0Circuit, OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.AC0Circuit.abs_centered_indicator line 55
def OAI.TwoPointCorrelations.BravermanDepth22Input line 65
Source documentation
Braverman's Corollary 2 at depth twenty-two. The constants absorb a choice of logarithm base. Distributions are represented by nonnegative densities relative to the uniform law on the Boolean cube.
```
def BravermanDepth22Input : Prop :=
…
```
lemma OAI.TwoPointCorrelations.abs_cubeAverage_le line 73
lemma OAI.TwoPointCorrelations.circuit_event_le_totalVariation line 82
Source documentation
For measures of equal total mass, an event difference is bounded by one half of the mean absolute density difference.
```
lemma circuit_event_le_totalVariation {n : ℕ} (c : AC0Circuit n)
    (f g : BooleanCube n → ℝ) (hmass : cubeAverage f = cubeAverage g) :
    |cubeAverage (fun x => f x * c.indicator x) -
      cubeAverage (fun x => g x * c.indicator x)| ≤
        cubeAverage (fun x => |f x - g x|) / 2 := by
…
```
Mentions: OAI.TwoPointCorrelations.AC0Circuit, OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubeAverage

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.fourier_comparison line 112

Source documentation

Fourier correction followed by Braverman's published theorem compares the original density against uniform inputs, with the correction error made explicit.

theorem BravermanDepth22Input.fourier_comparison (hBraverman : BravermanDepth22Input) :
    ∃ K C : ℕ, 0 < K ∧ 0 < C ∧ ∀ (n : ℕ) (c : AC0Circuit n), c.depth ≤ 22 →
      ∀ ε : ℝ, 0 < ε → ε ≤ 1 / 2 → ∀ t : ℕ,
        (K : ℝ) * (Real.log ((c.size : ℝ) / ε)) ^ C ≤ (t : ℝ) →
        ∀ (f : BooleanCube n → ℝ) (a : ℝ),
          (∀ x, 0 ≤ f x) → cubeAverage f = 1 → 0 ≤ a → lowWalshMass f t ≤ a →
          |cubeAverage (fun x => f x * c.indicator x) - cubeAverage c.indicator| ≤
            3 * a / 2 + ε := by
…

Mentions: OAI.TwoPointCorrelations.BravermanDepth22Input, OAI.TwoPointCorrelations.AC0Circuit, OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.lowWalshMass