HalaszPrimeWindows.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Prime logarithmic windows have bounded von Mangoldt mass at frequency resolution 1/T, once the primes are at least T². This is the precise short-interval sieve consequence used in the Halasz mean-square argument.

lemma OAI.TwoPointCorrelations.halasz_exp_reciprocal_bound line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeWindows.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_prime_window_log_length line 26
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeWindows.lean:26 (same declaration text).

theorem OAI.TwoPointCorrelations.halasz_prime_log_window_bound line 40

Source documentation

A bounded interval of logarithmic length 1/T contains O(1/T) weighted prime mass, uniformly over its position above T².

Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeWindows.lean:40 (same declaration text).

theorem halasz_prime_log_window_bound : ∃ C B : ℝ, 0 < C ∧ 2 ≤ B ∧
    ∀ (T u : ℝ) (P : Finset ℕ), B ≤ T → 1 ≤ u → T ^ 2 ≤ Real.exp u →
      (∀ p ∈ P, p.Prime ∧ u ≤ Real.log (p : ℝ) ∧ Real.log (p : ℝ) ≤ u + 1 / T) →
      (∑ p ∈ P, Real.log (p : ℝ) / (p : ℝ)) ≤ C / T := by
…

theorem OAI.TwoPointCorrelations.halasz_prime_windows_above_square line 112

Source documentation

The same local mass bound for every window, with the lower cutoff imposed on the prime set instead of on the window's left endpoint.

Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeWindows.lean:112 (same declaration text).

theorem halasz_prime_windows_above_square : ∃ C B : ℝ, 0 < C ∧ 2 ≤ B ∧
    ∀ (T : ℝ) (P : Finset ℕ), B ≤ T →
      (∀ p ∈ P, p.Prime ∧ T ^ 2 ≤ (p : ℝ)) → ∀ u : ℝ,
      (∑ p ∈ P.filter (fun (p : ℕ) =>
        u ≤ Real.log (p : ℝ) ∧ Real.log (p : ℝ) ≤ u + 1 / T),
          Real.log (p : ℝ) / (p : ℝ)) ≤ C / T := by
…