OAI/Geometry/Riemannian/HarmonicCore/Model.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HarmonicCounterexample.Main.E3 line 11
  2. abbrev OAI.HarmonicCounterexample.Main.M3 line 12
  3. def OAI.HarmonicCounterexample.Main.coordinateVector line 14
  4. structure OAI.HarmonicCounterexample.Main.SmoothMetric3 line 16
  5. def OAI.HarmonicCounterexample.Main.SmoothMetric3.inner line 23
  6. def OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv line 26
  7. def OAI.HarmonicCounterexample.Main.SmoothMetric3.christoffel line 29
  8. def OAI.HarmonicCounterexample.Main.SmoothMetric3.curvature line 35
  9. def OAI.HarmonicCounterexample.Main.SmoothMetric3.ricci line 41
  10. def OAI.HarmonicCounterexample.Main.SmoothMetric3.RicciNonnegative line 44
  11. def OAI.HarmonicCounterexample.Main.SmoothMetric3.sectionNumerator line 47
  12. def OAI.HarmonicCounterexample.Main.SmoothMetric3.sectionDenominator line 51
  13. def OAI.HarmonicCounterexample.Main.SmoothMetric3.pathLength line 54
  14. def OAI.HarmonicCounterexample.Main.SmoothMetric3.distance line 57
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.pathLength_nonneg line 61
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.distance_nonneg line 66
  17. def OAI.HarmonicCounterexample.Main.SmoothMetric3.Complete line 71
  18. def OAI.HarmonicCounterexample.Main.SmoothMetric3.EuclideanNearOrigin line 77
  19. def OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian line 80
  20. def OAI.HarmonicCounterexample.Main.SmoothMetric3.PolynomialGrowth line 85
  21. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv_add line 88
  22. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv_smul line 94
  23. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_add line 100
  24. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_smul line 116
  25. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.polynomialGrowth_zero line 136
  26. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.polynomialGrowth_add line 141
  27. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.polynomialGrowth_smul line 152
  28. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_zero line 161
  29. def OAI.HarmonicCounterexample.Main.SmoothMetric3.harmonicGrowthSpace line 164
  30. def OAI.HarmonicCounterexample.Main.SmoothMetric3.harmonicDimension line 176
  31. def OAI.HarmonicCounterexample.Main.SmoothMetric3.volumeMeasure line 179
  32. def OAI.HarmonicCounterexample.Main.SmoothMetric3.HasAVR line 182
  33. def OAI.HarmonicCounterexample.Main.SmoothMetric3.radialVector line 186
  34. def OAI.HarmonicCounterexample.Main.SmoothMetric3.NegativeRadialSequence line 189
  35. def OAI.HarmonicCounterexample.Main.SmoothMetric3.IsTangentConeAtInfinity line 196
  36. def OAI.HarmonicCounterexample.Main.SmoothMetric3.TwoNonisometricTangentCones line 206
  37. def OAI.HarmonicCounterexample.Main.euclidean line 216
  38. def OAI.HarmonicCounterexample.Main.MainStatement line 221