OAI/NumberTheory/Ostmann/Arithmetic/HistoryActualComparisonDecayArithmetic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.nat_mul_exp_reserve_le line 10
2. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.five_stage_exp_le line 16
3. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.five_stage_bulk_exp_le line 36
4. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.five_stage_exp_le_of_steps line 52
5. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.two_terms_exp_67_65_le line 58
6. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.two_norms_exp_67_65_le line 70
7. theorem OAI.Ostmann.Arithmetic.HistoryActualComparisonDecayArithmetic.norm_add_exp_67_65_le line 76