OAI/NumberTheory/TotientAsymptotic/WeightPerturbation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.one_sub_prod_le_sum line 9
2. lemma OAI.TotientAsymptotic.min_one_lipschitz line 25
3. lemma OAI.TotientAsymptotic.fk_reciprocal_lipschitz line 31

   Source documentation

   A bounded additive perturbation is valid even when the original weight vanishes, including the boundary r=k.

   lemma fk_reciprocal_lipschitz (k : ℕ) {r q : ℝ} (hr : 1 ≤ r)
       (_hq : 0 < q) (hq1 : q ≤ 1) :
       |fk k (r/q)-fk k r| ≤ (2*(k : ℝ)+1)*(1-q) := by
   …

   Mentions: OAI.TotientAsymptotic.fk