OAI/NumberTheory/JointDickman/Counting/InteriorAmplificationWindows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Positive coefficient windows strictly inside the smooth cutoff support

  1. def OAI.JointDickman.amplificationInteriorC line 11
  2. def OAI.JointDickman.amplificationInteriorA line 14
  3. theorem OAI.JointDickman.amplificationInteriorC_bounds line 17
  4. theorem OAI.JointDickman.amplificationInteriorC_subset line 23
  5. theorem OAI.JointDickman.amplificationInteriorA_subset line 32
  6. theorem OAI.JointDickman.amplificationInteriorPair_mem line 44
  7. theorem OAI.JointDickman.amplification_interior_row_mass_lower line 49