OAI/NumberTheory/JointDickman/Counting/AmplificationWindows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A positive rectangle inside the coefficient size-and-ratio support

  1. def OAI.JointDickman.amplificationLowerC line 13
  2. def OAI.JointDickman.amplificationLowerA line 16
  3. theorem OAI.JointDickman.amplificationLowerC_bounds line 19
  4. theorem OAI.JointDickman.amplificationLowerPair_mem line 25
  5. theorem OAI.JointDickman.amplificationWindow_log_bounds line 42
  6. theorem OAI.JointDickman.amplification_window_mass_lower line 80