OAI/NumberTheory/JointDickman/Amplification/ArithmeticPatternMeans.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

First-digit pattern averages over the full prime-square period

  1. theorem OAI.JointDickman.residuePrimePatterns_mean line 11
  2. theorem OAI.JointDickman.arithmeticSquareMean_patterns line 23
  3. theorem OAI.JointDickman.arithmeticSquareMean_pattern_comparison line 35
  4. theorem OAI.JointDickman.arithmeticSquareMean_add line 49
  5. theorem OAI.JointDickman.arithmeticSquareMean_const_mul line 53
  6. theorem OAI.JointDickman.arithmeticSquareMean_mono line 57