LowDegreeConstants.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.sigma_mul_log_four_div_le_two line 12
Source documentation
Uniform bias-dependent logarithmic bound used in the low-degree estimate.
```
theorem sigma_mul_log_four_div_le_two {σ : ℝ} (hσ : 0 < σ)
    (hσhalf : σ ≤ 1 / 2) : σ * Real.log (4 / σ) ≤ 2 := by
…
```

theorem OAI.Problem313.noise_loss_le_rpow line 39

Source documentation

The noise loss has a uniformly small power of the orbit-size parameter.

theorem noise_loss_le_rpow {σ m : ℝ} (hσ : 0 < σ)
    (hσhalf : σ ≤ 1 / 2) (hm : 1 ≤ m) :
    (σ / 4) ^ (-(2 : ℝ) * (σ * Real.log m / 64)) ≤ m ^ (1 / 16 : ℝ) := by
…

theorem OAI.Problem313.sigma_sq_mul_rpow_le line 57

Source documentation

Absorb the residual quarter-variance factor and the stronger exponent.

theorem sigma_sq_mul_rpow_le {σ m : ℝ} (hσ : 0 ≤ σ)
    (hσhalf : σ ≤ 1 / 2) (hm : 1 ≤ m) :
    σ ^ 2 * m ^ (-5 / 16 : ℝ) ≤ m ^ (-1 / 4 : ℝ) := by
…

theorem OAI.Problem313.influence_three_halves_le line 70

Source documentation

An individual influence contributes a small extra factor when total influence is small.

theorem influence_three_halves_le {a I m : ℝ} (ha : 0 ≤ a) (hm : 1 ≤ m)
    (hai : a ≤ I / m) (hI : I ≤ m ^ (1 / 4 : ℝ)) :
    a ^ (3 / 2 : ℝ) ≤ m ^ (-3 / 8 : ℝ) * a := by
…

theorem OAI.Problem313.sum_influence_three_halves_le line 97

Source documentation

Sum the individual three-halves estimate without a cardinality loss.

theorem sum_influence_three_halves_le {ι : Type u} (s : Finset ι) (a : ι → ℝ)
    {m : ℝ} (hm : 1 ≤ m) (ha : ∀ i ∈ s, 0 ≤ a i)
    (horbit : ∀ i ∈ s, a i ≤ (∑ j ∈ s, a j) / m)
    (hsmall : (∑ j ∈ s, a j) ≤ m ^ (1 / 4 : ℝ)) :
    (∑ i ∈ s, a i ^ (3 / 2 : ℝ)) ≤ m ^ (-3 / 8 : ℝ) * (∑ i ∈ s, a i) := by
…