HighDegreeWeights.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.remaining_degreeWeight_product_bound line 13

Source documentation

Remaining unexpanded factors cost at most one factor of five per large occurrence, and a total exponential error for the low occurrences.

theorem remaining_degreeWeight_product_bound {ι : Type*} (I : Finset ι)
    (e : ι → ℕ) {n s q : ℝ} (hn : 0 < n) (hs : 0 < s)
    (hshi : s ≤ Real.sqrt n) (hq : 0 < q) (hqhalf : q ≤ 1 / 2)
    (hqsqrt : q ≤ 2 / Real.sqrt n)
    (hqsmall : 5 * q ^ ((3 : ℝ) / 16) ≤ 1)
    (he : ∀ i ∈ I, 0 < e i) (hsum : (∑ i ∈ I, (e i : ℝ)) ≤ n) :
    (∏ i ∈ I, degreeWeight q (1 / 2 - s / (2 * n)) (e i)) ≤
      (5 : ℝ) ^ (4 * s) * Real.exp (24 * Real.sqrt n) := by
…

Mentions: OAI.Problem335.degreeWeight

theorem OAI.Problem335.high_degreeWeight_product_bound line 68

Source documentation

The actual factor weights in the one-high case obey the strong power saving required by the homogeneous depth-five circuit rank argument.

theorem high_degreeWeight_product_bound {ι : Type*} (I : Finset ι)
    (e : ι → ℕ) (d : ℕ) {n s q : ℝ} (hn : 1 ≤ n) (hs : 0 < s)
    (hshi : s ≤ Real.sqrt n) (hq : 0 < q) (hqhalf : q ≤ 1 / 2)
    (hqsqrt : q ≤ 2 / Real.sqrt n) (hqpow : q ≤ n ^ (-(2 : ℝ) / 5))
    (hqsmall : 5 * q ^ ((3 : ℝ) / 16) ≤ 1)
    (hlam : (3 : ℝ) / 8 ≤ 1 / 2 - s / (2 * n))
    (htone : 1 < n / (4 * s)) (hd : n / (4 * s) ≤ (d : ℝ))
    (he : ∀ i ∈ I, 0 < e i) (hsum : (∑ i ∈ I, (e i : ℝ)) ≤ n) :
    degreeWeight q (1 / 2 - s / (2 * n)) 1 ^ d *
        (∏ i ∈ I, degreeWeight q (1 / 2 - s / (2 * n)) (e i)) ≤
      (5 : ℝ) ^ (4 * s) * Real.exp (24 * Real.sqrt n) *
        n ^ (-(3 * Real.sqrt n) / 160) := by
…

Mentions: OAI.Problem335.degreeWeight

theorem OAI.Problem335.expanded_degreeWeight_product_bound line 115

Source documentation

The circuit interface only assumes n ≥ 64: the required slope and threshold bounds follow from s ≤ sqrt n. This adapter reconciles the canonical high-weight estimate with the circuit product interface.

theorem expanded_degreeWeight_product_bound {ι : Type*} (I : Finset ι) (e : ι → ℕ)
    (d : ℕ) {n s q : ℝ} (hn : 64 ≤ n) (hs : 0 < s) (hshi : s ≤ Real.sqrt n)
    (hq : 0 < q) (hqhalf : q ≤ 1 / 2) (hqsqrt : q ≤ 2 / Real.sqrt n)
    (hqpow : q ≤ n ^ (-(2 / 5 : ℝ))) (hqsmall : 5 * q ^ ((3 : ℝ) / 16) ≤ 1)
    (he : ∀ i ∈ I, 0 < e i) (hsum : ∑ i ∈ I, (e i : ℝ) ≤ n)
    (hd : n / (4 * s) ≤ (d : ℝ)) :
    (degreeWeight q (1 / 2 - s / (2 * n)) 1) ^ d *
      (∏ i ∈ I, degreeWeight q (1 / 2 - s / (2 * n)) (e i)) ≤
      (5 : ℝ) ^ (4 * s) * Real.exp (24 * Real.sqrt n) *
        n ^ (-(3 * Real.sqrt n / 160)) := by
…

Mentions: OAI.Problem335.degreeWeight