MRTPrincipalSmallHeight.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The principal character in the low-height Liouville prime-tail range, from the proved prime-number theorem and a uniform cosine integral bound.

lemma OAI.TwoPointCorrelations.mrt_small_height_phase_error line 15
lemma OAI.TwoPointCorrelations.mrt_principal_twist_re line 57
theorem OAI.TwoPointCorrelations.mrt_liouville_principal_small_height line 70

theorem OAI.TwoPointCorrelations.mrt_liouville_all_characters_small_height line 112

Source documentation

All characters, still restricted to the explicitly proved low-height range.

theorem mrt_liouville_all_characters_small_height : ∃ C : ℝ, 0 ≤ C ∧
    ∀ᶠ X : ℕ in atTop, ∀ q : ℕ, 0 < q →
      (q : ℝ) ≤ (Real.log (X : ℝ)) ^ (1 / 125 : ℝ) →
      ∀ χ : DirichletCharacter ℂ q, ∀ t : ℝ,
        |t| ≤ Real.exp ((Real.log (X : ℝ)) ^ (1 / 3 : ℝ)) →
        -C ≤ (∑ p ∈ mrtLiouvillePrimeTail X, characterTwist χ t p / (p : ℂ)).re := by
…

Mentions: OAI.TwoPointCorrelations.mrtLiouvillePrimeTail

theorem OAI.TwoPointCorrelations.mrt_liouville_distance_small_height line 130

Source documentation

The Liouville distance bound on the same proved low-height range.

theorem mrt_liouville_distance_small_height : ∃ K : ℝ, 0 ≤ K ∧
    ∀ᶠ X : ℕ in atTop, ∀ q : ℕ, 0 < q →
      (q : ℝ) ≤ (Real.log (X : ℝ)) ^ (1 / 125 : ℝ) →
      ∀ χ : DirichletCharacter ℂ q, ∀ t : ℝ,
        |t| ≤ Real.exp ((Real.log (X : ℝ)) ^ (1 / 3 : ℝ)) →
        (1 / 10 : ℝ) * Real.log (Real.log (X : ℝ)) - K ≤
          squaredDistance liouville (characterTwist χ t) X := by
…