OAI/NumberTheory/TotientAsymptotic/FiniteDyadicPowerMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal mass of a finite set with a logarithmic power saving in its count.

  1. lemma OAI.TotientAsymptotic.finite_dyadic_power_mass line 11
  2. lemma OAI.TotientAsymptotic.finite_dyadic_log_power_tail line 42