OAI/Geometry/StableBernstein/Model.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StableBernstein.W02.scalarDifferential line 18
  2. def OAI.StableBernstein.W02.differentialEnergy line 21
  3. def OAI.StableBernstein.W02.IsSmoothCompactTest line 23
  4. def OAI.StableBernstein.W02.IntrinsicStability line 34
  5. abbrev OAI.StableBernstein.W01.E6 line 45
  6. abbrev OAI.StableBernstein.W01.E7 line 46
  7. abbrev OAI.StableBernstein.W01.I6 line 47
  8. abbrev OAI.StableBernstein.W01.I7 line 48
  9. structure OAI.StableBernstein.W01.SmoothImmersion line 56
  10. def OAI.StableBernstein.W01.differential line 59
  11. lemma OAI.StableBernstein.W01.SmoothImmersion.differential_injective line 61
  12. structure OAI.StableBernstein.W01.GlobalUnitNormal line 64
  13. def OAI.StableBernstein.W01.inducedMetric line 69
  14. def OAI.StableBernstein.W01.inducedMetricBilinear line 71
  15. lemma OAI.StableBernstein.W01.inducedMetricBilinear_apply line 74
  16. lemma OAI.StableBernstein.W01.inducedMetric_symm line 76
  17. lemma OAI.StableBernstein.W01.inducedMetric_self_eq_norm_sq line 78
  18. lemma OAI.StableBernstein.W01.SmoothImmersion.inducedMetric_pos line 80
  19. def OAI.StableBernstein.W01.secondFundamentalForm line 87
  20. def OAI.StableBernstein.W01.secondFundamentalBilinear line 89
  21. def OAI.StableBernstein.W01.SmoothImmersion.toRiemannianMetric line 92
  22. def OAI.StableBernstein.W01.HasInducedRiemannianMetric line 115
  23. lemma OAI.StableBernstein.W01.SmoothImmersion.hasInducedRiemannianMetric line 120
  24. def OAI.StableBernstein.W18.ApproximateMidpoints line 135
  25. theorem OAI.StableBernstein.W18.approximate_dyadic_split line 138
  26. theorem OAI.StableBernstein.W18.compact_closedBall_extend line 157
  27. theorem OAI.StableBernstein.W18.totallyBounded_closedBall_of_compact_smaller line 189
  28. theorem OAI.StableBernstein.W18.compact_closedBall_of_compact_smaller line 233
  29. theorem OAI.StableBernstein.W18.properSpace_of_complete_locallyCompact_approximateMidpoints line 240
  30. theorem OAI.StableBernstein.W04.exists_half_speed_integral line 271
  31. structure OAI.StableBernstein.W01.CompleteInducedMetric line 298
  32. lemma OAI.StableBernstein.W01.CompleteInducedMetric.edist_eq line 303
  33. instance OAI.StableBernstein.W01.tangentFiniteDimensional line 306
  34. lemma OAI.StableBernstein.W01.tangent_dimension line 317
  35. def OAI.StableBernstein.W01.tangentOrthonormalBasis line 321
  36. def OAI.StableBernstein.W01.shapeOperator line 323
  37. def OAI.StableBernstein.W01.meanCurvatureTrace line 326
  38. def OAI.StableBernstein.W01.Minimal line 328
  39. def OAI.StableBernstein.W01.curvatureNormSqInBasis line 329
  40. def OAI.StableBernstein.W01.curvatureNormSq line 332
  41. def OAI.StableBernstein.W01.differentialPairingBilinear line 347
  42. lemma OAI.StableBernstein.W01.contMDiff_differentialPairing line 350
  43. lemma OAI.StableBernstein.W01.contMDiff_inducedMetricBilinear line 382
  44. lemma OAI.StableBernstein.W01.HasInducedRiemannianMetric.isContMDiffRiemannianBundle line 392
  45. theorem OAI.StableBernstein.W04.induced_continuousRiemannianBundle line 408
  46. theorem OAI.StableBernstein.W04.continuous_intrinsic_speed line 412
  47. theorem OAI.StableBernstein.W04.pathELength_eq_ofReal_speed_integral line 427
  48. theorem OAI.StableBernstein.W04.induced_approximateMidpoints line 436
  49. theorem OAI.StableBernstein.W04.induced_properSpace line 470
  50. theorem OAI.StableBernstein.W03.edist_lt_top_of_preconnected line 484
  51. theorem OAI.StableBernstein.W03.inducedRiemannianBundle_continuous line 498
  52. def OAI.StableBernstein.W03.canonicalInducedMetricSpace line 505
  53. theorem OAI.StableBernstein.W03.canonicalInducedMetricSpace_edist line 512
  54. theorem OAI.StableBernstein.W03.canonicalInducedMetricSpace_isRiemannian line 518
  55. def OAI.StableBernstein.W03.CanonicallyCompleteInducedMetric line 525
  56. theorem OAI.StableBernstein.W03.completeInducedMetric_of_canonical_complete line 528
  57. def OAI.StableBernstein.FullConclusion line 548
  58. def OAI.StableBernstein.W02.inverseChartBasisVector line 567
  59. def OAI.StableBernstein.W02.chartMetricMatrix line 571
  60. def OAI.StableBernstein.W02.chartVolumeDensity line 574
  61. def OAI.StableBernstein.W02.chartInverseExtension line 588
  62. def OAI.StableBernstein.W02.chartRiemannianMeasure line 591
  63. lemma OAI.StableBernstein.W02.exists_countable_chart_cover line 605
  64. def OAI.StableBernstein.W02.volumeChartCenters line 617
  65. def OAI.StableBernstein.W02.volumeChartPiece line 618
  66. def OAI.StableBernstein.W02.riemannianVolume line 620
  67. def OAI.StableBernstein.RiemannianGeometricStability line 632
  68. theorem OAI.StableBernstein.secondCountable_of_complete_induced_metric line 648
  69. theorem OAI.StableBernstein.canonical_complete_secondCountable line 654
  70. def OAI.StableBernstein.IntrinsicStableBernstein line 663