SmallKernelScales.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete small-kernel scale inequality for all divisor moduli

theorem OAI.Ostmann.small_kernel_scale_bound line 12

theorem OAI.Ostmann.eventual_small_kernel_norm_from_ranges line 30

Source documentation

The manuscript's range s <= L^4, v <= L and R >= L^6 automatically supplies the small-kernel bound for every divisor of L.

theorem eventual_small_kernel_norm_from_ranges (C₀ H ε : ℝ) (Φ : 𝓢(ℝ, ℂ))
    (hH : 0 ≤ H) (hε : 0 < ε) (hΦ : ∀ x : ℝ, H < x → Φ x = 0) :
    ∀ᶠ T : ℝ in atTop, ∀ (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
      (M : ℕ) (S : Finset ℕ) (u : ℝ),
      (M : ℝ) ≤ Real.exp (C₀ * T) → (P.card : ℝ) ≤ T ^ (9999999 / 10000000 : ℝ) →
      (∀ s ∈ S, Squarefree s ∧ s ≤ M ∧ s ≤ P.toList.prod ^ 4) →
      0 ≤ u → u ≤ 4 * T ^ (1 / 1000000 : ℝ) →
      ∀ (D : ∀ p : ℕ, Finset (ZMod p))
        (a : ∀ U : Finset ℕ, ZMod U.toList.prod) (θ : Finset ℕ → ℝ)
        (R v : ℝ) (c : Finset ℕ → ℂ),
      (P.toList.prod : ℝ) ^ 6 ≤ R → 0 < v → v ≤ P.toList.prod →
      (∀ U ∈ P.powerset, ‖c U‖ ≤ (1 / 16 : ℝ) ^ U.card) →
…