Physlib.SpaceAndTime.Space.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Meta.TODO.Basic
public import Mathlib.Analysis.InnerProductSpace.PiL2
public import Mathlib.Geometry.Manifold.Instances.Real

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 Physlib.SpaceAndTime.Space.Module.

Physlib 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 Physlib is discussed in numerous places on the Lean Zulip, including:

https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/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:

It allows us to be precise about the instances we define on Space d, and makes future refactoring of those instances easier.

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 Physlib.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.

@[expose] public section

A. The `Space` 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

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

structure Space (d : ℕ := 3) where val : Fin d → ℝ

lemma eq_of_val {d} {p q : Space d} (h : p.val = q.val) :
    p = q := byd:ℕp:Space dq:Space dh:p.val = q.val⊢ p = q
  cases pmkd:ℕq:Space dval✝:Fin d → ℝh:{ val := val✝ }.val = q.val⊢ { val := val✝ } = q
  cases qmk.mkd:ℕval✝¹:Fin d → ℝval✝:Fin d → ℝh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ }
  congrAll goals completed! 🐙



@[simp]
lemma val_eq_iff {d} {p q : Space d} :
    p.val = q.val ↔ p = q := byd:ℕp:Space dq:Space d⊢ p.val = q.val ↔ p = q
  apply Iff.intrompd:ℕp:Space dq:Space d⊢ p.val = q.val → p = qmprd:ℕp:Space dq:Space d⊢ p = q → p.val = q.val
  ·mpd:ℕp:Space dq:Space d⊢ p.val = q.val → p = q exact eq_of_valAll goals completed! 🐙
  ·mprd:ℕp:Space dq:Space d⊢ p = q → p.val = q.val intro hmprd:ℕp:Space dq:Space dh:p = q⊢ p.val = q.val
    rw [hmprd:ℕp:Space dq:Space dh:p = q⊢ q.val = q.valAll goals completed! 🐙]All goals completed! 🐙

B. Instances on `Space`

B.1. Instance of coercion to functions

instance {d} : CoeFun (Space d) (fun _ => Fin d → ℝ) where
  coe p := p.val

@[ext]
lemma eq_of_apply {d} {p q : Space d}
    (h : ∀ i : Fin d, p i = q i) : p = q := byd:ℕp:Space dq:Space dh:∀ (i : Fin d), p.val i = q.val i⊢ p = q
  apply eq_of_vald:ℕp:Space dq:Space dh:∀ (i : Fin d), p.val i = q.val i⊢ p.val = q.val
  funext id:ℕp:Space dq:Space dh:∀ (i : Fin d), p.val i = q.val ii:Fin d⊢ p.val i = q.val i
  exact h iAll goals completed! 🐙

B.2. The Non-emptiness

instance {d} : Nonempty (Space d) := Nonempty.intro
  ⟨fun _ => Classical.choice instNonemptyOfInhabited⟩

instance : Subsingleton (Space 0) := Subsingleton.intro <| fun _ _ =>
  eq_of_apply <| fun i => Fin.elim0 i

B.3.1. The additive action

              @[simp]
lemma vadd_val {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
    (v +ᵥ s).val = fun i => v i + s.val i := rfl@[simp]
lemma vadd_apply {d} (v : EuclideanSpace ℝ (Fin d))
    (s : Space d) (i : Fin d) :
    (v +ᵥ s) i = v i + s i := byd:ℕv:EuclideanSpace ℝ (Fin d)s:Space di:Fin d⊢ (v +ᵥ s).val i = v.ofLp i + s.val i rflAll goals completed! 🐙lemma vadd_transitive {d} (s1 s2 : Space d) :
    ∃ v : EuclideanSpace ℝ (Fin d), v +ᵥ s1 = s2 := byd:ℕs1:Space ds2:Space d⊢ ∃ v, v +ᵥ s1 = s2
  use WithLp.toLp 2 fun i => s2 i - s1 ihd:ℕs1:Space ds2:Space d⊢ (WithLp.toLp 2 fun i => s2.val i - s1.val i) +ᵥ s1 = s2
  ext ihd:ℕs1:Space ds2:Space di:Fin d⊢ ((WithLp.toLp 2 fun i => s2.val i - s1.val i) +ᵥ s1).val i = s2.val i
  simpAll goals completed! 🐙

B.3.2. Subtraction

@[simp]
lemma vsub_apply {d} (s1 s2 : Space d) (i : Fin d) :
    (s1 -ᵥ s2) i = s1 i - s2 i := rfl

B.3.3. AddTorsor instance

B.4. PseudoMetricSpace

lemma dist_eq {d} (p q : Space d) : dist p q = √ (∑ i, (p i - q i) ^ 2) := rfl

B.5. NormAddTorsor instance

B.6. Metric space instance

B.7. Non-trivality

instance instNontrivial {d : ℕ} [NeZero d] : Nontrivial (Space d) where
  exists_pair_ne := byd:ℕinst✝:NeZero d⊢ ∃ x y, x ≠ y
    obtain k := Classical.choice Space.instNonemptyd:ℕinst✝:NeZero dk:Space ?m.6⊢ ∃ x y, x ≠ y
    obtain ⟨v1, hv⟩ := exists_ne (0 : EuclideanSpace ℝ (Fin d))d:ℕinst✝:NeZero dk:Space ?m.6v1:EuclideanSpace ℝ (Fin d)hv:v1 ≠ 0⊢ ∃ x y, x ≠ y
    use k, v1 +ᵥ khd:ℕinst✝:NeZero dk:Space dv1:EuclideanSpace ℝ (Fin d)hv:v1 ≠ 0⊢ k ≠ v1 +ᵥ k
    simpa [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symmAll goals completed! 🐙

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

instance (d : ℕ) : IsManifold (𝓡 d) ⊤ (Space d) :=
  (homEuclideanSpaceSpace d).symm.toOpenPartialHomeomorph.isManifold_singleton (byd:ℕ⊢ (homEuclideanSpaceSpace d).symm.toOpenPartialHomeomorph.source = Set.univ simpAll goals completed! 🐙)

lemma chartAt_eq (d : ℕ) (p : Space d) :
    chartAt (EuclideanSpace ℝ (Fin d)) p =
    (homEuclideanSpaceSpace d).symm.toOpenPartialHomeomorph :=
  rfl