OAI/NumberTheory/Ostmann/Conclusion/ScaleReserves.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Conclusion.diagonalExponent line 10
2. theorem OAI.Ostmann.Conclusion.diagonalExponent_eq line 15
3. theorem OAI.Ostmann.Conclusion.bulkScale_one_le line 22

   Distinct definitions of this name: OAI/NumberTheory/Ostmann/Conclusion/FinalRateAbsorptionBasic.lean:9 (different declaration text). Qualify references as OAI.Ostmann.Conclusion.bulkScale_one_le@path.

4. theorem OAI.Ostmann.Conclusion.diagonalExponent_reserve line 25
5. theorem OAI.Ostmann.Conclusion.exp_pair_le line 39
6. theorem OAI.Ostmann.Conclusion.diagonal_total_reserve line 46
7. theorem OAI.Ostmann.Conclusion.giant_cost_reserve line 56