LargeKernelNorm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The large-kernel norm of the original positive quadratic series

theorem OAI.Ostmann.eventual_large_kernel_positive_norm line 15

Source documentation

The .006 + o(1) bound over the full large-kernel range. The coefficient family is the original compactly supported quadratic series, and the dyadic decomposition and all residue estimates are supplied by proved lemmas.

theorem eventual_large_kernel_positive_norm (C₀ H ε : ℝ) (Φ : 𝓢(ℝ, ℂ))
    (hC₀ : 0 ≤ C₀) (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 : ℝ),
      (∀ p ∈ P, 10000 ≤ p) → (M : ℝ) ≤ Real.exp (C₀ * T) →
      (P.card : ℝ) ≤ T ^ (9999999 / 10000000 : ℝ) →
      (∀ s ∈ S, Squarefree s) → (∀ s ∈ S, 4 * P.toList.prod ^ 2 ≤ s ∧ s ≤ M) →
      (∀ s ∈ S, P.toList.prod.Coprime s) → 2 ≤ u → u ≤ 4 * T ^ (1 / 1000000 : ℝ) →
      ∀ (D : ∀ p : ℕ, Finset (ZMod p))
        (a : ∀ U : Finset ℕ, ZMod U.toList.prod) (θ : Finset ℕ → ℝ)
        (R v : ℝ) (c : Finset ℕ → ℂ),
      0 < R → 0 < v → (∀ U ∈ P.powerset, ‖c U‖ ≤ (1 / 16 : ℝ) ^ U.card) →
…