OAI/NumberTheory/JointDickman/Amplification/FullModelLinearity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linearity in the scalar weight of each geometric box

  1. theorem OAI.JointDickman.fullSmallMajorArcModel_mul line 11
  2. def OAI.JointDickman.weightedGeometricPeriodSum line 36
  3. def OAI.JointDickman.weightedGeometricSmallArcSum line 42
  4. theorem OAI.JointDickman.weightedGeometricSmallArcSum_sub_model line 48