OAI/NumberTheory/JointDickman/Arithmetic/PeriodicConvolutionSmoothing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Smoothing a periodic lag factor along its residue class

  1. def OAI.JointDickman.residueSmoothed line 9
  2. theorem OAI.JointDickman.norm_sub_average_le line 12
  3. theorem OAI.JointDickman.periodicConvolution_smoothing line 28