OAI/NumberTheory/JointDickman/Arithmetic/RoughErrorLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Decay of the roughness-cutoff errors

The exponential Rankin error absorbs every fixed power of the scale and of its logarithm. This is the limit needed after the explicit moving-cutoff expansion.

  1. theorem OAI.JointDickman.rough_exponential_error_tendsto line 18