OAI/NumberTheory/JointDickman/Counting/ShortLagRemoval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Short additive lags have a uniformly small total contribution

  1. theorem OAI.JointDickman.arithmetic_short_lags_bound line 11
  2. theorem OAI.JointDickman.graph_energy_eq_lag_correlations line 39
  3. def OAI.JointDickman.graphEnergyWithoutShortLags line 48
  4. theorem OAI.JointDickman.graph_short_lag_removal_identity line 52
  5. theorem OAI.JointDickman.arithmetic_short_lags_removable line 67