MRTWeakHurwitzGrowth.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Weak Vinogradov--Korobov growth for the Hurwitz zeta function with its first term removed, and the finite-character reduction.

def OAI.TwoPointCorrelations.mrtVKLog line 13
def OAI.TwoPointCorrelations.mrtVKRadius line 15
def OAI.TwoPointCorrelations.mrtHurwitzFirstTerm line 17
def OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput line 22
Source documentation
A polynomial logarithmic bound on the shrinking VK disk. Removing the first Hurwitz term makes the bound uniform down to a = 0.
```
def MRTWeakHurwitzGrowthInput : Prop :=
…
```
lemma OAI.TwoPointCorrelations.mrt_hurwitz_first_term_bound line 29

theorem OAI.TwoPointCorrelations.mrt_character_of_hurwitz_growth line 52

Source documentation

Exact finite Hurwitz decomposition retains a polynomial modulus cost.

theorem mrt_character_of_hurwitz_growth {q : ℕ} [NeZero q]
    (χ : DirichletCharacter ℂ q) {s : ℂ} {A : ℝ}
    (hσ : 0 ≤ s.re) (hσ2 : s.re ≤ 2)
    (hh : ∀ a ∈ Set.Icc (0 : ℝ) 1,
      ‖hurwitzZeta (a : UnitAddCircle) s - mrtHurwitzFirstTerm a s‖ ≤ A) :
    ‖DirichletCharacter.LFunction χ s‖ ≤ (q : ℝ) * ((q : ℝ) ^ 2 + A) := by
…

Mentions: OAI.TwoPointCorrelations.mrtHurwitzFirstTerm

lemma OAI.TwoPointCorrelations.mrt_moving_point_region line 92

theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.character_disk line 107

Source documentation

Applying the weak Hurwitz input to the actual moving character disk.

theorem MRTWeakHurwitzGrowthInput.character_disk (h : MRTWeakHurwitzGrowthInput) :
    ∃ C T : ℝ, 0 < C ∧ 0 < T ∧ ∀ t : ℝ, T ≤ |t| →
      mrtVKRadius t ≤ 1 / 5 → ∀ (q : ℕ) [NeZero q],
      ∀ (χ : DirichletCharacter ℂ q), ∀ z : ℂ, ‖z‖ ≤ 1 →
        ‖DirichletCharacter.LFunction χ (mrtMovingPoint (mrtVKRadius t) t z)‖ ≤
          (q : ℝ) * ((q : ℝ) ^ 2 + (mrtVKLog t) ^ C) := by
…

Mentions: OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput, OAI.TwoPointCorrelations.mrtVKRadius, OAI.TwoPointCorrelations.mrtMovingPoint, OAI.TwoPointCorrelations.mrtVKLog