QualitativeRoughFourier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The qualitative rough multiplier, with arbitrary bounded complex coefficients, obtained directly from the finite four-form sieve.

lemma OAI.TwoPointCorrelations.rpow_neg_hundred_le_qualitative_rate line 16

theorem OAI.TwoPointCorrelations.PrimeReciprocalInput.qualitative_rough_fourier line 43

Source documentation

The manuscript qualitative multiplier estimate. Its fourth moment has only four logarithmic factors, which is stronger than the six needed in the analytic transfer.

theorem PrimeReciprocalInput.qualitative_rough_fourier (hM : PrimeReciprocalInput) :
    ∃ U V : ℝ, 0 < U ∧ 0 < V ∧ ∀ᶠ B : ℝ in atTop,
      ∀ (D h : ℕ), (1 / 2 : ℝ) * Real.exp (B ^ (9999 / 10000 : ℝ)) ≤ D → 0 < h →
      ∀ (Z : Finset ℕ) (c : ℕ → ℂ),
      (∀ z ∈ Z, D ≤ z ∧ z < D + D ∧
        HasNoPrimeFactorBelow (Real.exp (B ^ (9999 / 10000 : ℝ))) z) →
      (∀ z ∈ Z, ‖c z‖ ≤ 1) →
      (∀ θ, ‖weightedRoughFourier Z c h θ‖ ≤
        U * (Real.log B / B ^ (9999 / 10000 : ℝ))) ∧
      (∫ θ, ‖weightedRoughFourier Z c h θ‖ ^ 4 ∂AddCircle.haarAddCircle) ≤
        V / (D : ℝ) * (Real.log B / B ^ (9999 / 10000 : ℝ)) ^ 4 := by
…

Mentions: OAI.TwoPointCorrelations.PrimeReciprocalInput, OAI.TwoPointCorrelations.HasNoPrimeFactorBelow, OAI.TwoPointCorrelations.weightedRoughFourier