OAI/NumberTheory/JointDickman/Counting/GraphLagMajorant.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An actual lag mass is dominated by a finite sum of periodic means

  1. def OAI.JointDickman.arithmeticLagMass line 12
  2. def OAI.JointDickman.graphLagMajorant line 16
  3. theorem OAI.JointDickman.arithmeticLagMass_supported line 23
  4. theorem OAI.JointDickman.arithmeticLagMass_le_majorant line 52
  5. def OAI.JointDickman.graphLagMean line 77
  6. theorem OAI.JointDickman.graphLagMajorant_tendsto line 83