OAI/NumberTheory/JointDickman/Amplification/WeightedCandidateComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform removal errors with the actual bounded counting restriction

  1. theorem OAI.JointDickman.weightedCandidateRetained_bounds line 12
  2. theorem OAI.JointDickman.weighted_candidate_remainder_removal line 21
  3. theorem OAI.JointDickman.weighted_candidate_coefficient_removal line 68