OAI/NumberTheory/JointDickman/Probability/FixedResidueReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Dividing a residue class and its averaging interval by a fixed divisor

  1. def OAI.JointDickman.residueBinAverage line 10
  2. theorem OAI.JointDickman.residueBinAverage_unit line 16
  3. theorem OAI.JointDickman.natCast_fixed_residue_iff line 21
  4. theorem OAI.JointDickman.sum_fixed_residue line 36
  5. theorem OAI.JointDickman.residueBinAverage_dilate line 50
  6. theorem OAI.JointDickman.residueBinAverage_fixed_divisor line 79