OAI/Geometry/WeakHessian/LocalBounds/SpeedApprox.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.speedApprox line 19
  2. lemma OAI.WeakHessian.metricSpeed_eq_iInf_speedApprox line 24
  3. lemma OAI.WeakHessian.lowerSemicontinuous_speedApprox line 58
  4. lemma OAI.WeakHessian.measurable_metricSpeed line 68
  5. lemma OAI.WeakHessian.LocallyL2.aestronglyMeasurable line 74
  6. lemma OAI.WeakHessian.LocallyL2.aemeasurable line 86
  7. lemma OAI.WeakHessian.IsTestPlan.ae_prod_eval_of_ae line 89
  8. lemma OAI.WeakHessian.IsTestPlan.aemeasurable_evalReal line 109
  9. lemma OAI.WeakHessian.IsTestPlan.aemeasurable_eval line 116
  10. lemma OAI.WeakHessian.IsTestPlan.aemeasurable_action line 122
  11. lemma OAI.WeakHessian.LocallyL2.add line 131
  12. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.add line 136
  13. lemma OAI.WeakHessian.IsTestPlan.of_plan_le_smul line 182
  14. lemma OAI.WeakHessian.BoundedTracks.of_plan_le_smul line 206
  15. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.ae_endpoint_le line 211
  16. lemma OAI.continuous_ae_map_of_ae line 242