OAI/Dynamics/EntropyCounterexample/RadialOrbitRepresentation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.RadialOrbit.direction line 14
  2. theorem OAI.Problem340.RadialOrbit.norm_direction line 18
  3. theorem OAI.Problem340.RadialOrbit.norm_smul_direction line 24
  4. def OAI.Problem340.RadialOrbit.radialMap line 29
  5. theorem OAI.Problem340.RadialOrbit.radialMap_zero line 31
  6. theorem OAI.Problem340.RadialOrbit.radialMap_polar line 34
  7. theorem OAI.Problem340.RadialOrbit.iterate_radialMap_polar line 43
  8. theorem OAI.Problem340.RadialOrbit.iterate_radialMap_eq line 53
  9. def OAI.Problem340.RadialOrbit.polarMap line 60
  10. theorem OAI.Problem340.RadialOrbit.continuous_polarMap line 63
  11. theorem OAI.Problem340.RadialOrbit.range_polarMap line 67
  12. theorem OAI.Problem340.RadialOrbit.polarMap_semiconj line 83
  13. def OAI.Problem340.RadialOrbit.polarMapPi line 92
  14. theorem OAI.Problem340.RadialOrbit.continuous_polarMapPi line 96
  15. theorem OAI.Problem340.RadialOrbit.range_polarMapPi line 101
  16. theorem OAI.Problem340.RadialOrbit.polarMapPi_semiconj line 120
  17. theorem OAI.Problem340.RadialOrbit.complex_polar_representation line 130