OAI/NumberTheory/JointDickman/Amplification/GraphPairMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A periodic upper bound for each actual graph representation

  1. theorem OAI.JointDickman.graphResidueEnvelope_nonneg line 11
  2. theorem OAI.JointDickman.graphEdgeEnvelope_nonneg line 21
  3. theorem OAI.JointDickman.graphPair_mass_le_prefix line 29
  4. theorem OAI.JointDickman.mean_scaled_multiple line 70
  5. theorem OAI.JointDickman.graphPair_majorant_tendsto line 85