HalaszCosineMinorant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A three-harmonic minorant for the prime-phase defect in corrected MRT Lemma A.4(ii). Its mean is 81/256, enough to retain the needed 1/10 after restricting primes above exp((log X)^(27/40)).

lemma OAI.TwoPointCorrelations.halasz_sqrt_polynomial_minorant line 14
lemma OAI.TwoPointCorrelations.halasz_cosine_three_harmonics line 19

theorem OAI.TwoPointCorrelations.halasz_weighted_cosine_repulsion line 34

Source documentation

Three bounded prime-phase sums suffice; no Fourier approximation or limit interchange is needed for this part of the repulsion argument.

theorem halasz_weighted_cosine_repulsion {ι : Type*} (P : Finset ι)
    (w θ : ι → ℝ) (hw : ∀ p ∈ P, 0 ≤ w p) (E : ℝ)
    (h₁ : |∑ p ∈ P, w p*Real.cos (θ p)| ≤ E)
    (h₂ : |∑ p ∈ P, w p*Real.cos (2*θ p)| ≤ E)
    (h₃ : |∑ p ∈ P, w p*Real.cos (3*θ p)| ≤ E) :
    (81/256:ℝ)*(∑ p ∈ P, w p)-(95/256)*E ≤
      ∑ p ∈ P, w p*(1-|Real.cos (θ p/2)|) := by
…