The structure of a module on Space #

The scope of this module is to define on Space d the structure of a Module (aka vector space), a Norm and an InnerProductSpace, and give properties of these structures.

These instances require certain non-canonical choices to be made, for example the choice of a zero and for a basis, a choice of orientation.

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

source

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

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

source

@[simp]

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

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

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

@[simp]

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

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

source

instance Space.instModuleReal {d : ℕ} :

Module ℝ (Space d)

Equations

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

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

theorem Space.point_dim_zero_eq (p : Space 0) :

p = 0

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

Space.instSeminormedAddCommGroup = { toNorm := Space.instNorm, toAddCommGroup := Space.instAddCommGroup, toPseudoMetricSpace := Space.instPseudoMetricSpace, dist_eq := ⋯ }

source

@[simp]

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

dist p q = ‖p - q‖

source

noncomputable instance Space.instNormedAddCommGroup {d : ℕ} :

NormedAddCommGroup (Space d)

Equations

Space.instNormedAddCommGroup = { toNorm := Space.instNorm, toAddCommGroup := Space.instAddCommGroup, toMetricSpace := Space.instMetricSpace, dist_eq := ⋯ }

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.

A.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 continuous 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_1, continuous_invFun := Space.oneEquivCLE._proof_2 }

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

PhysLean Documentation

PhysLean.SpaceAndTime.Space.Module

The structure of a module on Space #

A.1. Instance of an additive commutative monoid #

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

A.3. Instance of an inner product space #

A.4. Instance of a measurable space #

The norm on `Space` #

Inner product #

Basis #

Coordinates #

Directions #

One equiv #

The structure of a module on Space #

A.1. Instance of an additive commutative monoid #

A.2. Instance of a module over ℝ #

A.3. Instance of an inner product space #

A.4. Instance of a measurable space #

The norm on Space #

Inner product #

Basis #

Coordinates #

Directions #

One equiv #

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

The norm on `Space` #