HalaszModeratePhase.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform prime-phase repulsion for the moderate-frequency part of MRT Appendix A. The fourth-root logarithmic coordinate keeps the exponentially small PNT error separate from the polynomial frequency range.

lemma OAI.TwoPointCorrelations.halasz_polynomial_phase_error line 16
lemma OAI.TwoPointCorrelations.halasz_logarithmic_phase_scale line 32

theorem OAI.TwoPointCorrelations.halasz_moderate_masked_distance line 53

Source documentation

Uniform masked distance repulsion in the moderate frequency range. The lower bound is independent of the deleted prime set.

theorem halasz_moderate_masked_distance :
    ∀ᶠ y : ℝ in atTop, ∀ (F : ℕ → ℂ), OneBounded F →
      ∀ (Q : Finset ℕ) (N : ℕ) (t t₁ : ℝ), Real.log N = y ^ 4 →
      1 ≤ |t - t₁| * y ^ 2 → |t - t₁| ≤ y ^ 80 →
      squaredDistance F (mrtArchimedeanTwist t₁) N ≤
        squaredDistance F (mrtArchimedeanTwist t) N →
      Real.log (Real.log N) / 16 - 1 / 2 ≤
        squaredDistance (mrtMissingCoefficient F Q) (mrtArchimedeanTwist t) N := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.mrtMissingCoefficient

theorem OAI.TwoPointCorrelations.halasz_moderate_distance_nat line 79

Source documentation

The moderate-frequency clause in the original natural cutoff, with a fixed positive margin over the exponent needed in the last MRT class.

theorem halasz_moderate_distance_nat :
    ∀ᶠ N : ℕ in atTop, ∀ (F : ℕ → ℂ), OneBounded F →
      ∀ (Q : Finset ℕ) (t t₁ : ℝ),
      (Real.log N) ^ (1 / (16 : ℝ)) / 2 ≤ |t - t₁| →
      |t - t₁| ≤ (Real.log N) ^ 20 →
      squaredDistance F (mrtArchimedeanTwist t₁) N ≤
        squaredDistance F (mrtArchimedeanTwist t) N →
      (31 / 500 : ℝ) * Real.log (Real.log N) ≤
        squaredDistance (mrtMissingCoefficient F Q) (mrtArchimedeanTwist t) N := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.mrtMissingCoefficient