OAI/NumberTheory/JointDickman/Arithmetic/RoughMeanBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.rough_normalized_mean_bound line 16

   Source documentation

   The normalized summatory mean is bounded uniformly away from the zero logarithmic scale. Only the cited classical expansion and prime estimates are used.

   theorem rough_normalized_mean_bound
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput) {z δ : ℝ}
       (hz : z = 1 / 4 ∨ z = 1 / 2) (hδ : 0 < δ) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ᶠ B : ℕ in atTop, ∀ Y : ℝ,
         9 ≤ Y → δ * B ≤ Real.log Y →
         roughMeanNormalization B z *
           roughSquarefreeSummatory (Nat.primesLE (auxiliaryCutoff B)) z Y ≤ C * Y := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.roughMeanNormalization, OAI.JointDickman.roughSquarefreeSummatory, OAI.JointDickman.auxiliaryCutoff