MRTLiouvilleDistance.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite prime identities in the Liouville specialization of MRT, including the reduction to the uniform lower bound for the real part of the character prime sum in (1.12) of arXiv:1503.05121v3.

lemma OAI.TwoPointCorrelations.mrt_liouville_prime line 16
lemma OAI.TwoPointCorrelations.mrt_characterTwist_pow line 20
lemma OAI.TwoPointCorrelations.mrt_prime_sum_real line 29
lemma OAI.TwoPointCorrelations.mrt_liouville_distance_sum line 37
lemma OAI.TwoPointCorrelations.mrt_liouville_distance_prime_sum line 46
lemma OAI.TwoPointCorrelations.mrt_liouville_distance_band_lower line 53
def OAI.TwoPointCorrelations.mrtLiouvillePrimeTail line 68

theorem OAI.TwoPointCorrelations.mrt_liouville_prime_tail_mass line 72

Source documentation

Mertens supplies a quarter of log log X on the exact VK tail.

theorem mrt_liouville_prime_tail_mass :
    ∃ C : ℝ, 0≤C ∧ ∀ X : ℕ, 1≤Real.log (X:ℝ) →
      (1/4:ℝ)*Real.log (Real.log (X:ℝ))-C ≤
        ∑ p ∈ mrtLiouvillePrimeTail X, 1/(p:ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.mrtLiouvillePrimeTail

theorem OAI.TwoPointCorrelations.mrt_liouville_distance_from_prime_tail line 84

Source documentation

A character prime-tail lower bound yields the Liouville pretentious-distance estimate.

theorem mrt_liouville_distance_from_prime_tail (K : ℝ)
    (htail : ∀ᶠ X : ℕ in atTop, ∀ q : ℕ, 0<q →
      (q:ℝ)≤(Real.log (X:ℝ))^(1/125:ℝ) →
      ∀ χ : DirichletCharacter ℂ q, ∀ t : ℝ, |t|≤X →
        -K ≤ (∑ p ∈ mrtLiouvillePrimeTail X,
          characterTwist χ t p/((p:ℝ):ℂ)).re) :
    ∃ K' : ℝ, 0≤K' ∧ ∀ᶠ X : ℕ in atTop, ∀ q : ℕ, 0<q →
      (q:ℝ)≤(Real.log (X:ℝ))^(1/125:ℝ) →
      ∀ χ : DirichletCharacter ℂ q, ∀ t : ℝ, |t|≤X →
        (1/10:ℝ)*Real.log (Real.log (X:ℝ))-K' ≤
          squaredDistance liouville (characterTwist χ t) X := by
…

Mentions: OAI.TwoPointCorrelations.mrtLiouvillePrimeTail