EventualResidueComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit polynomial bit and independence budgets give the finite-interval circuit comparison required in the graph application.

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_residue_comparison line 13

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_scalar_residue_comparison line 86

Source documentation

Scalar expansions preserve their signed coefficients through the finite-law comparison; only their total absolute mass enters the error.

theorem BravermanDepth22Input.eventually_scalar_residue_comparison
    (hBr : BravermanDepth22Input) (C : ℝ) (hC : 0 ≤ C) :
    ∃ A : ℕ, 1000 ≤ A ∧ ∀ᶠ L : ℝ in atTop,
      ∀ (m : ℕ) (s : Fin m → ℕ) [∀ i, NeZero (s i)],
      0 < m → (m : ℝ) ≤ Real.exp L + 1 →
      Pairwise (fun i j => (s i).Coprime (s j)) →
      (∀ i, (s i : ℝ) ≤ Real.exp L) →
      ∀ (ι : Type) [Fintype ι] (n : ℕ) (coord : Fin n → Fin m)
        (test : ∀ i, ZMod (s (coord i)) → Bool)
        (c : ι → AC0Circuit n) (coeff : ι → ℝ),
      (∀ i, (c i).depth ≤ 20) → (∀ i, ((c i).size : ℝ) ≤ Real.exp (L ^ 6)) →
      (∑ i, |coeff i|) ≤ Real.exp (C * L ^ 5) →
…

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