OAI/NumberTheory/Ostmann/Construction/EnumeratedSchedulePhase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual pivot phase in the enumeration used by the harmonic prior

  1. def OAI.Ostmann.enumeratedPartitionEquiv line 11
  2. theorem OAI.Ostmann.enumeratedPartitionEquiv_pivot line 17
  3. theorem OAI.Ostmann.enumeratedPartitionEquiv_rest line 21
  4. theorem OAI.Ostmann.scheduledPrimePhase_factor_enumerated line 27