OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantWeightedPriorReplacementBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.primeTest_weightedResidueTest line 14
2. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.mixedTest_weightedResidueTest line 21
3. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.norm_actual_weightedResidueTest_le line 28
4. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.sum_norm_primeTest_weighted_le line 38
5. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.sum_norm_mixedTest_weighted_le line 50
6. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.weightedResidueTest_one line 66
7. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.periodicSourcePrimeMean_unweighted line 74
8. theorem OAI.Ostmann.Arithmetic.HistoryGiantWeightedPriorReplacement.periodicSourceMixedMean_unweighted line 81