Space

In this module, we define the the type Space d which corresponds to d-dimensional flat Euclidean space and prove some properties about it.

The scope of this module is to define on Space d basic instances related translations and the metric. We do not here define the structure of a Module on Space d, as this is done in PhysLean.SpaceAndTime.Space.Module.

PhysLean sits downstream of Mathlib, and above we import the necessary Mathlib modules which contain (perhaps transitively through imports) the definitions and theorems we need.

Implementation details

The exact implementation of Space d into PhysLean is discussed in numerous places on the Lean Zulip, including:

• https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Space.20vs.20EuclideanSpace/with/575332888

There is a choice between defining Space d as an abbrev of EuclideanSpace ℝ (Fin d), as a def of a type with value EuclideanSpace ℝ (Fin d) or as a structure with a field val : Fin d → ℝ :

+---------------------------------------------------+---------+-------+-----------+ | | abbrev | def | structure | +---------------------------------------------------+---------+-------+-----------+ | allows casting from EuclideanSpace | yes | yes | no | | carries instances from EuclideanSpace | yes | no | no | | requires reproving of lemmas from EuclideanSpace| no | yes | yes | +---------------------------------------------------+---------+-------+-----------+

The structure is the most conservative choice, as everything needs redefining. However, there is are two benefits of using it:

1. It allows us to be precise about the instances we define on Space d, and makes future refactoring of those instances easier.
2. It allows us to give the necessary physics context to results about Space d, which would not otherwise be possible if we reuse results from Mathlib.

In this module we give Space d the instances of a NormedAddTorsor and a MetricSpace. These physically correspond to the statement that you can add a vector to a point in space, and that there is a notion of distance between points in space. This notion of distance corresponds to a choice of length unit.

In PhysLean.SpaceAndTime.Space.Module we give Space d the structure of a Module (aka vector space), a Norm and an InnerProductSpace. These require certain choices, for example the choice of a zero in Space d.

This module structure is necessary in numerous places. For example, the normal derivatives used by physicists ∂_x, ∂_y, ∂_z require a module structure.

Because of this, one should be careful to avoid using the explicit zero in Space d, or adding two Space d values together. Where possible one should use the VAdd (EuclideanSpace ℝ (Fin d)) (Space d) instance instead.

A. The Space type

structure Space (d : ℕ := 3) : Type

The type Space d is the world-volume which corresponds to d dimensional (flat) Euclidean space with a given (but arbitrary) choice of length unit, and a given (but arbitrary) choice of zero.

The default value of d is 3. Thus Space = Space 3

• val : Fin d → ℝ

  The underlying map Fin d → ℝ associated with a point in Space.

theorem Space.eq_of_val {d : ℕ} {p q : Space d} (h : p.val = q.val) : p = q

@[simp]

theorem Space.val_eq_iff {d : ℕ} {p q : Space d} : p.val = q.val ↔ p = q

B. Instances on Space

B.1. Instance of coercion to functions

instance Space.instCoeFunForallFinReal {d : ℕ} : CoeFun (Space d) fun (x : Space d) => Fin d → ℝ

Equations

• Space.instCoeFunForallFinReal = { coe := fun (p : Space d) => p.val }

theorem Space.eq_of_apply {d : ℕ} {p q : Space d} (h : ∀ (i : Fin d), p.val i = q.val i) : p = q

theorem Space.eq_of_apply_iff {d : ℕ} {p q : Space d} : p = q ↔ ∀ (i : Fin d), p.val i = q.val i

B.2. The Non-emptiness

instance Space.instNonempty {d : ℕ} : Nonempty (Space d)

instance Space.instSubsingletonOfNatNat : Subsingleton (Space 0)

B.3.1. The additive action

noncomputable instance Space.instVAddEuclideanSpaceRealFin {d : ℕ} : VAdd (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

• Space.instVAddEuclideanSpaceRealFin = { vadd := fun (v : EuclideanSpace ℝ (Fin d)) (s : Space d) => { val := fun (i : Fin d) => v.ofLp i + s.val i } }

@[simp]

theorem Space.vadd_val {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) : (v +ᵥ s).val = fun (i : Fin d) => v.ofLp i + s.val i

@[simp]

theorem Space.vadd_apply {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) (i : Fin d) : (v +ᵥ s).val i = v.ofLp i + s.val i

theorem Space.vadd_transitive {d : ℕ} (s1 s2 : Space d) : ∃ (v : EuclideanSpace ℝ (Fin d)), v +ᵥ s1 = s2

noncomputable instance Space.instAddActionEuclideanSpaceRealFin {d : ℕ} : AddAction (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

• Space.instAddActionEuclideanSpaceRealFin = { toVAdd := Space.instVAddEuclideanSpaceRealFin, add_vadd := ⋯, zero_vadd := ⋯ }

B.3.2. Subtraction

noncomputable instance Space.instVSubEuclideanSpaceRealFin {d : ℕ} : VSub (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

• Space.instVSubEuclideanSpaceRealFin = { vsub := fun (s1 s2 : Space d) => WithLp.toLp 2 fun (i : Fin d) => s1.val i - s2.val i }

@[simp]

theorem Space.vsub_apply {d : ℕ} (s1 s2 : Space d) (i : Fin d) : (s1 -ᵥ s2).ofLp i = s1.val i - s2.val i

B.3.3. AddTorsor instance

noncomputable instance Space.instAddTorsorEuclideanSpaceRealFin {d : ℕ} : AddTorsor (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

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

B.4. PseudoMetricSpace

noncomputable instance Space.instDist {d : ℕ} : Dist (Space d)

Equations

• Space.instDist = { dist := fun (p q : Space d) => √(∑ i : Fin d, (p.val i - q.val i) ^ 2) }

theorem Space.dist_eq {d : ℕ} (p q : Space d) : dist p q = √(∑ i : Fin d, (p.val i - q.val i) ^ 2)

noncomputable instance Space.instPseudoMetricSpace {d : ℕ} : PseudoMetricSpace (Space d)

Equations

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

B.5. NormAddTorsor instance

noncomputable instance Space.instNormedAddTorsorEuclideanSpaceRealFin {d : ℕ} : NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

• Space.instNormedAddTorsorEuclideanSpaceRealFin = { toAddTorsor := Space.instAddTorsorEuclideanSpaceRealFin, dist_eq_norm' := ⋯ }

B.6. Metric space instance

noncomputable instance Space.instMetricSpace {d : ℕ} : MetricSpace (Space d)

Equations

• Space.instMetricSpace = { toPseudoMetricSpace := Space.instPseudoMetricSpace, eq_of_dist_eq_zero := ⋯ }

B.7. Non-trivality

instance Space.instNontrivialSucc {d : ℕ} : Nontrivial (Space d.succ)

C. Model structure (i.e. structure of a manifold)

noncomputable def Space.manifoldStructure (d : ℕ) : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin d)) (Space d)

The manifold structure on Space d.

Equations

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