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 #

source

structure Space (d : ℕ := 3) :

Type

The type Space d represents d dimensional Euclidean space. 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.

Instances For

source

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

p = q

source

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

source

instance Space.instCoeFunForallFinReal {d : ℕ} :

CoeFun (Space d) fun (x : Space d) => Fin d → ℝ

Equations

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

source

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

p = q

source

theorem Space.eq_of_apply_iff {d : ℕ} {p q : Space d} :

p = q ↔ ∀ (i : Fin d), p.val i = q.val i

B.1. Instance of an additive commutative monoid #

source

instance Space.instAdd {d : ℕ} :

Add (Space d)

Equations

Space.instAdd = { add := fun (p q : Space d) => { val := fun (i : Fin d) => p.val i + q.val i } }

source

@[simp]

theorem Space.add_val {d : ℕ} (x y : Space d) :

(x + y).val = x.val + y.val

source

@[simp]

theorem Space.add_apply {d : ℕ} (x y : Space d) (i : Fin d) :

(x + y).val i = x.val i + y.val i

source

instance Space.instZero {d : ℕ} :

Zero (Space d)

Equations

Space.instZero = { zero := { val := fun (x : Fin d) => 0 } }

source

@[simp]

theorem Space.zero_val {d : ℕ} :

val 0 = fun (x : Fin d) => 0

source

@[simp]

theorem Space.zero_apply {d : ℕ} (i : Fin d) :

val 0 i = 0

source

instance Space.instAddCommMonoid {d : ℕ} :

AddCommMonoid (Space d)

Equations

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

source

@[simp]

theorem Space.nsmul_val {d : ℕ} (n : ℕ) (a : Space d) :

(n • a).val = fun (i : Fin d) => n • a.val i

source

@[simp]

theorem Space.nsmul_apply {d : ℕ} (n : ℕ) (a : Space d) (i : Fin d) :

(n • a).val i = n • a.val i

B.2. Instance of a module over `ℝ` #

source

instance Space.instSMulReal {d : ℕ} :

SMul ℝ (Space d)

Equations

Space.instSMulReal = { smul := fun (c : ℝ) (p : Space d) => { val := fun (i : Fin d) => c * p.val i } }

source

@[simp]

theorem Space.smul_val {d : ℕ} (c : ℝ) (p : Space d) :

(c • p).val = fun (i : Fin d) => c * p.val i

source

@[simp]

theorem Space.smul_apply {d : ℕ} (c : ℝ) (p : Space d) (i : Fin d) :

(c • p).val i = c * p.val i

source

instance Space.instModuleReal {d : ℕ} :

Module ℝ (Space d)

Equations

Space.instModuleReal = { toSMul := Space.instSMulReal, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

B.3. Addition of Euclidean spaces #

source

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 } }

source

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

source

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

source

theorem Space.vadd_transitive {d : ℕ} (s1 s2 : Space d) :

∃ (v : EuclideanSpace ℝ (Fin d)), v +ᵥ s1 = s2

source

theorem Space.eq_vadd_zero {d : ℕ} (s : Space d) :

∃ (v : EuclideanSpace ℝ (Fin d)), s = v +ᵥ 0

source

@[simp]

theorem Space.smul_vadd_zero {d : ℕ} (k : ℝ) (v : EuclideanSpace ℝ (Fin d)) :

k • (v +ᵥ 0) = k • v +ᵥ 0

source

noncomputable instance Space.instAddActionEuclideanSpaceRealFin {d : ℕ} :

AddAction (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

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

source

@[simp]

theorem Space.add_vadd_zero {d : ℕ} (v1 v2 : EuclideanSpace ℝ (Fin d)) :

(v1 +ᵥ 0) + (v2 +ᵥ 0) = (v1 + v2) +ᵥ 0

B.3. Instance of an inner product space #

source

noncomputable instance Space.instNorm {d : ℕ} :

Norm (Space d)

Equations

Space.instNorm = { norm := fun (p : Space d) => √(∑ i : Fin d, p.val i ^ 2) }

source

theorem Space.norm_eq {d : ℕ} (p : Space d) :

‖p‖ = √(∑ i : Fin d, p.val i ^ 2)

source

@[simp]

theorem Space.abs_eval_le_norm {d : ℕ} (p : Space d) (i : Fin d) :

|p.val i| ≤ ‖p‖

source

theorem Space.norm_sq_eq {d : ℕ} (p : Space d) :

‖p‖ ^ 2 = ∑ i : Fin d, p.val i ^ 2

source

@[simp]

theorem Space.norm_vadd_zero {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) :

‖v +ᵥ 0‖ = ‖v‖

source

instance Space.instNeg {d : ℕ} :

Neg (Space d)

Equations

Space.instNeg = { neg := fun (p : Space d) => { val := fun (i : Fin d) => -p.val i } }

source

@[simp]

theorem Space.neg_val {d : ℕ} (p : Space d) :

(-p).val = fun (i : Fin d) => -p.val i

source

@[simp]

theorem Space.neg_apply {d : ℕ} (p : Space d) (i : Fin d) :

(-p).val i = -p.val i

source

noncomputable instance Space.instAddCommGroup {d : ℕ} :

AddCommGroup (Space d)

Equations

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

source

@[simp]

theorem Space.sub_apply {d : ℕ} (p q : Space d) (i : Fin d) :

(p - q).val i = p.val i - q.val i

source

@[simp]

theorem Space.sub_val {d : ℕ} (p q : Space d) :

(p - q).val = fun (i : Fin d) => p.val i - q.val i

source

@[simp]

theorem Space.vadd_zero_sub_vadd_zero {d : ℕ} (v1 v2 : EuclideanSpace ℝ (Fin d)) :

(v1 +ᵥ 0) - (v2 +ᵥ 0) = (v1 - v2) +ᵥ 0

source

noncomputable instance Space.instSeminormedAddCommGroup {d : ℕ} :

SeminormedAddCommGroup (Space d)

Equations

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

source

@[simp]

theorem Space.dist_eq {d : ℕ} (p q : Space d) :

dist p q = ‖p - q‖

source

noncomputable instance Space.instNormedAddCommGroup {d : ℕ} :

NormedAddCommGroup (Space d)

Equations

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

source

instance Space.instInnerReal {d : ℕ} :

Inner ℝ (Space d)

Equations

Space.instInnerReal = { inner := fun (p q : Space d) => ∑ i : Fin d, p.val i * q.val i }

source

@[simp]

theorem Space.inner_vadd_zero {d : ℕ} (v1 v2 : EuclideanSpace ℝ (Fin d)) :

inner ℝ (v1 +ᵥ 0) (v2 +ᵥ 0) = inner ℝ v1 v2

source

theorem Space.inner_apply {d : ℕ} (p q : Space d) :

inner ℝ p q = ∑ i : Fin d, p.val i * q.val i

source

instance Space.instInnerProductSpaceReal {d : ℕ} :

InnerProductSpace ℝ (Space d)

Equations

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

B.4. Instance of a measurable space #

source

instance Space.instMeasurableSpace {d : ℕ} :

MeasurableSpace (Space d)

Equations

Space.instMeasurableSpace = borel (Space d)

source

instance Space.instBorelSpace {d : ℕ} :

BorelSpace (Space d)

The norm on `Space` #

Inner product #

source

theorem Space.inner_eq_sum {d : ℕ} (p q : Space d) :

inner ℝ p q = ∑ i : Fin d, p.val i * q.val i

source

@[simp]

theorem Space.sum_apply {d : ℕ} {ι : Type} [Fintype ι] (f : ι → Space d) (i : Fin d) :

(∑ x : ι, f x).val i = ∑ x : ι, (f x).val i

Basis #

source

noncomputable def Space.basis {d : ℕ} :

OrthonormalBasis (Fin d) ℝ (Space d)

The standard basis of Space based on Fin d.

Equations

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

Instances For

source

theorem Space.apply_eq_basis_repr_apply {d : ℕ} (p : Space d) (i : Fin d) :

p.val i = (basis.repr p).ofLp i

source

@[simp]

theorem Space.basis_repr_apply {d : ℕ} (p : Space d) (i : Fin d) :

(basis.repr p).ofLp i = p.val i

source

@[simp]

theorem Space.basis_repr_symm_apply {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (i : Fin d) :

(basis.repr.symm v).val i = v.ofLp i

source

theorem Space.basis_apply {d : ℕ} (i j : Fin d) :

(basis i).val j = if i = j then 1 else 0

source

@[simp]

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

(basis i).val i = 1

source

@[simp]

theorem Space.inner_basis {d : ℕ} (p : Space d) (i : Fin d) :

inner ℝ p (basis i) = p.val i

source

@[simp]

theorem Space.basis_inner {d : ℕ} (i : Fin d) (p : Space d) :

inner ℝ (basis i) p = p.val i

source

theorem Space.basis_repr_inner_eq {d : ℕ} (p : Space d) (v : EuclideanSpace ℝ (Fin d)) :

inner ℝ (basis.repr p) v = inner ℝ p (basis.repr.symm v)

source

instance Space.instFiniteDimensionalReal {d : ℕ} :

FiniteDimensional ℝ (Space d)

source

@[simp]

theorem Space.finrank_eq_dim {d : ℕ} :

Module.finrank ℝ (Space d) = d

source

@[simp]

theorem Space.rank_eq_dim {d : ℕ} :

Module.rank ℝ (Space d) = ↑d

source

@[simp]

theorem Space.fderiv_basis_repr {d : ℕ} (p : Space d) :

fderiv ℝ (⇑basis.repr) p = LinearMap.toContinuousLinearMap ↑basis.repr.toLinearEquiv

source

@[simp]

theorem Space.fderiv_basis_repr_symm {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) :

fderiv ℝ (⇑basis.repr.symm) v = LinearMap.toContinuousLinearMap ↑basis.repr.symm.toLinearEquiv

Coordinates #

source

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

Instances For

source

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

coord μ p = p.val μ

source

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

Instances For

source

theorem Space.coord_contDiff {d : ℕ} {i : Fin d} :

ContDiff ℝ ↑⊤ fun (x : Space d) => coord i x

source

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

(coordCLM μ) p = coord μ p

source

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

Instances For

source

theorem Space.eval_continuous {d : ℕ} (i : Fin d) :

Continuous fun (p : Space d) => p.val i

source

theorem Space.eval_differentiable {d : ℕ} (i : Fin d) :

Differentiable ℝ fun (p : Space d) => p.val i

source

theorem Space.eval_contDiff {d : ℕ} {n : WithTop ℕ∞} (i : Fin d) :

ContDiff ℝ n fun (p : Space d) => p.val i

source

def Space.equivPi (d : ℕ) :

Space d ≃L[ℝ ] Fin d → ℝ

The continous linear equivalence between Space d and the corresponding Pi type.

Equations

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

Instances For

source

theorem Space.mk_continuous {d : ℕ} :

Continuous fun (f : Fin d → ℝ) => { val := f }

source

theorem Space.mk_differentiable {d : ℕ} :

Differentiable ℝ fun (f : Fin d → ℝ) => { val := f }

source

theorem Space.mk_contDiff {d n : ℕ} :

ContDiff ℝ ↑n fun (f : Fin d → ℝ) => { val := f }

source

@[simp]

theorem Space.fderiv_mk {d : ℕ} (f : Fin d → ℝ) :

fderiv ℝ mk f = ↑(equivPi d).symm

source

@[simp]

theorem Space.fderiv_val {d : ℕ} (p : Space d) :

fderiv ℝ val p = ↑(equivPi d)

Directions #

source

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

Type

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

unit : Space d
Unit vector specifying the direction.
norm : ‖self.unit‖ = 1

Instances For

source

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

Instances For

source

@[simp]

theorem Space.direction_unit_sq_sum {d : ℕ} (s : Direction d) :

∑ i : Fin d, s.unit.val i ^ 2 = 1

One equiv #

source

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.

Instances For

source

theorem Space.oneEquiv_coe :

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

source

theorem Space.oneEquiv_symm_coe :

⇑oneEquiv.symm = fun (x : ℝ) => { val := fun (x_1 : Fin 1) => x }

source

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

(oneEquiv.symm x).val i = x

source

theorem Space.oneEquiv_continuous :

Continuous ⇑oneEquiv

source

theorem Space.oneEquiv_symm_continuous :

Continuous ⇑oneEquiv.symm

source

noncomputable def Space.oneEquivCLE :

Space 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 }

Instances For

source

theorem Space.oneEquiv_measurableEmbedding :

MeasurableEmbedding ⇑oneEquiv

source

theorem Space.oneEquiv_symm_measurableEmbedding :

MeasurableEmbedding ⇑oneEquiv.symm

source

theorem Space.oneEquiv_measurePreserving :

MeasureTheory.MeasurePreserving (⇑oneEquiv) MeasureTheory.volume MeasureTheory.volume

source

theorem Space.oneEquiv_symm_measurePreserving :

MeasureTheory.MeasurePreserving (⇑oneEquiv.symm) MeasureTheory.volume MeasureTheory.volume

source

theorem Space.volume_eq_addHaar {d : ℕ} :

MeasureTheory.volume = basis.toBasis.addHaar

source

@[simp]

theorem Space.volume_metricBall_three :

MeasureTheory.volume (Metric.ball 0 1) = ENNReal.ofReal (4 / 3 * Real.pi)

source

instance Space.instNontrivialSucc {d : ℕ} :

Nontrivial (Space d.succ)

source

instance Space.instSubsingletonOfNatNat :

Subsingleton (Space 0)

source

theorem Space.volume_closedBall_neq_zero {d : ℕ} (x : Space d.succ) (r : ℝ) (hr : 0 < r) :

MeasureTheory.volume (Metric.closedBall x r) ≠ 0

source

theorem Space.volume_closedBall_neq_top {d : ℕ} (x : Space d.succ) (r : ℝ) :

MeasureTheory.volume (Metric.closedBall x r) ≠ ⊤

PhysLean Documentation

PhysLean.SpaceAndTime.Space.Basic

Space #

The `Space` type #

B. Instances on `Space` #

B.1. Instance of coercion to functions #

B.1. Instance of an additive commutative monoid #

B.2. Instance of a module over `ℝ` #

B.3. Addition of Euclidean spaces #

B.3. Instance of an inner product space #

B.4. Instance of a measurable space #

The norm on `Space` #

Inner product #

Basis #

Coordinates #

Directions #

One equiv #

Space #

The Space type #

B. Instances on Space #

B.1. Instance of coercion to functions #

B.1. Instance of an additive commutative monoid #

B.2. Instance of a module over ℝ #

B.3. Addition of Euclidean spaces #

B.3. Instance of an inner product space #

B.4. Instance of a measurable space #

The norm on Space #

Inner product #

Basis #

Coordinates #

Directions #

One equiv #

The `Space` type #

B. Instances on `Space` #

B.2. Instance of a module over `ℝ` #

The norm on `Space` #