OAI/Geometry/IsometricImmersion/Flows/FlowTransport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.capPullback line 14
  2. def OAI.SmoothLocal.Flow.capChartSigma line 16
  3. def OAI.SmoothLocal.Flow.capTransportA line 20
  4. def OAI.SmoothLocal.Flow.capTransportC line 23
  5. def OAI.SmoothLocal.Flow.driftOperator line 26
  6. theorem OAI.SmoothLocal.Flow.capChart_partial line 32
  7. theorem OAI.SmoothLocal.Flow.capPullback_contDiffOn line 51
  8. theorem OAI.SmoothLocal.Flow.capPullback_partial line 57
  9. theorem OAI.SmoothLocal.Flow.capPullback_partial_initial line 71
  10. theorem OAI.SmoothLocal.Flow.capPullback_partial_time line 79
  11. theorem OAI.SmoothLocal.Flow.capPullback_original_y line 89
  12. theorem OAI.SmoothLocal.Flow.capPullback_second_initial_forward line 97
  13. theorem OAI.SmoothLocal.Flow.capPullback_original_yy line 123
  14. theorem OAI.SmoothLocal.Flow.coordinateDrift_contDiffOn line 138
  15. theorem OAI.SmoothLocal.Flow.capPullback_drift_twice line 143
  16. theorem OAI.SmoothLocal.Flow.capChartRho_partial_initial line 163
  17. theorem OAI.SmoothLocal.Flow.capChartSigma_eq_rho_partial line 177
  18. theorem OAI.SmoothLocal.Flow.capChartSigma_contDiffOn line 186
  19. theorem OAI.SmoothLocal.Flow.capTransportA_partial_initial line 194
  20. theorem OAI.SmoothLocal.Flow.cap_driftOperator_transport line 221