OAI/NumberTheory/Ostmann/Characters/TemplateAmplitudeRecurrenceAmplitude.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Characters.Template.PrimeCharacterData line 16
2. abbrev OAI.Ostmann.Characters.Template.PrimeTranslationData line 19
3. def OAI.Ostmann.Characters.Template.sampledHistoryPhase line 22
4. def OAI.Ostmann.Characters.Template.samplePrimeSupport line 31
5. def OAI.Ostmann.Characters.Template.amplitudeIntegrand line 35
6. def OAI.Ostmann.Characters.Template.actualAmplitude line 50
7. theorem OAI.Ostmann.Characters.Template.actualAmplitude_disintegration line 62
8. theorem OAI.Ostmann.Characters.Template.sampledHistoryPhase_zero line 79