OAI/NumberTheory/TotientAsymptotic/MovingSmoothDyadic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A moving smoothness condition on a totient transfers to its dyadic slice.

  1. lemma OAI.TotientAsymptotic.B_mono line 10
  2. lemma OAI.TotientAsymptotic.relative_smooth_at_dyadic line 13