MRTWeakVKApplications.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual character tails and the two required distance consequences of weak Hurwitz growth. The growth proposition remains an explicit premise.

theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.power_prime_tail line 15

theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.liouville_distance line 39

Source documentation

This is the full original modulus/height range, conditional only on the explicit weak Hurwitz growth input.

theorem MRTWeakHurwitzGrowthInput.liouville_distance (h : MRTWeakHurwitzGrowthInput) :
    ∃ 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.MRTWeakHurwitzGrowthInput

theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.high_prime line 72
Source documentation
The three harmonic phases needed for high-prime repulsion use only the principal character of modulus one.
```
theorem MRTWeakHurwitzGrowthInput.high_prime (h : MRTWeakHurwitzGrowthInput) :
    HalaszHighPrimeInput := by
…
```
Mentions: OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput, OAI.TwoPointCorrelations.HalaszHighPrimeInput