OAI/NumberTheory/JointDickman/Amplification/MultiplicityMargins.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.largeMultiplicityLoss_tendsto line 12
2. theorem OAI.JointDickman.exists_common_multiplicity_tolerance line 21

   Source documentation

   A common arbitrarily small positive tolerance preserves both the small-addition exponent and the large-addition margin.

   theorem exists_common_multiplicity_tolerance {L : ℕ} (hL : 10000 ≤ L)
       {cap : ℝ} (hcap : 0 < cap) :
       ∃ τ : ℝ, 0 < τ ∧ τ ≤ cap ∧ τ ≤ samplingTau ∧
         smallMultiplicityExponent L τ < 8/1000 ∧
         largeMultiplicityLoss (1/(L : ℝ)) (1/200) τ (1/1000) < 4/100 := by
   …

   Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.smallMultiplicityExponent, OAI.JointDickman.largeMultiplicityLoss

3. theorem OAI.JointDickman.log_add_one_cube_div_rpow_tendsto line 47

   Source documentation

   Every fixed logarithmic polynomial is negligible compared to the strict power saving in the large-class estimate.

   theorem log_add_one_cube_div_rpow_tendsto {c : ℝ} (hc : 0 < c) :
       Tendsto (fun B : ℝ => (Real.log B+1)^3/B^c) atTop (𝓝 0) := by
   …