OAI/NumberTheory/JointDickman/Arithmetic/RoughDensityRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform boundedness and Lipschitz control of the actual density

These estimates provide the profile hypotheses in the coarse channel. Their constants are independent of the auxiliary integer B.

  1. theorem OAI.JointDickman.uniform_power_eventually_bounded line 18
  2. theorem OAI.JointDickman.scaledRoughDensity_bounded_lipschitz line 36