HalaszDoubleMean.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The ordinary mean reduces to the adaptive double prime convolution, with an explicit N log log N error.

def OAI.TwoPointCorrelations.halaszDenominatorConstant line 13
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleMean.lean:13 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_double_mean_bound line 16
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleMean.lean:16 (same declaration text).
def OAI.TwoPointCorrelations.halaszDoubleErrorConstant line 41
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleMean.lean:41 (same declaration text).
lemma OAI.TwoPointCorrelations.halaszDoubleErrorConstant_nonneg line 45
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleMean.lean:45 (same declaration text).

theorem OAI.TwoPointCorrelations.halasz_double_mean_log_fourth line 54

Source documentation

The logarithmic-fourth-power prime cutoff used in the mean-value proof.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleMean.lean:54 (same declaration text).

theorem halasz_double_mean_log_fourth (f : ℕ → ℂ) (hf : OneBounded f)
    (hmul : ∀ m n : ℕ, 0 < m → 0 < n → f (m * n) = f m * f n)
    (N : ℕ) (hlog : 1 ≤ Real.log (Real.log (N : ℝ)))
    (hL : 1 ≤ Real.log (N : ℝ) ^ 4)
    (hLN : Real.log (N : ℝ) ^ 4 ≤ (N : ℝ) / 2) :
    Real.log (N : ℝ) * ‖∑ n ∈ Icc 1 N, f n‖ ≤
      ‖halaszDoubleConvolution f N (Real.log (N : ℝ) ^ 4)‖ +
        halaszDoubleErrorConstant * (N : ℝ) * Real.log (Real.log N) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszDoubleConvolution, OAI.TwoPointCorrelations.halaszDoubleErrorConstant

theorem OAI.TwoPointCorrelations.halasz_double_mean_log_sixteenth line 89

Source documentation

The larger fixed logarithmic cutoff needed by the narrow-window truncation. The deletion error still has order N log log N.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleMean.lean:89 (same declaration text).

theorem halasz_double_mean_log_sixteenth (f : ℕ → ℂ) (hf : OneBounded f)
    (hmul : ∀ m n : ℕ, 0 < m → 0 < n → f (m * n) = f m * f n)
    (N : ℕ) (hlog : 1 ≤ Real.log (Real.log (N : ℝ)))
    (hL : 1 ≤ Real.log (N : ℝ) ^ 16)
    (hLN : Real.log (N : ℝ) ^ 16 ≤ (N : ℝ) / 2) :
    Real.log (N : ℝ) * ‖∑ n ∈ Icc 1 N, f n‖ ≤
      ‖halaszDoubleConvolution f N (Real.log (N : ℝ) ^ 16)‖ +
        (halaszDoubleErrorConstant + 12) * (N : ℝ) * Real.log (Real.log N) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszDoubleConvolution, OAI.TwoPointCorrelations.halaszDoubleErrorConstant