OAI/NumberTheory/JointDickman/Arithmetic/AmplificationSmoothCutoff.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth cutoff equal to one on the positive interior rectangle

  1. def OAI.JointDickman.amplificationBump line 11
  2. theorem OAI.JointDickman.amplificationBump_bounds line 17
  3. theorem OAI.JointDickman.amplificationBump_one line 20
  4. theorem OAI.JointDickman.amplificationBump_zero line 27
  5. theorem OAI.JointDickman.amplificationBump_support line 37
  6. theorem OAI.JointDickman.amplificationBump_contDiff line 44
  7. theorem OAI.JointDickman.amplificationBump_compactSupport line 47
  8. def OAI.JointDickman.amplificationSmoothWeight line 50
  9. theorem OAI.JointDickman.amplificationSmoothWeight_bounds line 53
  10. theorem OAI.JointDickman.amplificationSmoothWeight_one line 59
  11. theorem OAI.JointDickman.amplificationSmoothWeight_one_on_interior line 86
  12. theorem OAI.JointDickman.amplificationSmoothWeight_support line 94