OAI/NumberTheory/JointDickman/Counting/FrozenCoefficientLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The published coefficient law with a fixed smooth Fourier profile

  1. theorem OAI.JointDickman.moebius_totient_complex_norm_le_one line 11
  2. theorem OAI.JointDickman.coefficient_frozen_majorArc_law line 22