OAI/Geometry/IsometricImmersion/Energy/SqrtEnergyGronwall.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Hyperbolic.regularized_sqrt_rate_le line 12
  2. def OAI.SmoothLocal.Hyperbolic.regularizedWeightedEnergy line 30
  3. def OAI.SmoothLocal.Hyperbolic.regularizedWeightedRate line 33
  4. theorem OAI.SmoothLocal.Hyperbolic.regularizedWeightedEnergy_hasDerivAt line 37
  5. theorem OAI.SmoothLocal.Hyperbolic.regularizedWeightedRate_le line 51
  6. theorem OAI.SmoothLocal.Hyperbolic.regularized_sqrt_energy_gronwall line 65
  7. theorem OAI.SmoothLocal.Hyperbolic.sqrt_energy_gronwall line 97