OAI/NumberTheory/JointDickman/Amplification/RampedCandidate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual candidate cutoff and its ramped arithmetic counterpart

  1. def OAI.JointDickman.rampedCandidateCutoff line 10
  2. def OAI.JointDickman.rampedProductCutoff line 15
  3. theorem OAI.JointDickman.rampedProductCutoff_bounds line 18
  4. theorem OAI.JointDickman.candidateSiteKernel_pair_cutoff_congr line 23
  5. theorem OAI.JointDickman.rampedCandidateCutoff_pair line 34
  6. theorem OAI.JointDickman.rampedCandidateCutoff_bounds line 42
  7. theorem OAI.JointDickman.rampedArithmetic_eq_weighted line 60