OAI/NumberTheory/Ostmann/Characters/SparseKernelNumerics.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sparse_kernel_numeric_margin line 12

   Source documentation

   The scalar decrease survives both the square kernel and the cost of the side blocks. The fixed epsilon here is deliberately smaller than necessary.

   theorem sparse_kernel_numeric_margin (p ε s U : ℝ) (hp : 100 ≤ p)
       (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 1000000)
       (hs : s ≤ 1 - (17 / 10) * (1 - ε ^ 2) / p + (289 / 100) * ε / p)
       (hU : 1 - 4 * ε / p ≤ U) :
       s + 20 * (6 * ε / Real.sqrt p) ^ 2 ≤ U * (1 - (8 / 5) / p) := by
   …