LowDegreeWeights.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem335.degreeWeight_nonneg line 11
lemma OAI.Problem335.degreeWeight_le_five_mul_distance line 15
lemma OAI.Problem335.low_odd_degreeWeight_le line 30
lemma OAI.Problem335.low_even_degreeWeight_le line 52
lemma OAI.Problem335.low_degreeWeight_le_with_correction line 68

theorem OAI.Problem335.low_degreeWeight_product_bound line 88

Source documentation

The actual factor weights, rather than hypothetical costs, give the all-low product saving in the circuit argument.

theorem low_degreeWeight_product_bound {ι : Type*} (I : Finset ι) (e : ι → ℕ)
    {n s q : ℝ} (hn : 1 ≤ n) (hs : 0 < s)
    (hslo : Real.sqrt n / 2 ≤ 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) (helow : ∀ i ∈ I, (e i : ℝ) < n / (4 * s))
    (hsum : ∑ i ∈ I, (e i : ℝ) = n) :
    (∏ i ∈ I, degreeWeight q (1 / 2 - s / (2 * n)) (e i)) ≤
      Real.exp (24 * Real.sqrt n) * n ^ (-Real.sqrt n / 20) := by
…

Mentions: OAI.Problem335.degreeWeight