OAI/NumberTheory/JointDickman/Arithmetic/MovingPrimeIndependence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact independence from every fixed residue coordinate

  1. theorem OAI.JointDickman.auxiliarySquarePeriod_eventually_coprime line 11
  2. theorem OAI.JointDickman.residueAmplification_mean line 24
  3. theorem OAI.JointDickman.fixed_residue_amplification_average line 30
  4. theorem OAI.JointDickman.eventually_fixed_residue_amplification_average line 49