OAI/NumberTheory/JointDickman/Arithmetic/RoughDensityDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Derivatives of the density used in partial summation

The finite model is differentiated directly, and its first derivative converges uniformly away from zero along with the density itself.

  1. def OAI.JointDickman.scaledRoughDensityDeriv line 17
  2. theorem OAI.JointDickman.hasDerivAt_scaledRoughDensity line 22
  3. theorem OAI.JointDickman.hasDerivAt_logarithmic_model line 43
  4. theorem OAI.JointDickman.scaledRoughDensityDeriv_tendstoUniformlyOn line 67