OAI/NumberTheory/Ostmann/Characters/TemplateAmplitudePriorSources.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.Template.previousConstituent line 12
  2. theorem OAI.Ostmann.Characters.Template.previousConstituent_copied line 18
  3. theorem OAI.Ostmann.Characters.Template.previousConstituent_outside line 24
  4. theorem OAI.Ostmann.Characters.Template.nextPrimeShells_eq_previous line 30
  5. def OAI.Ostmann.Characters.Template.scheduledConstituentOrigin line 38
  6. def OAI.Ostmann.Characters.Template.scheduledPrimeShells line 44
  7. theorem OAI.Ostmann.Characters.Template.scheduledPrimeShells_succ line 50
  8. theorem OAI.Ostmann.Characters.Template.scheduledPrimeShells_eq_origin line 55
  9. theorem OAI.Ostmann.Characters.Template.scheduledPrimeShells_positive line 65
  10. def OAI.Ostmann.Characters.Template.scheduledPrimePrior line 73
  11. theorem OAI.Ostmann.Characters.Template.scheduledPrimePrior_succ_cmean line 80