HalaszPrimePhase.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Prime phase sums on a finite real interval. The prime-number error retains its exponentially small lower-endpoint factor and its explicit frequency dependence.

lemma OAI.TwoPointCorrelations.halasz_prime_band_filter line 15
lemma OAI.TwoPointCorrelations.halasz_prime_phase_sum line 22
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.halasz_prime_phase_error line 36
lemma OAI.TwoPointCorrelations.halasz_log_phase_substitution line 52
lemma OAI.TwoPointCorrelations.halasz_log_phase_lower line 75
lemma OAI.TwoPointCorrelations.halasz_prime_band_tail line 116
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.halasz_prime_phase_lower line 125

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.halasz_masked_phase_lower line 140

Source documentation

A finite quantitative repulsion bound, retaining the actual PNT error.

theorem ModFiveThetaInput.halasz_masked_phase_lower (hP : ModFiveThetaInput) :
    ∃ c K : ℝ, 0 < c ∧ 0 ≤ K ∧ ∀ (F : ℕ → ℂ), OneBounded F →
      ∀ (Q : Finset ℕ) (N : ℕ) (Y t t₁ : ℝ),
      Real.exp 1 ≤ Y → Y ≤ N → 1 ≤ |t - t₁| * Real.log Y →
      squaredDistance F (mrtArchimedeanTwist t₁) N ≤
        squaredDistance F (mrtArchimedeanTwist t) N →
      (Real.log (Real.log N / Real.log Y) - 3 -
        (8 + |t - t₁|) * K * Real.exp (-c * Real.sqrt (Real.log Y)) / Real.log Y) / 8 ≤
          squaredDistance (mrtMissingCoefficient F Q) (mrtArchimedeanTwist t) N := by
…

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