OAI/NumberTheory/TotientAsymptotic/FordDimensionScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary lower bounds for the dimension and volume normalization.

  1. lemma OAI.TotientAsymptotic.dimension_exponential_lower line 14
  2. lemma OAI.TotientAsymptotic.central_volume_one_le line 34
  3. lemma OAI.TotientAsymptotic.dimension_row_model_budget line 48