OAI/Dynamics/StandardMap/CurveCharts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.StandardMapEntropy.CurveInterval line 11
2. def OAI.StandardMapEntropy.CurveInterval.length line 18
3. def OAI.StandardMapEntropy.CurveInterval.parameter line 19
4. lemma OAI.StandardMapEntropy.CurveInterval.length_nonneg line 20
5. lemma OAI.StandardMapEntropy.CurveInterval.length_le_one line 21
6. lemma OAI.StandardMapEntropy.CurveInterval.parameter_mem line 22
7. lemma OAI.StandardMapEntropy.CurveInterval.parameter_range line 24
8. lemma OAI.StandardMapEntropy.CurveInterval.parameter_sub line 26
9. lemma OAI.StandardMapEntropy.CurveInterval.parameter_abs_sub line 28
10. def OAI.StandardMapEntropy.CurveInterval.velocity line 31
11. lemma OAI.StandardMapEntropy.CurveInterval.velocity_norm line 32
12. lemma OAI.StandardMapEntropy.CurveInterval.velocity_continuous line 35
13. lemma OAI.StandardMapEntropy.CurveInterval.hasDeriv line 39
14. lemma OAI.StandardMapEntropy.CurveInterval.variation line 42
15. lemma OAI.StandardMapEntropy.curve_compact_hull line 53