OAI/NumberTheory/JointDickman/Counting/CountingCutoffError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact error when the finite counting cutoff is replaced by its ramp

  1. def OAI.JointDickman.smoothCandidateCutoff line 10
  2. theorem OAI.JointDickman.smoothCandidateCutoff_nonneg line 13
  3. theorem OAI.JointDickman.finiteCandidateCutoff_ramp_error line 19
  4. theorem OAI.JointDickman.candidateSiteKernel_cutoff_error line 44