OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkPatternIntegralReplacementBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Arithmetic.HistoryBulkPatternIntegralReplacement.Reference line 23
2. def OAI.Ostmann.Arithmetic.HistoryBulkPatternIntegralReplacement.Reference.weight line 37
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkPatternIntegralReplacement.Reference.weight_norm_le line 43
4. abbrev OAI.Ostmann.Arithmetic.HistoryBulkPatternIntegralReplacement.Family line 57
5. def OAI.Ostmann.Arithmetic.HistoryBulkPatternIntegralReplacement.familyValue line 61
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkPatternIntegralReplacement.familyValue_sub_norm_le line 70