OAI/NumberTheory/JointDickman/Amplification/RampDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded Lipschitz densities after the lower ramp cutoff

  1. def OAI.JointDickman.rampDensity line 12
  2. theorem OAI.JointDickman.rampDensity_zero line 15
  3. theorem OAI.JointDickman.rampDensity_eq line 19
  4. theorem OAI.JointDickman.rampDensity_bound line 23
  5. theorem OAI.JointDickman.clampedDensity_lipschitz line 31
  6. theorem OAI.JointDickman.rampDensity_lipschitz line 42