KernelAnalyticParameters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete error absorption for the quadratic-kernel parameters

theorem OAI.Ostmann.exists_kernel_size_exponent line 11
Source documentation
Choose the kernel-size exponent after the absolute zero-comparison constant has been fixed.
```
theorem exists_kernel_size_exponent (Cz : ℝ) (hCz : 5 ≤ Cz) :
    ∃ η : ℝ, 0 < η ∧ η ≤ 1 / 1000 ∧ 4 * Cz * η = 1 / 40000 := by
…
```
theorem OAI.Ostmann.kernel_sqrt_error_absorption line 20
theorem OAI.Ostmann.page_threshold_siegel_power line 29
Source documentation
The Page threshold is (log X)^100 and Siegel is used only at exponent 1/200, giving a square-root error in log X.
```
theorem page_threshold_siegel_power (L : ℝ) (hL : 0 ≤ L) :
    ((L ^ (100 : ℕ)) : ℝ) ^ (1 / 200 : ℝ) = Real.sqrt L := by
…
```

theorem OAI.Ostmann.kernel_zero_error_absorption line 37

Source documentation

The logarithmic conductor cost and square-root Siegel cost are both absorbed by the chosen fixed coefficient of L.

theorem kernel_zero_error_absorption (Cz η K A H L logQ : ℝ)
    (hCz : 0 ≤ Cz) (hK : 0 ≤ K) (hL : 0 ≤ L)
    (hη : 4 * Cz * η ≤ 1 / 40000)
    (hQ : logQ ≤ 2 * η * L + Real.log 20)
    (hKsize : (40000 * K) ^ 2 ≤ L)
    (hconst : 40000 * (2 * Cz * Real.log 20 + H + A + 2) ≤ L) :
    2 * Cz * logQ + K * Real.sqrt L + H + A + 2 ≤ L / 10000 := by
…

theorem OAI.Ostmann.kernel_divisor_error_absorption line 50

Source documentation

The elementary divisor bound is o(L) with a square-root cutoff.

theorem kernel_divisor_error_absorption (D Y : ℕ) (L : ℝ)
    (hL : 0 < L) (hlarge : (40000 : ℝ) ^ 2 ≤ L)
    (hYlo : Real.sqrt L ≤ Y) (hYhi : (Y : ℝ) ≤ Real.sqrt L + 1)
    (hlogD : Real.log D ≤ L) :
    (Y : ℝ) + Real.log D / Y ≤ L / 10000 := by
…