OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkPrincipalBSquareReplacementDensityBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.DensitySources line 22
2. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.densityFactor line 28
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.norm_densityFactor_le line 33
4. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.densityAmplitude line 39
5. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.densityBErrorSum line 45
6. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.densityPatternFactor line 56
7. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.densityBExpressionSum line 65
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalBSquareReplacement.densityBExpressionSum_sub line 75