OAI/NumberTheory/JointDickman/Probability/AmplificationTensorProfile.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual amplification weight in normalized geometric-box coordinates

  1. def OAI.JointDickman.amplificationSpatialProfile line 12
  2. def OAI.JointDickman.amplificationTensorProfile line 15
  3. def OAI.JointDickman.amplificationBoxWeight line 18
  4. theorem OAI.JointDickman.amplificationTensorProfile_continuous line 21
  5. theorem OAI.JointDickman.amplificationSpatialProfile_bounds line 34
  6. theorem OAI.JointDickman.amplificationSpatialProfile_support line 42
  7. theorem OAI.JointDickman.amplificationSpatialProfile_cutoff line 71
  8. theorem OAI.JointDickman.amplificationTensorProfile_cutoff line 78
  9. theorem OAI.JointDickman.amplificationBump_lipschitz line 85
  10. theorem OAI.JointDickman.amplificationBoxWeight_freezing line 100