OAI/NumberTheory/Ostmann/Conclusion/TransferRecurrence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Conclusion.transferBudget line 10
2. theorem OAI.Ostmann.Conclusion.transferBudget_zero line 13
3. theorem OAI.Ostmann.Conclusion.transferBudget_succ line 16
4. theorem OAI.Ostmann.Conclusion.transferBudget_lt line 22
5. theorem OAI.Ostmann.Conclusion.exp_half_square line 31
6. theorem OAI.Ostmann.Conclusion.transfer_step line 39
7. theorem OAI.Ostmann.Conclusion.transfer_exact_lower line 61
8. theorem OAI.Ostmann.Conclusion.transfer_exact_log line 85
9. theorem OAI.Ostmann.Conclusion.incompatible_final_rates line 94