OAI/Geometry/SmoothYau/Model.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.Euclidean line 11

    Also declared: ComparatorChallenges/SmoothYau.lean:12 (same declaration text).

  2. abbrev OAI.YauCounterexamples.Sphere line 12

    Also declared: ComparatorChallenges/SmoothYau.lean:13 (same declaration text).

  3. abbrev OAI.YauCounterexamples.FourManifold line 13

    Also declared: ComparatorChallenges/SmoothYau.lean:14 (same declaration text).

  4. abbrev OAI.YauCounterexamples.FourModel line 14

    Also declared: ComparatorChallenges/SmoothYau.lean:15 (same declaration text).

  5. instance OAI.YauCounterexamples.torusChartedSpace line 16

    Also declared: ComparatorChallenges/SmoothYau.lean:17 (same declaration text).

  6. instance OAI.YauCounterexamples.torusIsManifold line 19

    Also declared: ComparatorChallenges/SmoothYau.lean:20 (same declaration text).

  7. instance OAI.YauCounterexamples.fourChartedSpace line 23

    Also declared: ComparatorChallenges/SmoothYau.lean:24 (same declaration text).

  8. instance OAI.YauCounterexamples.fourIsManifold line 26

    Also declared: ComparatorChallenges/SmoothYau.lean:27 (same declaration text).

  9. abbrev OAI.YauCounterexamples.SmoothMetric line 38

    Source documentation

    Ordinary smooth positive-definite Riemannian metrics, with the existing tangent topology.

    Also declared: ComparatorChallenges/SmoothYau.lean:39 (same declaration text).

    abbrev SmoothMetric (E : Type*) [NormedAddCommGroup E] [NormedSpace ā„ E]
    (M : Type*) [TopologicalSpace M] [ChartedSpace E M] [IsManifold š“˜(ā„, E) āˆž M] :=
ā€¦
  10. abbrev OAI.YauCounterexamples.CoordIndex line 42

    Also declared: ComparatorChallenges/SmoothYau.lean:43 (same declaration text).

  11. def OAI.YauCounterexamples.coordinateVector line 46

    Source documentation

    A coordinate vector, pushed from a chart back into the tangent bundle.

    Also declared: ComparatorChallenges/SmoothYau.lean:47 (same declaration text).

    def coordinateVector (p : M) (y : E) (i : CoordIndex E) :
    TangentSpace š“˜(ā„, E) ((chartAt E p).symm y) :=
ā€¦

    Mentions: OAI.YauCounterexamples.CoordIndex

  12. def OAI.YauCounterexamples.metricCoefficients line 51

    Source documentation

    Metric coefficients in a chart. Only values in the chart target are used.

    Also declared: ComparatorChallenges/SmoothYau.lean:52 (same declaration text).

    def metricCoefficients (g : SmoothMetric E M) (p : M) (y : E) :
    Matrix (CoordIndex E) (CoordIndex E) ā„ :=
ā€¦

    Mentions: OAI.YauCounterexamples.SmoothMetric, OAI.YauCounterexamples.CoordIndex

  13. def OAI.YauCounterexamples.laplaceBeltrami line 59

    Source documentation

    The local coordinate formula det(g)^(-1/2) d_i(det(g)^(1/2) g^{ij} d_j u). The chart at the evaluation point is used, so all derivatives are taken in its open target.

    Also declared: ComparatorChallenges/SmoothYau.lean:60 (same declaration text).

    def laplaceBeltrami (g : SmoothMetric E M) (u : M ā†’ ā„) (x : M) : ā„ :=
ā€¦

    Mentions: OAI.YauCounterexamples.SmoothMetric

  14. structure OAI.YauCounterexamples.CoordinateTest line 70

    Source documentation

    One compact-chart seminorm test for the usual smooth topology of metrics.

    Also declared: ComparatorChallenges/SmoothYau.lean:71 (same declaration text).

    structure CoordinateTest (E : Type*) [NormedAddCommGroup E] [NormedSpace ā„ E]
    [FiniteDimensional ā„ E] (M : Type*) [TopologicalSpace M] [ChartedSpace E M] where
ā€¦
  15. def OAI.YauCounterexamples.IsSmoothNeighborhood line 82

    Source documentation

    The finite compact-chart derivative tests defining a Cāˆž neighborhood. A single positive tolerance suffices for the finitely many tests.

    Also declared: ComparatorChallenges/SmoothYau.lean:83 (same declaration text).

    def IsSmoothNeighborhood (gā‚€ : SmoothMetric E M) (N : Set (SmoothMetric E M)) : Prop :=
ā€¦

    Mentions: OAI.YauCounterexamples.SmoothMetric

  16. def OAI.YauCounterexamples.nodalMeasure line 92

    Source documentation

    Hausdorff measure for the path distance of the actual Riemannian metric, not the metric inherited from any ambient embedding.

    Also declared: ComparatorChallenges/SmoothYau.lean:93 (same declaration text).

    def nodalMeasure [T3Space M] (g : SmoothMetric E M) (d : ā„) (u : M ā†’ ā„) : ā„ā‰„0āˆž :=
ā€¦

    Mentions: OAI.YauCounterexamples.SmoothMetric

  17. def OAI.YauCounterexamples.HasUnboundedNodalRatio line 103

    Source documentation

    The eigensequence belongs to one fixed metric and has finite nodal measure.

    Also declared: ComparatorChallenges/SmoothYau.lean:104 (same declaration text).

    def HasUnboundedNodalRatio [T3Space M] (g : SmoothMetric E M) (d : ā„•) : Prop :=
ā€¦

    Mentions: OAI.YauCounterexamples.SmoothMetric

  18. def OAI.YauCounterexamples.IsRound line 116

    Source documentation

    The round metric is the pullback of the Euclidean scalar product under inclusion of the unit sphere. This predicate specifies exactly that tensor.

    Also declared: ComparatorChallenges/SmoothYau.lean:117 (same declaration text).

    def IsRound (g : SmoothMetric (Euclidean 3) (Sphere 3)) : Prop :=
ā€¦

    Mentions: OAI.YauCounterexamples.SmoothMetric, OAI.YauCounterexamples.Euclidean, OAI.YauCounterexamples.Sphere