AffineKernelBias.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual squarefree kernels retain the common-center character bias

theorem OAI.Ostmann.quadraticPrimeMean_zero line 12
theorem OAI.Ostmann.exists_affine_kernel_assignment line 21
theorem OAI.Ostmann.kernel_root_log_bound line 35
theorem OAI.Ostmann.kernel_prime_divisor_loss line 47

theorem OAI.Ostmann.exists_biased_affine_kernels line 59

Source documentation

A single actual kernel assignment is shared by all later tests.

theorem exists_biased_affine_kernels (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (S : Finset ℤ) (m : ℕ) (h : ℤ) (e : ℕ → ℂ) (c T Y : ℝ)
    (hc : 0 < c) (hT : 0 < T) (hcard : 0 < P.card) (he : ∀ p ∈ P, ‖e p‖ ≤ 1)
    (hlogp : ∀ p ∈ P, T ≤ Real.log (p : ℝ))
    (hsize : 2 * Y ≤ (c / 2) * P.card * T)
    (hbound : ∀ x ∈ S, |(((m : ℤ) * x - h : ℤ) : ℝ)| ≤ Real.exp Y)
    (hbias : ∀ x ∈ S, c ≤ ‖quadraticPrimeMean P e ((m : ℤ) * x - h)‖) :
    ∃ (kernel : ℤ → ℤ) (root : ℤ → ℕ), ∀ x ∈ S,
      kernel x ≠ 0 ∧ 0 < root x ∧ Squarefree (kernel x).natAbs ∧
      kernel x * (root x : ℤ) ^ 2 = (m : ℤ) * x - h ∧
      c / 2 ≤ ‖quadraticPrimeMean P e (kernel x)‖ := by
…