OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightSourceXi.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.sourceXiConstant line 10
2. theorem OAI.Ostmann.Arithmetic.sourceLeafAmplitude_pair line 13
3. structure OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.SourceDomain line 29
4. def OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualRealXi line 36
5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualRealXi_norm_le line 43
6. theorem OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.actualRealXi_counterpart_norm_le line 63