OAI/NumberTheory/JointDickman/Counting/CountingSlowMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

From the periodic sampling error to the moving counting scale

  1. def OAI.JointDickman.countingArithmeticCutError line 12
  2. theorem OAI.JointDickman.arithmeticSiteCutMean_period_bound line 18
  3. theorem OAI.JointDickman.blockPatternEquiv_arithmetic_modEq line 34
  4. theorem OAI.JointDickman.counting_slow_mean line 43