PhysLean Documentation

PhysLean.SpaceAndTime.SpaceTime.Basic

Spacetime #

i. Overview #

In this file we define the type SpaceTime d which corresponds to d+1 dimensional spacetime. This is equipped with an instance of the action of a Lorentz group, corresponding to Minkowski-spacetime.

It is defined through Lorentz.Vector d, and carries the tensorial instance, allowing it to be used in tensorial expressions.

ii. Key results #

iii. Table of contents #

iv. References #

A. The definition of SpaceTime d #

@[reducible, inline]
abbrev SpaceTime (d : := 3) :

SpaceTime d corresponds to d+1 dimensional space-time. This is equipped with an instaance of the action of a Lorentz group, corresponding to Minkowski-spacetime.

Equations
Instances For

    B. Maps to and from Space and Time #

    B.1. Linear map to Space d #

    The space part of spacetime.

    Equations
    Instances For

      B.1.1. Explicit expansion of map to space #

      @[simp]
      theorem SpaceTime.space_toCoord_symm {d : } (f : Fin 1 Fin d) :
      space f = fun (i : Fin d) => f (Sum.inr i)

      B.1.2. Equivariance of the to space under rotations #

      The function space is equivariant with respect to rotations.

      Equations
      Instances For

        B.2. Linear map to Time #

        The time part of spacetime.

        Equations
        Instances For

          B.2.1. Explicit expansion of map to time in terms of coordinates #

          @[simp]
          theorem SpaceTime.time_val_toCoord_symm {d : } (f : Fin 1 Fin d) :
          (time f).val = f (Sum.inl 0)

          B.3. toTimeAndSpace: Continuous linear equivalence to Time × Space d #

          A continuous linear equivalence between SpaceTime d and Time × Space d.

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

            B.3.1. Derivative of toTimeAndSpace #

            B.3.2. Derivative of the inverse of toTimeAndSpace #

            B.3.3. toTimeAndSpace acting on spatial basis vectors #

            B.3.4. toTimeAndSpace acting on the temperal basis vectors #

            C. Continous linear map to coordinates #

            def SpaceTime.coord {d : } (μ : Fin (1 + d)) :

            For a given μ : Fin (1 + d) coord μ p is the coordinate of p in the direction μ.

            This is denoted 𝔁 μ p, where 𝔁 is typed with \MCx.

            Equations
            Instances For

              For a given μ : Fin (1 + d) coord μ p is the coordinate of p in the direction μ.

              This is denoted 𝔁 μ p, where 𝔁 is typed with \MCx.

              Equations
              Instances For
                theorem SpaceTime.coord_apply {d : } (μ : Fin (1 + d)) (y : SpaceTime d) :
                (coord μ) y = y (finSumFinEquiv.symm μ)

                The continuous linear map from a point in space time to one of its coordinates.

                Equations
                Instances For

                  D. Derivatives of functions on SpaceTime d #

                  D.1. The definition of the derivative #

                  noncomputable def SpaceTime.deriv {M : Type} [AddCommGroup M] [Module M] [TopologicalSpace M] {d : } (μ : Fin 1 Fin d) (f : SpaceTime dM) :
                  SpaceTime dM

                  The derivative of a function SpaceTime d → ℝ along the μ coordinte.

                  Equations
                  Instances For

                    The derivative of a function SpaceTime d → ℝ along the μ coordinte.

                    Equations
                    Instances For

                      D.2. Basic equality lemmas #

                      theorem SpaceTime.deriv_eq {M : Type} [AddCommGroup M] [Module M] [TopologicalSpace M] {d : } (μ : Fin 1 Fin d) (f : SpaceTime dM) (y : SpaceTime d) :
                      theorem SpaceTime.deriv_apply_eq {d : } (μ ν : Fin 1 Fin d) (f : SpaceTime dLorentz.Vector d) (hf : Differentiable f) (y : SpaceTime d) :
                      deriv μ f y ν = (fderiv (fun (x : SpaceTime d) => f x ν) y) (Lorentz.Vector.basis μ)
                      @[simp]
                      theorem SpaceTime.deriv_coord {d : } (μ ν : Fin 1 Fin d) :
                      (deriv μ fun (x : SpaceTime d) => x ν) = if μ = ν then 1 else 0

                      D.3. Derivative of the zero function #

                      @[simp]
                      theorem SpaceTime.deriv_zero {d : } (μ : Fin 1 Fin d) :
                      (deriv μ fun (x : SpaceTime d) => 0) = 0

                      D.4. The derivative of a function composed with a Lorentz transformation #

                      theorem SpaceTime.deriv_comp_lorentz_action {M : Type} [NormedAddCommGroup M] [NormedSpace M] {d : } (μ : Fin 1 Fin d) (f : SpaceTime dM) (hf : Differentiable f) (Λ : (LorentzGroup d)) (x : SpaceTime d) :
                      deriv μ (fun (x : SpaceTime d) => f (Λ x)) x = ν : Fin 1 Fin d, Λ ν μ deriv ν f (Λ x)

                      D.5. Spacetime derivatives in terms of time and space derivatives #

                      theorem SpaceTime.deriv_sum_inr {d : } {M : Type} [NormedAddCommGroup M] [NormedSpace M] (f : SpaceTime dM) (hf : Differentiable f) (x : SpaceTime d) (i : Fin d) :
                      deriv (Sum.inr i) f x = Space.deriv i (fun (y : Space d) => f (toTimeAndSpace.symm ((toTimeAndSpace x).1, y))) (toTimeAndSpace x).2

                      E. Measures on SpaceTime d #

                      E.1. Instance of a measureable space #

                      E.2. Instance of a borel space #

                      E.3. Definition of an inner product space structure on SpaceTime d #

                      E.4. Instance of a measure space #

                      E.5. Volume measure is positive on non-empty open sets #

                      E.6. Volume measure is a finite measure on compact sets #

                      E.7. Volume measure is an additive Haar measure #