OAI/NumberTheory/Ostmann/Characters/TemplateAmplitudePriorDefs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.Template.constituentPrimePrior line 15
  2. def OAI.Ostmann.Characters.Template.copiedPrimePrior line 20
  3. def OAI.Ostmann.Characters.Template.outsidePrimePrior line 26
  4. def OAI.Ostmann.Characters.Template.pivotPrimePrior line 32
  5. def OAI.Ostmann.Characters.Template.constituentSampleState line 39
  6. def OAI.Ostmann.Characters.Template.copiedSampleState line 43
  7. def OAI.Ostmann.Characters.Template.outsideSampleState line 48
  8. def OAI.Ostmann.Characters.Template.scheduledSample line 53
  9. def OAI.Ostmann.Characters.Template.copyPairInputEquiv line 60
  10. def OAI.Ostmann.Characters.Template.nextSampleEquiv line 71
  11. def OAI.Ostmann.Characters.Template.nextPrimeShells line 76
  12. theorem OAI.Ostmann.Characters.Template.nextPrimeShells_positive line 83
  13. def OAI.Ostmann.Characters.Template.nextSample line 90