OAI/NumberTheory/JointDickman/Counting/CoefficientProfileFreeze.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Freezing the slowly varying coefficient density inside one box

  1. def OAI.JointDickman.testFourierTransform line 12
  2. theorem OAI.JointDickman.compact_weighted_phase_integral line 15
  3. theorem OAI.JointDickman.coefficientDensity_log_difference line 30
  4. theorem OAI.JointDickman.coefficientFourier_freeze_bound line 44