FourierMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counting low-order Fourier coefficients

The number of nonempty coordinate sets of order at most t is at most (t+1)n^t. Combining individual coefficient bounds with this count gives the explicit error budget used by finite residue comparison.

lemma OAI.TwoPointCorrelations.card_lowWalshSets_le line 19
lemma OAI.TwoPointCorrelations.lowWalshMass_le_of_coefficients line 43

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.coefficient_comparison line 59

Source documentation

The fixed-parameter finite-law consequence of Braverman's theorem: only the individual low-order Fourier errors and the actual circuit size and depth occur as hypotheses.

theorem BravermanDepth22Input.coefficient_comparison (hBraverman : BravermanDepth22Input) :
    ∃ K C : ℕ, 0 < K ∧ 0 < C ∧ ∀ (n : ℕ), 0 < 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 ≤ δ →
          (∀ S ∈ lowWalshSets n t, |walshCoefficient f S| ≤ δ) →
          δ * ((t + 1 : ℕ) : ℝ) * (n : ℝ) ^ 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.lowWalshSets, OAI.TwoPointCorrelations.walshCoefficient