OAI/NumberTheory/JointDickman/Arithmetic/RoughDensityLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.roughDensityPolynomial line 18
2. def OAI.JointDickman.scaledRoughDensity line 23
3. theorem OAI.JointDickman.scaledRoughDensity_eq line 28
4. theorem OAI.JointDickman.scalar_power_uniform line 50

   Source documentation

   A coefficient limit gives a uniform limit for a fixed negative power.

   theorem scalar_power_uniform {a δ c : ℝ} {u : ℕ → ℝ}
       (ha : a ≤ 0) (hδ : 0 < δ) (hu : Tendsto u atTop (𝓝 c)) :
       TendstoUniformlyOn (fun (B : ℕ) (s : ℝ) => u B * s ^ a)
         (fun s => c * s ^ a) atTop (Set.Ici δ) := by
   …

5. theorem OAI.JointDickman.finite_power_uniform line 71

   Source documentation

   Finite fixed powers preserve uniform convergence of their coefficients.

   theorem finite_power_uniform (S : Finset ℕ) (a c : ℕ → ℝ) (u : ℕ → ℕ → ℝ)
       {δ : ℝ} (hδ : 0 < δ) (ha : ∀ j ∈ S, a j ≤ 0)
       (hu : ∀ j ∈ S, Tendsto (fun B => u B j) atTop (𝓝 (c j))) :
       TendstoUniformlyOn (fun B s => ∑ j ∈ S, u B j * s ^ a j)
         (fun s => ∑ j ∈ S, c j * s ^ a j) atTop (Set.Ici δ) := by
   …

6. theorem OAI.JointDickman.scaledRoughDensity_tendstoUniformlyOn line 87

   Source documentation

   The density converges uniformly on every interval bounded away from zero. The stronger half-line statement is available because all exponents are negative.

   theorem scaledRoughDensity_tendstoUniformlyOn
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput)
       (c : ℕ → ℝ) {z δ : ℝ} (hc : c 0 = squarefreeLeadingConstant z)
       (hz : 0 < z) (hzhalf : z ≤ 1 / 2) (hδ : 0 < δ) (H : ℕ) :
       TendstoUniformlyOn (fun B s => scaledRoughDensity c z H B s)
         (fun s => ((4 : ℝ) ^ (-z) *
           (Real.exp (-Real.eulerMascheroniConstant * z) / Real.Gamma z)) * s ^ (z - 1))
         atTop (Set.Ici δ) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.scaledRoughDensity