OAI/NumberTheory/JointDickman/Amplification/ShrinkingDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.scaledRoughCoefficient_weighted_succ_tendsto line 13

   Source documentation

   The higher coefficients still vanish after the loss at s=B^(-1/10).

   theorem scaledRoughCoefficient_weighted_succ_tendsto
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (c : ℕ → ℝ) {z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) (j : ℕ) :
       Tendsto (fun B => scaledRoughCoefficient c z (j + 1) B *
         (B : ℝ) ^ ((j + 1 : ℕ) / 10 : ℝ)) atTop (𝓝 0) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.scaledRoughCoefficient

2. def OAI.JointDickman.shrinkingDensityError line 57
3. theorem OAI.JointDickman.shrinkingDensityError_tendsto line 63
4. theorem OAI.JointDickman.scaledRoughDensity_ratio line 115
5. theorem OAI.JointDickman.scaledRoughDensity_ratio_error line 135

   Source documentation

   The relative error is small uniformly down to s=B^(-1/10).

   theorem scaledRoughDensity_ratio_error (c : ℕ → ℝ) (z k : ℝ) (H B : ℕ)
       (hB : 0 < B) {s : ℝ} (hs : (B : ℝ) ^ (-(1 / 10 : ℝ)) ≤ s) :
       |scaledRoughDensity c z H B s / s ^ (z - 1) - k| ≤ shrinkingDensityError c z k H B := by
   …

   Mentions: OAI.JointDickman.scaledRoughDensity, OAI.JointDickman.shrinkingDensityError

6. theorem OAI.JointDickman.scaledRoughDensity_shrinking_bounds line 165

   Source documentation

   Positivity and the singular power bound hold all the way down to the moving lower boundary, uniformly in the scale.

   theorem scaledRoughDensity_shrinking_bounds
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput)
       (c : ℕ → ℝ) {z : ℝ} (hc : c 0 = squarefreeLeadingConstant z)
       (hz : 0 < z) (hzhalf : z ≤ 1 / 2) (H : ℕ) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ s : ℝ,
         (B : ℝ) ^ (-(1 / 10 : ℝ)) ≤ s →
         0 < scaledRoughDensity c z H B s ∧
           scaledRoughDensity c z H B s ≤ K * s ^ (z - 1) := by
   …

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