OAI/Dynamics/StandardMap/CurveColumns.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.complexPair line 11
2. lemma OAI.StandardMapEntropy.complexPair_norm line 12
3. lemma OAI.StandardMapEntropy.complexPair_transfer line 20
4. lemma OAI.StandardMapEntropy.curveIterVelocity_transfer line 22
5. lemma OAI.StandardMapEntropy.complex_operator_columns line 36
6. def OAI.StandardMapEntropy.horizontalVelocity line 49
7. def OAI.StandardMapEntropy.verticalVelocity line 51
8. lemma OAI.StandardMapEntropy.horizontalVelocity_eq line 53
9. lemma OAI.StandardMapEntropy.verticalVelocity_eq line 56
10. lemma OAI.StandardMapEntropy.liftTransfer_columns_bound line 59
11. lemma OAI.StandardMapEntropy.continuous_horizontalVelocity line 64
12. lemma OAI.StandardMapEntropy.continuous_verticalVelocity line 73