OAI/NumberTheory/JointDickman/Amplification/MonotoneSumComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Decreasing weights preserve domination of partial sums

  1. lemma OAI.JointDickman.antitone_weighted_sum_nonpos line 9
  2. lemma OAI.JointDickman.antitone_weighted_sum_le line 26