OAI/NumberTheory/JointDickman/Amplification/AdditivePhaseVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite partial summation for a nearby additive frequency

  1. lemma OAI.JointDickman.additivePhase_sub_one_norm_le line 10
  2. lemma OAI.JointDickman.additivePhase_difference_norm_le line 21
  3. lemma OAI.JointDickman.bounded_partial_sums_weighted line 31