OAI/NumberTheory/JointDickman/Amplification/RegularizedProductWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The coefficient-regularized product weight in the candidate mean

  1. def OAI.JointDickman.regularizedProductWeight line 12
  2. theorem OAI.JointDickman.regularizedProductWeight_bounds line 18
  3. theorem OAI.JointDickman.candidateRetainedWeight_eq_product line 33