OAI/NumberTheory/Ostmann/Characters/TemplateSourceAmplitude.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceAmplitudeSequence line 21
2. abbrev OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.SourceTransferBounds line 29
3. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceAmplitudeSequence_eq line 37
4. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourceUnitDiagonal_eq_scheduled line 48
5. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.eventually_sourceAmplitudeSequence_zero line 59