OAI/Geometry/WeakMTW/Coordinates/FanCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFan line 23
2. def OAI.WeakMTWGlobalSupport.WeakMTW.fanCoordinates line 26
3. def OAI.WeakMTWGlobalSupport.WeakMTW.fanDomain line 29
4. def OAI.WeakMTWGlobalSupport.WeakMTW.fanMomentum line 32
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFan_smooth line 36
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanDomain_open line 45
7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanCoordinates_smooth line 49
8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanCoordinates_ode line 59
9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanCoordinates_energy line 68
10. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanMomentum_coord line 80