LowDegreeNumerical.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.low_degree_bound_of_noise_projection line 13

Source documentation

The numerical part of the biased low-degree estimate, with its original noise loss.

theorem low_degree_bound_of_noise_projection {ι : Type u} [Fintype ι]
    (a : ι → ℝ) (m I σ L : ℝ)
    (hm : 1 ≤ m) (hσ : 0 < σ) (hσhalf : σ ≤ 1 / 2)
    (ha : ∀ i, 0 ≤ a i) (hsum : ∑ i, a i = I)
    (hindividual : ∀ i, a i ≤ I / m) (hL1 : L ≤ 1)
    (hprojection : L ≤ σ ^ 2 * (σ / 4) ^
      (-(2 : ℝ) * (σ * Real.log m / 64)) * ∑ i, (a i) ^ (3 / 2 : ℝ)) :
    L ≤ m ^ (-1 / 4 : ℝ) * I := by
…

theorem OAI.Problem313.bernoulli_stddev_bounds line 29
Source documentation
The Bernoulli standard deviation lies in the range required by the noise estimate.
```
theorem bernoulli_stddev_bounds {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    0 < Real.sqrt (p * (1 - p)) ∧ Real.sqrt (p * (1 - p)) ≤ 1 / 2 := by
…
```

theorem OAI.Problem313.low_degree_bound_of_biased_projection line 38

Source documentation

Bias-parameter form of the numerical low-degree estimate.

theorem low_degree_bound_of_biased_projection {ι : Type u} [Fintype ι]
    (a : ι → ℝ) (m I p L : ℝ)
    (hm : 1 ≤ m) (hp : 0 < p) (hp1 : p < 1)
    (ha : ∀ i, 0 ≤ a i) (hsum : ∑ i, a i = I)
    (hindividual : ∀ i, a i ≤ I / m) (hL1 : L ≤ 1)
    (hprojection : L ≤ (p * (1 - p)) * (Real.sqrt (p * (1 - p)) / 4) ^
      (-(2 : ℝ) * (Real.sqrt (p * (1 - p)) * Real.log m / 64)) *
      ∑ i, (a i) ^ (3 / 2 : ℝ)) :
    L ≤ m ^ (-1 / 4 : ℝ) * I := by
…