Space

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

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.

The Space type

@[reducible, inline]

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

The type Space d representes d dimensional Euclidean space. The default value of d is 3. Thus Space = Space 3.

Equations

• Space d = EuclideanSpace ℝ (Fin d)

Basic operations on Space.

Instances on Space

Inner product

theorem Space.inner_eq_sum {d : ℕ} (p q : Space d) : inner ℝ p q = ∑ i : Fin d, p i * q i

Basis

noncomputable def Space.basis {d : ℕ} : OrthonormalBasis (Fin d) ℝ (Space d)

The standard basis of Space based on Fin d.

Equations

• Space.basis = EuclideanSpace.basisFun (Fin d) ℝ

theorem Space.basis_apply {d : ℕ} (i j : Fin d) : basis i j = if i = j then 1 else 0

@[simp]

theorem Space.basis_self {d : ℕ} (i : Fin d) : basis i i = 1

@[simp]

theorem Space.basis_repr {d : ℕ} (p : Space d) : basis.repr p = p

@[simp]

theorem Space.inner_basis {d : ℕ} (p : Space d) (i : Fin d) : inner ℝ p (basis i) = p i

@[simp]

theorem Space.basis_inner {d : ℕ} (i : Fin d) (p : Space d) : inner ℝ (basis i) p = p i

Coordinates

noncomputable def Space.coord {d : ℕ} (μ : Fin d) (p : Space d) : ℝ

The standard coordinate functions of Space based on Fin d.

The notation 𝔁 μ p can be used for this.

Equations

• Space.coord μ p = inner ℝ p (Space.basis μ)

theorem Space.coord_apply {d : ℕ} (μ : Fin d) (p : Space d) : coord μ p = p μ

noncomputable def Space.coordCLM {d : ℕ} (μ : Fin d) : Space d →L[ℝ] ℝ

The standard coordinate functions of Space based on Fin d, as a continuous linear map.

Equations

• Space.coordCLM μ = { toFun := Space.coord μ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem Space.coord_contDiff {d : ℕ} {i : Fin d} : ContDiff ℝ ↑⊤ fun (x : Space d) => coord i x

theorem Space.coordCLM_apply {d : ℕ} (μ : Fin d) (p : Space d) : (coordCLM μ) p = coord μ p

def Space.term𝔁 : Lean.ParserDescr

The standard coordinate functions of Space based on Fin d.

The notation 𝔁 μ p can be used for this.

Equations

• Space.term𝔁 = Lean.ParserDescr.node `Space.term𝔁 1024 (Lean.ParserDescr.symbol "𝔁")

Derivatives

noncomputable def Space.deriv {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (μ : Fin d) (f : Space d → M) : Space d → M

Given a function f : Space d → M the derivative of f in direction μ.

Equations

• Space.deriv μ f x = (fderiv ℝ f x) (EuclideanSpace.single μ 1)

def Space.«term∂[_]» : Lean.ParserDescr

Given a function f : Space d → M the derivative of f in direction μ.

Equations

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

theorem Space.deriv_eq {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (μ : Fin d) (f : Space d → M) (x : Space d) : deriv μ f x = (fderiv ℝ f x) (EuclideanSpace.single μ 1)

theorem Space.deriv_eq_fderiv_basis {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (μ : Fin d) (f : Space d → M) (x : Space d) : deriv μ f x = (fderiv ℝ f x) (basis μ)

Gradient

noncomputable def Space.grad {d : ℕ} (f : Space d → ℝ) : Space d → EuclideanSpace ℝ (Fin d)

The vector calculus operator grad.

Equations

• Space.grad f x i = Space.deriv i f x

def Space.«term∇» : Lean.ParserDescr

The vector calculus operator grad.

Equations

• Space.«term∇» = Lean.ParserDescr.node `Space.«term∇» 1024 (Lean.ParserDescr.symbol "∇")

Curl

noncomputable def Space.curl (f : Space → EuclideanSpace ℝ (Fin 3)) : Space → EuclideanSpace ℝ (Fin 3)

The vector calculus operator curl.

Equations

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

def Space.curlNotation : Lean.ParserDescr

The vector calculus operator curl.

Equations

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

Div

noncomputable def Space.div {d : ℕ} (f : Space d → EuclideanSpace ℝ (Fin d)) : Space d → ℝ

The vector calculus operator div.

Equations

• Space.div f x = ∑ i : Fin d, (fun (i : Fin d) (x : Space d) => Space.deriv i ((fun (i : Fin d) (x : Space d) => Space.coord i (f x)) i) x) i x

def Space.divNotation : Lean.ParserDescr

The vector calculus operator div.

Equations

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

Laplacians

noncomputable def Space.laplacian {d : ℕ} (f : Space d → ℝ) : Space d → ℝ

The scalar laplacian operator.

Equations

• Space.laplacian f x = ∑ i : Fin d, (fun (i : Fin d) (x : Space d) => Space.deriv i (Space.deriv i f) x) i x

def Space.termΔ : Lean.ParserDescr

The scalar laplacian operator.

Equations

• Space.termΔ = Lean.ParserDescr.node `Space.termΔ 1024 (Lean.ParserDescr.symbol "Δ")

noncomputable def Space.laplacianVec {d : ℕ} (f : Space d → EuclideanSpace ℝ (Fin d)) : Space d → EuclideanSpace ℝ (Fin d)

The vector laplacianVec operator.

Equations

• Space.laplacianVec f x i = Space.laplacian ((fun (i : Fin d) (x : Space d) => Space.coord i (f x)) i) x

def Space.termΔ_1 : Lean.ParserDescr

The vector laplacianVec operator.

Equations

• Space.termΔ_1 = Lean.ParserDescr.node `Space.termΔ_1 1024 (Lean.ParserDescr.symbol "Δ")

Directions

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

Notion of direction where unit returns a unit vector in the direction specified.

• unit : EuclideanSpace ℝ (Fin d)

  Unit vector specifying the direction.

• norm : ‖self.unit‖ = 1

noncomputable def Space.toDirection {d : ℕ} (x : Space d) (h : x ≠ 0) : Direction d

Direction of a Space value with respect to the origin.

Equations

• x.toDirection h = { unit := ‖x‖⁻¹ • x, norm := ⋯ }

One equiv

noncomputable def Space.oneEquiv : Space 1 ≃ₗᵢ[ℝ] ℝ

The linear isometric equivalence between Space 1 and ℝ.

Equations

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

theorem Space.oneEquiv_coe : ⇑oneEquiv = fun (x : Space 1) => x 0

theorem Space.oneEquiv_symm_coe : ⇑oneEquiv.symm = fun (x : ℝ) (x_1 : Fin 1) => x

theorem Space.oneEquiv_symm_apply (x : ℝ) (i : Fin 1) : oneEquiv.symm x i = x

theorem Space.oneEquiv_continuous : Continuous ⇑oneEquiv

theorem Space.oneEquiv_symm_continuous : Continuous ⇑oneEquiv.symm

noncomputable def Space.oneEquivCLE : EuclideanSpace ℝ (Fin 1) ≃L[ℝ] ℝ

The continuous linear equivalence between Space 1 and ℝ.

Equations

• Space.oneEquivCLE = { toLinearEquiv := ↑Space.oneEquiv, continuous_toFun := Space.oneEquivCLE._proof_2, continuous_invFun := Space.oneEquivCLE._proof_3 }

theorem Space.oneEquiv_measurableEmbedding : MeasurableEmbedding ⇑oneEquiv

theorem Space.oneEquiv_symm_measurableEmbedding : MeasurableEmbedding ⇑oneEquiv.symm

theorem Space.oneEquiv_measurePreserving : MeasureTheory.MeasurePreserving (⇑oneEquiv) MeasureTheory.volume MeasureTheory.volume

theorem Space.oneEquiv_symm_measurePreserving : MeasureTheory.MeasurePreserving (⇑oneEquiv.symm) MeasureTheory.volume MeasureTheory.volume