OAI/NumberTheory/JointDickman/Amplification/WeightedCandidateProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Product-dependent cutoffs in the exact candidate mean

  1. def OAI.JointDickman.weightedCandidateRetained line 9
  2. theorem OAI.JointDickman.weightedCandidateRetained_mean line 14
  3. def OAI.JointDickman.weightedAmplificationArithmeticSum line 52
  4. def OAI.JointDickman.weightedRegularizedArithmeticSum line 58
  5. theorem OAI.JointDickman.weightedRegularizedArithmeticSum_eq_product line 65
  6. theorem OAI.JointDickman.weighted_amplification_regularization_error line 91