OAI/NumberTheory/JointDickman/Amplification/WeightedPeriodLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.JointDickman.weighted_geometric_period_split line 12
  2. theorem OAI.JointDickman.weighted_geometric_period_model_vanishing line 35