OAI/NumberTheory/JointDickman/Analysis/FairLaplaceFeature.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fair-split Laplace features are finite-prime multiplicative weights

  1. def OAI.JointDickman.primeLaplaceFeature line 12
  2. theorem OAI.JointDickman.retainedPrimeProduct_rpow line 15
  3. theorem OAI.JointDickman.fairSplitAverage_laplace line 29
  4. theorem OAI.JointDickman.primeLaplaceFeature_at_integer line 46
  5. theorem OAI.JointDickman.primeLaplaceWeight_bounds line 53
  6. theorem OAI.JointDickman.fairSplitAverage_laplace_sum line 61