OAI/Geometry/WeakHessian/LocalBounds/Law.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.lawAt line 57
  2. lemma OAI.WeakHessian.lawAt_coe line 61
  3. lemma OAI.WeakHessian.continuous_lawAt_plan line 65
  4. lemma OAI.WeakHessian.continuous_lawAt_time line 69
  5. def OAI.WeakHessian.cellPlanFamily line 81
  6. lemma OAI.WeakHessian.isCompact_cellPlanFamily line 86
  7. lemma OAI.WeakHessian.IsGeodesic.speed_energy_le line 121
  8. def OAI.WeakHessian.CDEnvironment.stablePlanFamily line 133
  9. lemma OAI.WeakHessian.CDEnvironment.stablePlanFamily_closed line 136
  10. lemma OAI.WeakHessian.CDEnvironment.exists_stable_plan line 146
  11. def OAI.WeakHessian.CDEnvironment.limitPlan line 164
  12. lemma OAI.WeakHessian.CDEnvironment.limitPlan_dyadic line 167
  13. lemma OAI.WeakHessian.CDEnvironment.limitPlan_finite_entropy_dyadic line 172
  14. lemma OAI.WeakHessian.CDEnvironment.limitPlan_entropy_bound_dyadic line 177
  15. lemma OAI.WeakHessian.CDEnvironment.limitPlan_dominated_dyadic line 184
  16. lemma OAI.WeakHessian.CDEnvironment.limitPlan_dominated line 189
  17. lemma OAI.WeakHessian.CDEnvironment.limitPlan_supported line 216
  18. lemma OAI.WeakHessian.CDEnvironment.limitPlan_finite_entropy line 222
  19. lemma OAI.WeakHessian.CDEnvironment.limitPlan_boundedTracks line 236
  20. lemma OAI.WeakHessian.CDEnvironment.limitPlan_isTestPlan line 245