Space

This file contains d-dimensional space.

Note on implementation

The definition of Space d currently inherits all instances of EuclideanSpace ℝ (Fin d).

This, in particular, automatically equips Space d with a norm. This norm induces a metric on Space d which is the standard Euclidean metric. Thus Space d automatically corresponds to flat space.

The definition of deriv through fderiv explicitly uses this metric.

Space d also inherits instances of EuclideanSpace ℝ (Fin d) such as a zero vector, the ability to add two space positions etc, which are not really allowed operations on Space d.

@[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)

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) ℝ

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 μ)

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 "𝔁")

Calculus

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)

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)

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.

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 "∇")

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.

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.

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.laplacian_vec {d : ℕ} (f : Space d → EuclideanSpace ℝ (Fin d)) : Space d → EuclideanSpace ℝ (Fin d)

The vector laplacian_vec operator.

Equations

• Space.laplacian_vec 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 laplacian_vec operator.

Equations

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

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 := ⋯ }