LowWeightEulerBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Numerical Euler-product constants for the large-kernel coefficient energy

theorem OAI.Ostmann.low_weight_euler_bound line 14

Source documentation

A fixed lower cutoff for the small primes suffices for the manuscript's .006 K low-weight norm estimate. No asymptotic prime estimate is assumed.

theorem low_weight_euler_bound (P : Finset ℕ) (hP : ∀ p ∈ P, 10000 ≤ p) :
    Real.exp ((P.card : ℝ) / 200) *
      (∏ p ∈ P, (1 + (1 / 16 : ℝ) ^ 2 + 2 * (1 / 16 : ℝ) * (Real.sqrt (p : ℝ))⁻¹)) ≤
        Real.exp (3 * (P.card : ℝ) / 250) := by
…

theorem OAI.Ostmann.low_weight_euler_norm_bound line 40
theorem OAI.Ostmann.low_weight_euler_bound_scale line 49
theorem OAI.Ostmann.small_kernel_divisor_product_bound line 69
Source documentation
The coarser small-kernel divisor factor is still harmless compared with its exp(-.9 K) loss.
```
theorem small_kernel_divisor_product_bound (K : ℕ) :
    (1 + Real.sqrt 2 / 16) ^ K ≤ Real.exp ((K : ℝ) / 10) := by
…
```