OAI/NumberTheory/JointDickman/Amplification/HalaszArithmetic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.halasz_distance_eq line 11
2. theorem OAI.JointDickman.halasz_arithmetic_mean_value line 32

   Source documentation

   The logarithmic-height mean bound for normalized ordinary multiplicative functions, with the exact prime-distance convention used in this result.

   theorem halasz_arithmetic_mean_value : ∃ C X₀ : ℝ, 0 < C ∧
       ∀ N : ℕ, X₀ ≤ N → ∀ f : ArithmeticFunction ℂ,
         f.IsMultiplicative → (∀ n, ‖f n‖ ≤ 1) → ∀ M : ℝ, 0 ≤ M →
         (∀ t : ℝ, |t| ≤ Real.log (N : ℝ)^8 → M ≤ primeDistanceSquared f N t) →
         ‖∑ n ∈ Icc 1 N, f n‖ ≤ C*N*
           ((M+1)*Real.exp (-M) + Real.log (Real.log N)/Real.log N) := by
   …