OAI/Geometry/WeakHessian/Measure/InlinedFile0.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.IsTestPlan.of_measure_le_smul line 26
  2. lemma OAI.WeakHessian.isTestPlan_iff_of_comparable line 37
  3. lemma OAI.WeakHessian.LocallyL2.of_measure_le_smul line 42
  4. lemma OAI.WeakHessian.locallyL2_iff_of_comparable line 49
  5. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.of_measure_le_smul line 54
  6. lemma OAI.WeakHessian.localWeakUpperGradient_iff_of_comparable line 63
  7. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.change_measure line 69
  8. lemma OAI.WeakHessian.minimalLocalWeakUpperGradient_iff_of_comparable line 78
  9. lemma OAI.WeakHessian.weakGradient_isMinimal line 84
  10. theorem OAI.WeakHessian.weakGradient_eq_of_comparable line 89
  11. theorem OAI.WeakHessian.gamma_eq_of_comparable line 105
  12. lemma OAI.WeakHessian.localSobolev_iff_of_comparable line 112
  13. theorem OAI.WeakHessian.sobolev_iff_of_comparable line 118
  14. def OAI.WeakHessian.exponentialMeasure line 131
  15. lemma OAI.WeakHessian.exponentialMeasure_le line 135
  16. lemma OAI.WeakHessian.measure_le_exponentialMeasure line 143
  17. lemma OAI.WeakHessian.exponentialMeasure_comparable line 160
  18. theorem OAI.WeakHessian.weakGradient_exponentialMeasure line 167
  19. theorem OAI.WeakHessian.gamma_exponentialMeasure line 174
  20. theorem OAI.WeakHessian.sobolev_exponentialMeasure_iff line 181
  21. lemma OAI.WeakHessian.absolutelyContinuous_of_dist_le line 190
  22. lemma OAI.WeakHessian.lipschitz_comp_absolutelyContinuous line 205
  23. lemma OAI.WeakHessian.lintegral_lt_top_of_square line 217
  24. lemma OAI.WeakHessian.IsAC2.absolutelyContinuous line 240
  25. lemma OAI.WeakHessian.deriv_comp_le_metricSpeed line 296
  26. lemma OAI.WeakHessian.deriv_comp_le_metricSpeed_all line 324
  27. lemma OAI.WeakHessian.lipschitz_endpoint_bound line 335
  28. lemma OAI.WeakHessian.lipschitz_isLocalWeakUpperGradient line 355
  29. lemma OAI.WeakHessian.weakGradient_le_lipschitz line 369
  30. lemma OAI.WeakHessian.LocallyL2.const_mul line 377
  31. lemma OAI.WeakHessian.isLocalWeakUpperGradient_const line 381
  32. lemma OAI.WeakHessian.isMinimalLocalWeakUpperGradient_const line 389
  33. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.ae_eq line 393
  34. lemma OAI.WeakHessian.weakGradient_ae_eq_of_isMinimal line 399
  35. lemma OAI.WeakHessian.weakGradient_const line 403
  36. lemma OAI.WeakHessian.weakGradient_nonneg line 407
  37. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.const_mul line 412
  38. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.const_mul line 434
  39. lemma OAI.WeakHessian.weakGradient_const_mul line 447
  40. lemma OAI.WeakHessian.gamma_self line 462
  41. lemma OAI.WeakHessian.IsLaplacian.energy_identity line 472
  42. lemma OAI.WeakHessian.IsLaplacian.energy_le_graph_sq line 477