OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightPositiveSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.AllPivots line 11
2. def OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.AllPivotCells line 18
3. def OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.AllPivotsPositive line 21
4. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.AllPivots.mono line 24
5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.AllPivotCells.positive line 32
6. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotCells_of_support_ne_zero line 37
7. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotCells_of_realHistoryScalar_ne_zero line 51
8. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.allPivotsPositive_of_realHistoryScalar_ne_zero line 58
9. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.realHistoryScalar_eq_zero_of_not_allPivotCells line 64
10. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.realHistoryScalar_eq_zero_of_not_allPivotsPositive line 71