PrimeDetector.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's exact prime detector on a fixed norm envelope. The finite weighted identity applies to both squarefree-supported kernels, with the same coefficients before any estimate is used.

lemma OAI.CubicFirstMoment.eventually_prime_detector_window line 15
lemma OAI.CubicFirstMoment.squarefree_kernel_prime_detector line 35

theorem OAI.CubicFirstMoment.prime_detector_finite_envelope line 54

Source documentation

Exact finite prime sum decomposition on an arbitrary fixed envelope. No analytic estimate and no kernel-specific coefficient is introduced.

theorem prime_detector_finite_envelope {c C : ℝ} (hc : 0 < c) (hC : 0 < C)
    {ψ : ℝ → ℝ}
    (hψone : ∀ x : ℝ, 0 < x → x ≤ 1 → ψ x = 1)
    (hψzero : ∀ x : ℝ, 2 ≤ x → ψ x = 0) :
    ∀ᶠ X : ℝ in atTop, ∀ (S : Finset Eisenstein) (K : Eisenstein → ℂ),
      (∀ n ∈ S, c*X ≤ norm n ∧ norm n ≤ C*X) →
      (∀ n ∈ S, ¬Squarefree n → K n = 0) →
      (∑ n ∈ S with Prime n, K n) =
        (∑ n ∈ S, (roughProduct ψ (X^(2/5:ℝ)) n:ℂ)*K n) -
          ∑ n ∈ S with (primeFactors n).card = 2,
            (roughProduct ψ (X^(2/5:ℝ)) n:ℂ)*K n := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primeFactors