MRTPrimeSparseGram.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The prime-supported sparse mean square keeps the reciprocal logarithmic weight of the coefficient norm. The Mangoldt kernel estimate is an explicit local hypothesis; its analytic proof is separate from this finite duality.

theorem OAI.TwoPointCorrelations.mrt_sparse_divided_weight_energy line 17

Source documentation

The full reciprocal weight in finite weighted Gram duality.

theorem mrt_sparse_divided_weight_energy {ι : Type*}
    (K P : Finset ι) (hPK : P ⊆ K) (w freq : ι → ℝ) (a : ι → ℂ)
    (hw : ∀ n ∈ K, 0 ≤ w n) (hwP : ∀ n ∈ P, 0 < w n)
    (S : Finset ℝ)
    (hsep : ∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|)
    {A D : ℝ} (hA : 0 ≤ A) (hD : 0 ≤ D)
    (hkernel : ∀ t ∈ S, ∀ s ∈ S,
      ‖mrtExponentialPolynomial K (fun n => (w n:ℂ)) freq (t-s)‖ ≤
        A/(1+(t-s)^2)+D) :
    (∑ t ∈ S, ‖mrtExponentialPolynomial P a freq t‖^2) ≤
      (8*A+(S.card:ℝ)*D) * ∑ n ∈ P, ‖a n‖^2/w n := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

theorem OAI.TwoPointCorrelations.mrt_sparse_prime_gram line 63

Source documentation

A nonnegative smooth Mangoldt majorant supplies the exact logarithmic coefficient gain in the prime-supported sparse mean square.

theorem mrt_sparse_prime_gram (K P : Finset ℕ) (hPK : P ⊆ K)
    (hP : ∀ p ∈ P, p.Prime) (ψ : ℕ → ℝ)
    (hψ : ∀ n ∈ K, 0 ≤ ψ n) (hψP : ∀ p ∈ P, 1 ≤ ψ p)
    (a : ℕ → ℂ) (S : Finset ℝ)
    (hsep : ∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|)
    {A D : ℝ} (hA : 0 ≤ A) (hD : 0 ≤ D)
    (hkernel : ∀ t ∈ S, ∀ s ∈ S,
      ‖mrtExponentialPolynomial K
        (fun n => (ψ n * ArithmeticFunction.vonMangoldt n:ℝ))
        (fun n => -Real.log (n:ℝ)) (t-s)‖ ≤ A/(1+(t-s)^2)+D) :
    (∑ t ∈ S, ‖mrtExponentialPolynomial P a
      (fun n => -Real.log (n:ℝ)) t‖^2) ≤
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

theorem OAI.TwoPointCorrelations.mrt_short_prime_logarithmic_mass line 97

Source documentation

The coefficient mass in a short logarithmic prime interval has both logarithmic savings needed by the prime-supported sparse estimate.

theorem mrt_short_prime_logarithmic_mass : ∃ C B : ℝ, 0 < C ∧ 2 ≤ B ∧
    ∀ (H u : ℝ) (P : Finset ℕ) (F : ℕ → ℂ), B ≤ H → 1 ≤ u →
      H^2 ≤ Real.exp u →
      (∀ p ∈ P, p.Prime ∧ u ≤ Real.log (p:ℝ) ∧ Real.log (p:ℝ) ≤ u+1/H) →
      OneBounded F →
      (∑ p ∈ P, ‖F p/(p:ℂ)‖^2/Real.log (p:ℝ)) ≤
        C/(H*Real.exp u*u^2) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded