FiniteResidueComparison.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Finite residue-circuit comparison

An original residue circuit has depth at most twenty. Each input tests one residue coordinate, and is replaced by its explicit truth table on the corresponding bit block. The encoded circuit therefore has depth at most twenty-two. The empirical Fourier bound, the published Braverman input, and the two decoding errors give a completely finite error estimate.

lemma OAI.TwoPointCorrelations.abs_add_three line 19
def OAI.TwoPointCorrelations.residueCircuitInputs line 24
Source documentation
Inputs to an actual Boolean circuit, with each input depending on one specified residue coordinate. Equality with a fixed residue is a special case.
```
def residueCircuitInputs {n m : ℕ} (s : Fin m → ℕ) (coord : Fin n → Fin m)
    (test : ∀ i, ZMod (s (coord i)) → Bool) (r : ∀ j, ZMod (s j)) : BooleanCube n :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
def OAI.TwoPointCorrelations.residueCircuitEvent line 28

def OAI.TwoPointCorrelations.encodeResidueCircuit line 33

Source documentation

The actual truth-table circuit used for encoded residue testing.

noncomputable def encodeResidueCircuit {n m : ℕ} (s : Fin m → ℕ)
    [∀ i, NeZero (s i)] (B : ℕ) (coord : Fin n → Fin m)
    (test : ∀ i, ZMod (s (coord i)) → Bool) (c : AC0Circuit n) : AC0Circuit (m * B) :=
…

Mentions: OAI.TwoPointCorrelations.AC0Circuit

lemma OAI.TwoPointCorrelations.flattenBitBlocks_block line 40
lemma OAI.TwoPointCorrelations.encodeResidueCircuit_eval line 46
lemma OAI.TwoPointCorrelations.encodeResidueCircuit_indicator line 57
lemma OAI.TwoPointCorrelations.encodeResidueCircuit_depth line 65
lemma OAI.TwoPointCorrelations.encodeResidueCircuit_size line 71
lemma OAI.TwoPointCorrelations.encodeResidueCircuit_interval_average line 77
lemma OAI.TwoPointCorrelations.encodeResidueCircuit_uniform_average line 93

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.finite_residue_comparison line 117

Source documentation

Comparison for the original depth-twenty residue circuit. The arithmetic hypotheses are precisely positivity and pairwise coprimality of the moduli; no squarefreeness or bound on their total product is used. The low-order Fourier error and the decoding error are explicit finite quantities.

theorem BravermanDepth22Input.finite_residue_comparison (hBraverman : BravermanDepth22Input) :
    ∃ K C : ℕ, 0 < K ∧ 0 < C ∧ ∀ (m B : ℕ), 0 < m * B →
      ∀ (s : Fin m → ℕ) [∀ i, NeZero (s i)],
      Pairwise (fun i j => (s i).Coprime (s j)) →
      ∀ (n : ℕ) (coord : Fin n → Fin m)
        (test : ∀ i, ZMod (s (coord i)) → Bool) (c : AC0Circuit n), c.depth ≤ 20 →
      ∀ ε : ℝ, 0 < ε → ε ≤ 1 / 2 → ∀ t : ℕ,
        (K : ℝ) * (Real.log
          (((encodeResidueCircuit s B coord test c).size : ℝ) / ε)) ^ C ≤ (t : ℝ) →
        ∀ (a N : ℕ), 0 < N → ∀ M A : ℝ, 1 ≤ M → (∀ i, (s i : ℝ) ≤ M) →
          (M ^ t / (N : ℝ)) * ((t + 1 : ℕ) : ℝ) * ((m * B : ℕ) : ℝ) ^ t ≤ A →
          |uniformAverage (fun x : Fin N =>
…

Mentions: OAI.TwoPointCorrelations.BravermanDepth22Input, OAI.TwoPointCorrelations.AC0Circuit, OAI.TwoPointCorrelations.encodeResidueCircuit, OAI.TwoPointCorrelations.uniformAverage