OAI/Geometry/IsometricImmersion/Flows/HeightFlowUniformBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.flowRhoJetBound line 13
  2. def OAI.SmoothLocal.Flow.heightG1JetBound line 15
  3. def OAI.SmoothLocal.Flow.heightBJetBound line 18
  4. def OAI.SmoothLocal.Flow.heightG1Lower line 21
  5. def OAI.SmoothLocal.Flow.heightRemainderBound line 24
  6. theorem OAI.SmoothLocal.Flow.heightG1Lower_pos line 32
  7. theorem OAI.SmoothLocal.Flow.exists_height_flow_uniform_coefficients line 39