OAI/NumberTheory/TotientAsymptotic/TerminalStateCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact multiplicity bounds for the final smooth factor states.

  1. def OAI.TotientAsymptotic.terminalRight line 13
  2. lemma OAI.TotientAsymptotic.terminalRight_product line 16
  3. lemma OAI.TotientAsymptotic.terminal_state_encoding_injective line 20
  4. lemma OAI.TotientAsymptotic.terminal_state_card_le line 36