OAI/NumberTheory/JointDickman/Amplification/GeometricPeriodLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The original separated Fourier expression and the retained full-arc model

  1. def OAI.JointDickman.geometricPeriodSum line 11
  2. theorem OAI.JointDickman.geometric_period_split line 16
  3. theorem OAI.JointDickman.geometric_period_model_vanishing line 39