OAI/Geometry/SmoothYau/Smoothness/SphericalBaseProfileRadius.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.contMDiffAt_coordinateVector line 42
  2. lemma OAI.YauCounterexamples.contDiffOn_metricCoefficient line 57
  3. lemma OAI.YauCounterexamples.metricCoefficients_posDef line 104
  4. lemma OAI.YauCounterexamples.metricCoefficients_det_pos line 138
  5. lemma OAI.YauCounterexamples.contDiffOn_metricDet line 142
  6. lemma OAI.YauCounterexamples.contDiffOn_metricDensity line 153
  7. lemma OAI.YauCounterexamples.contDiffOn_metricAdjugate line 192
  8. lemma OAI.YauCounterexamples.contDiffOn_metricInverse line 206
  9. lemma OAI.YauCounterexamples.metricInverse_posDef line 213
  10. lemma OAI.YauCounterexamples.quadratic_profile_fderiv line 238
  11. theorem OAI.YauCounterexamples.sphere_quadratic_profile_fderiv_ne_zero line 262
  12. lemma OAI.YauCounterexamples.coordinateMetricGradient_eq_zero_iff line 291
  13. lemma OAI.YauCounterexamples.positive_bilinear_bounded line 315
  14. def OAI.YauCounterexamples.flatMetricOfForm line 330
  15. def OAI.YauCounterexamples.metricBasisCoordinate line 371
  16. def OAI.YauCounterexamples.metricMatrixForm line 374
  17. lemma OAI.YauCounterexamples.metricMatrixForm_apply line 378
  18. lemma OAI.YauCounterexamples.metricMatrixForm_pos line 383
  19. lemma OAI.YauCounterexamples.metricMatrixForm_contDiffOn line 391
  20. def OAI.YauCounterexamples.chartMetricForm line 397
  21. lemma OAI.YauCounterexamples.chartMetricForm_contDiffOn line 400
  22. lemma OAI.YauCounterexamples.chartMetricForm_pos line 404
  23. lemma OAI.YauCounterexamples.chartMetricForm_pairing line 409
  24. lemma OAI.YauCounterexamples.chartMetricForm_symm line 437
  25. def OAI.YauCounterexamples.sphereChartMetric line 458
  26. lemma OAI.YauCounterexamples.sphereChartMetric_pairing line 465
  27. lemma OAI.YauCounterexamples.sphereChartMetric_selfFlat line 469
  28. lemma OAI.YauCounterexamples.sphereChartMetric_round line 475
  29. lemma OAI.YauCounterexamples.sphereChart_norm_sq line 484
  30. def OAI.YauCounterexamples.sphericalBaseProfile line 493
  31. lemma OAI.YauCounterexamples.sphericalBaseProfile_smooth line 497
  32. theorem OAI.YauCounterexamples.sphericalBaseProfile_chart_hessian line 509
  33. lemma OAI.YauCounterexamples.sphericalBaseProfile_chart_eq line 533
  34. lemma OAI.YauCounterexamples.sphericalBaseProfile_chart_smooth line 543
  35. theorem OAI.YauCounterexamples.sphericalBaseProfile_chart_margins line 549
  36. lemma OAI.YauCounterexamples.sphericalBaseProfile_chart_fderiv_ne_zero line 566
  37. lemma OAI.YauCounterexamples.sphericalBaseProfile_radius line 598
  38. def OAI.YauCounterexamples.sphericalProfileGlue line 604
  39. lemma OAI.YauCounterexamples.sphericalProfileGlue_chart line 609
  40. lemma OAI.YauCounterexamples.sphericalProfileGlue_smooth line 617
  41. lemma OAI.YauCounterexamples.sphericalProfileGlue_sub line 626
  42. lemma OAI.YauCounterexamples.sphericalProfileGlue_tsupport line 634
  43. lemma OAI.YauCounterexamples.sphericalProfileGlue_close line 646
  44. theorem OAI.YauCounterexamples.spherical_envelope_perturbation line 658