OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightDerivConstants.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.partitionDerivativeConstant line 10
2. theorem OAI.Ostmann.Arithmetic.partitionDerivativeConstant_pos line 12
3. theorem OAI.Ostmann.Arithmetic.partition_deriv_le_constant line 15
4. def OAI.Ostmann.Arithmetic.cellDerivativeConstant line 18
5. theorem OAI.Ostmann.Arithmetic.cellDerivativeConstant_pos line 20
6. theorem OAI.Ostmann.Arithmetic.cell_deriv_le_constant line 23
7. def OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualSourceDerivativeRate line 32
8. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualSourceDerivativeRate_nonneg line 35
9. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.cellDerivativeConstant_mul_le_rate line 39