OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.realHistorySupportWeight line 14
2. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.realHistorySupportWeight_bounds line 23
3. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.realHistoryScalar_eq_zero_of_support_zero line 39
4. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.realHistorySupportWeight_ne_zero_of_scalar_ne_zero line 54
5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.logCurve_contDiff line 60
6. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.encode_realHistoryScalar_logCurve_differentiableAt line 67