OAI/NumberTheory/Ostmann/Construction/Coefficient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.outsideProduct line 9
2. def OAI.Ostmann.Construction.modFraction line 11
3. def OAI.Ostmann.Construction.baseCoefficient line 14
4. def OAI.Ostmann.Construction.History.internalMass line 24
5. theorem OAI.Ostmann.Construction.History.internalMass_eq_occurrences line 30
6. theorem OAI.Ostmann.Construction.History.internalMass_nonneg line 40
7. def OAI.Ostmann.Construction.coefficient line 51
8. def OAI.Ostmann.Construction.regularTransform line 58
9. def OAI.Ostmann.Construction.amplitude line 66
10. theorem OAI.Ostmann.Construction.coefficient_empty line 71