OAI/Geometry/SmoothYau/Smoothness/PulledGradient.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.localMetricFlat line 22
  2. lemma OAI.YauCounterexamples.localMetricFlat_pairing line 27
  3. lemma OAI.YauCounterexamples.localMetricFlat_invertible line 36
  4. lemma OAI.YauCounterexamples.contMDiffAt_localMetricFlat line 58
  5. lemma OAI.YauCounterexamples.local_metricGradient line 65
  6. theorem OAI.YauCounterexamples.contMDiff_metricGradient line 87
  7. def OAI.YauCounterexamples.selfMetricFlat line 120
  8. lemma OAI.YauCounterexamples.selfMetricFlat_apply line 125
  9. lemma OAI.YauCounterexamples.localMetricFlat_self line 129
  10. lemma OAI.YauCounterexamples.contDiff_selfMetricFlat line 141
  11. lemma OAI.YauCounterexamples.selfMetricFlat_symm line 150
  12. lemma OAI.YauCounterexamples.selfMetricFlat_pos line 154
  13. lemma OAI.YauCounterexamples.selfMetricFlat_invertible line 157
  14. def OAI.YauCounterexamples.coordinateKoszul line 162
  15. lemma OAI.YauCounterexamples.coordinateKoszul_apply line 165
  16. def OAI.YauCounterexamples.metricChristoffel line 170
  17. lemma OAI.YauCounterexamples.metricChristoffel_pairing line 174
  18. lemma OAI.YauCounterexamples.contDiff_metricChristoffel line 183
  19. lemma OAI.YauCounterexamples.fderiv_selfMetricFlat_symm line 197
  20. lemma OAI.YauCounterexamples.metricChristoffel_symm line 211
  21. lemma OAI.YauCounterexamples.metricChristoffel_compatible line 219
  22. lemma OAI.YauCounterexamples.metricGradient_self line 227
  23. theorem OAI.YauCounterexamples.compact_positive_bilinear_lower line 239
  24. lemma OAI.YauCounterexamples.compact_selfMetricFlat_lower line 271
  25. theorem OAI.YauCounterexamples.compact_metric_tangent_bound line 276
  26. def OAI.YauCounterexamples.coordinateCovariantSecond line 322
  27. lemma OAI.YauCounterexamples.continuous_coordinateCovariantSecond line 327
  28. lemma OAI.YauCounterexamples.quadraticPlaneStrict_iff_nonzero line 346
  29. lemma OAI.YauCounterexamples.quadraticPlaneFull_iff_nonzero line 360
  30. def OAI.YauCounterexamples.actualCoordinateHessian line 374
  31. def OAI.YauCounterexamples.coordinateMetricGradient line 377
  32. lemma OAI.YauCounterexamples.coordinateMetricGradient_eq line 380
  33. lemma OAI.YauCounterexamples.contDiff_coordinateMetricGradient line 385
  34. def OAI.YauCounterexamples.actualProfileTraceForm line 394
  35. def OAI.YauCounterexamples.actualProfileStrict line 398
  36. def OAI.YauCounterexamples.actualProfileFull line 402
  37. lemma OAI.YauCounterexamples.continuous_actualProfileTraceForm line 406
  38. lemma OAI.YauCounterexamples.selfMetricFlat_metric_norm line 421
  39. lemma OAI.YauCounterexamples.actualProfileTraceForm_tangent line 433
  40. lemma OAI.YauCounterexamples.profileStrict_iff_quadratic line 447
  41. lemma OAI.YauCounterexamples.profileFull_iff_quadratic line 461
  42. lemma OAI.YauCounterexamples.quadraticPlaneStrict_transport line 475
  43. lemma OAI.YauCounterexamples.quadraticPlaneFull_transport line 491
  44. lemma OAI.YauCounterexamples.coordinateProfileStrict_iff_tangent line 508
  45. lemma OAI.YauCounterexamples.coordinateProfileFull_iff_tangent line 536
  46. lemma OAI.YauCounterexamples.actualProfileStrict_iff_tangent line 564
  47. lemma OAI.YauCounterexamples.actualProfileFull_iff_tangent line 572
  48. theorem OAI.YauCounterexamples.exists_actual_preparation_covector line 580
  49. lemma OAI.YauCounterexamples.second_directional_eq line 639
  50. lemma OAI.YauCounterexamples.smooth_comp_second line 646
  51. lemma OAI.YauCounterexamples.smooth_product_second line 667
  52. theorem OAI.YauCounterexamples.corrugation_first line 691
  53. lemma OAI.YauCounterexamples.smooth_sum_second line 720
  54. lemma OAI.YauCounterexamples.smooth_const_smul_second line 735
  55. lemma OAI.YauCounterexamples.scaled_comp_second line 747
  56. theorem OAI.YauCounterexamples.corrugation_second line 760
  57. lemma OAI.YauCounterexamples.periodicRadialOffset_norm_le line 801
  58. lemma OAI.YauCounterexamples.periodicRadialOffset_radius_sq_le line 809
  59. theorem OAI.YauCounterexamples.periodicRadial_coefficients_bounded line 821
  60. theorem OAI.YauCounterexamples.periodicRadialFunction_bounded line 866
  61. theorem OAI.YauCounterexamples.periodicRadialFunction_fderiv_bound line 889
  62. def OAI.YauCounterexamples.pulledGradient line 925
  63. lemma OAI.YauCounterexamples.pulledGradient_pairing line 929
  64. def OAI.YauCounterexamples.pulledHessian line 933
  65. lemma OAI.YauCounterexamples.norm_bilinear_pullback_le line 938
  66. lemma OAI.YauCounterexamples.planeRadialCovector_le_radius line 949
  67. lemma OAI.YauCounterexamples.radial_coframe_bounds line 957
  68. lemma OAI.YauCounterexamples.periodicRadialSpeed_le_angular line 974
  69. def OAI.YauCounterexamples.radialCorrugation line 987
  70. lemma OAI.YauCounterexamples.radialCorrugation_smooth line 992
  71. lemma OAI.YauCounterexamples.radialCorrugation_gradient line 1003