CardinalKernelNorm.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coefficient norms at the actual cardinality of the selected primes

theorem OAI.Ostmann.kernelScale_range line 14

theorem OAI.Ostmann.eventual_large_kernel_norm_card line 27

Source documentation

The large-kernel norm has exponent .006 K, with K the actual number of selected primes, including when K is a small fixed multiple of the original analytic scale.

theorem eventual_large_kernel_norm_card (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 : ℝ),
      T ^ (9999999 / 10000000 : ℝ) / 1000 ≤ (P.card : ℝ) →
      (∀ p ∈ P, 10000 ≤ p) → (M : ℝ) ≤ Real.exp (C₀ * T) →
      (∀ s ∈ S, Squarefree s) →
      (∀ s ∈ S, 4 * P.toList.prod ^ 2 ≤ s ∧ s ≤ M) →
      (∀ s ∈ S, P.toList.prod.Coprime s) →
      2 ≤ u → u ≤ 2 * T ^ (1 / 1000000 : ℝ) →
      ∀ (D : ∀ p : ℕ, Finset (ZMod p))
…

theorem OAI.Ostmann.eventual_small_kernel_norm_card line 56
theorem OAI.Ostmann.eventual_off_witness_norm_card line 83