OAI/Geometry/IsometricImmersion/Flows/FlowHeightCoefficients.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.heightOriginalA line 12
  2. def OAI.SmoothLocal.Flow.heightOriginalB line 15
  3. def OAI.SmoothLocal.Flow.heightOriginalC0 line 18
  4. def OAI.SmoothLocal.Flow.heightChartA line 23
  5. def OAI.SmoothLocal.Flow.heightChartB line 26
  6. def OAI.SmoothLocal.Flow.heightChartC line 29
  7. def OAI.SmoothLocal.Flow.heightChartG1 line 32
  8. def OAI.SmoothLocal.Flow.heightChartRemainder line 35
  9. theorem OAI.SmoothLocal.Flow.heightOriginalA_contDiffOn line 43
  10. theorem OAI.SmoothLocal.Flow.heightOriginalA_partial_y line 48
  11. theorem OAI.SmoothLocal.Flow.heightOriginalC0_eq line 57
  12. theorem OAI.SmoothLocal.Flow.heightChartA_eq line 69
  13. theorem OAI.SmoothLocal.Flow.heightChartG1_pos line 74
  14. theorem OAI.SmoothLocal.Flow.heightChartA_partial_initial line 82
  15. theorem OAI.SmoothLocal.Flow.heightChartC_expanded line 100
  16. theorem OAI.SmoothLocal.Flow.heightChartC_factor line 116
  17. theorem OAI.SmoothLocal.Flow.heightChartA_contDiffOn line 134
  18. theorem OAI.SmoothLocal.Flow.heightChartRemainder_contDiffOn line 144
  19. theorem OAI.SmoothLocal.Flow.heightChartC_contDiffOn line 163
  20. theorem OAI.SmoothLocal.Flow.heightChartRemainder_bounded_on_compact line 176
  21. theorem OAI.SmoothLocal.Flow.height_coefficient_operator_transport line 193