Documentation

Mathlib.Geometry.Manifold.Instances.Real

Constructing examples of manifolds over ℝ #

We introduce the necessary bits to be able to define manifolds modelled over ℝ^n, boundaryless or with boundary or with corners. As a concrete example, we construct explicitly the manifold with boundary structure on the real interval [x, y].

More specifically, we introduce

Notations #

In the locale Manifold, we introduce the notations

For instance, if a manifold M is boundaryless, smooth and modelled on EuclideanSpace ℝ (Fin m), and N is smooth with boundary modelled on EuclideanHalfSpace n, and f : M β†’ N is a smooth map, then the derivative of f can be written simply as mfderiv (𝓑 m) (π“‘βˆ‚ n) f (as to why the model with corners can not be implicit, see the discussion in Geometry.Manifold.SmoothManifoldWithCorners).

Implementation notes #

The manifold structure on the interval [x, y] = Icc x y requires the assumption x < y as a typeclass. We provide it as [Fact (x < y)].

The half-space in ℝ^n, used to model manifolds with boundary. We only define it when 1 ≀ n, as the definition only makes sense in this case.

Equations
Instances For

    The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative coordinates.

    Equations
    Instances For
      Equations
      • instTopologicalSpaceEuclideanHalfSpace = instTopologicalSpaceSubtype
      Equations
      • instTopologicalSpaceEuclideanQuadrant = instTopologicalSpaceSubtype
      Equations
      • instInhabitedEuclideanHalfSpace = { default := ⟨0, β‹―βŸ© }
      Equations
      • instInhabitedEuclideanQuadrant = { default := ⟨0, β‹―βŸ© }
      theorem EuclideanQuadrant.ext {n : β„•} (x y : EuclideanQuadrant n) (h : ↑x = ↑y) :
      x = y
      theorem EuclideanHalfSpace.ext {n : β„•} [NeZero n] (x y : EuclideanHalfSpace n) (h : ↑x = ↑y) :
      x = y
      theorem EuclideanQuadrant.convex {n : β„•} :
      Convex ℝ {x : EuclideanSpace ℝ (Fin n) | βˆ€ (i : Fin n), 0 ≀ x i}
      theorem range_euclideanHalfSpace (n : β„•) [NeZero n] :
      (Set.range fun (x : EuclideanHalfSpace n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | 0 ≀ y 0}
      @[deprecated range_euclideanHalfSpace]
      theorem range_half_space (n : β„•) [NeZero n] :
      (Set.range fun (x : EuclideanHalfSpace n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | 0 ≀ y 0}

      Alias of range_euclideanHalfSpace.

      @[simp]
      theorem interior_halfSpace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      interior {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a < y i}
      @[deprecated interior_halfSpace]
      theorem interior_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      interior {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a < y i}

      Alias of interior_halfSpace.

      @[simp]
      theorem closure_halfSpace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      closure {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i}
      @[deprecated closure_halfSpace]
      theorem closure_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      closure {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i}

      Alias of closure_halfSpace.

      @[simp]
      theorem closure_open_halfSpace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      closure {y : PiLp p fun (x : Fin n) => ℝ | a < y i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i}
      @[deprecated closure_open_halfSpace]
      theorem closure_open_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      closure {y : PiLp p fun (x : Fin n) => ℝ | a < y i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i}

      Alias of closure_open_halfSpace.

      @[simp]
      theorem frontier_halfSpace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      frontier {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a = y i}
      @[deprecated frontier_halfSpace]
      theorem frontier_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      frontier {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a = y i}

      Alias of frontier_halfSpace.

      theorem range_euclideanQuadrant (n : β„•) :
      (Set.range fun (x : EuclideanQuadrant n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | βˆ€ (i : Fin n), 0 ≀ y i}
      @[deprecated range_euclideanQuadrant]
      theorem range_quadrant (n : β„•) :
      (Set.range fun (x : EuclideanQuadrant n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | βˆ€ (i : Fin n), 0 ≀ y i}

      Alias of range_euclideanQuadrant.

      Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanHalfSpace n), used as a model for manifolds with boundary. In the locale Manifold, use the shortcut π“‘βˆ‚ n.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanQuadrant n), used as a model for manifolds with corners

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The model space used to define n-dimensional real manifolds without boundary.

          Equations
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The model space used to define n-dimensional real manifolds with boundary.

              Equations
              Instances For

                Pretty printer defined by notation3 command.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def IccLeftChart (x y : ℝ) [h : Fact (x < y)] :

                  The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in EuclideanHalfSpace 1.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def IccRightChart (x y : ℝ) [h : Fact (x < y)] :

                    The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in EuclideanHalfSpace 1.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      instance IccChartedSpace (x y : ℝ) [h : Fact (x < y)] :

                      Charted space structure on [x, y], using only two charts taking values in EuclideanHalfSpace 1.

                      Equations
                      • One or more equations did not get rendered due to their size.

                      The manifold structure on [x, y] is smooth.

                      Register the manifold structure on Icc 0 1. These are merely special cases of IccChartedSpace and Icc_smoothManifoldWithCorners.