SpaceStruct d

This is a work in progress reimplementation of Space d that abstracts over the underlying EuclideanSpace

Space d is planned to be deprecated in favor of SpaceStruct d. Once the necessary components are migrated to be compatible with SpaceStruct, it will become the default implementation of Space

structure SpaceStruct (d : ℕ := 3) : Type

The type SpaceStruct d represents d dimensional Euclidean space. The default value of d is 3. Thus SpaceStuct = Spacestruct 3.

• val : EuclideanSpace ℝ (Fin d)

  The underlying EuclideanSpace associated SpaceStruct d

Basic operations on Space.

noncomputable instance instAddSpaceStruct {d : ℕ} : Add (SpaceStruct d)

Equations

• instAddSpaceStruct = { add := fun (x y : SpaceStruct d) => { val := x.val + y.val } }

@[simp]

theorem add_val {d : ℕ} (x y : SpaceStruct d) : x + y = { val := x.val + y.val }

instance instNegSpaceStruct {d : ℕ} : Neg (SpaceStruct d)

Equations

• instNegSpaceStruct = { neg := fun (x : SpaceStruct d) => { val := -x.val } }

@[simp]

theorem neg_val {d : ℕ} (x : SpaceStruct d) : (-x).val = -x.val

noncomputable instance instSubSpaceStruct {d : ℕ} : Sub (SpaceStruct d)

Equations

• instSubSpaceStruct = { sub := fun (x y : SpaceStruct d) => { val := x.val - y.val } }

instance instSMulRealSpaceStruct {d : ℕ} : SMul ℝ (SpaceStruct d)

Equations

• instSMulRealSpaceStruct = { smul := fun (k : ℝ) (x : SpaceStruct d) => { val := k • x.val } }

instance instZeroSpaceStruct {d : ℕ} : Zero (SpaceStruct d)

Equations

• instZeroSpaceStruct = { zero := { val := 0 } }

noncomputable instance instInnerRealSpaceStruct (d : ℕ) : Inner ℝ (SpaceStruct d)

Equations

• instInnerRealSpaceStruct d = { inner := fun (x y : SpaceStruct d) => inner ℝ x.val y.val }

noncomputable instance instVAddEuclideanSpaceRealFinSpaceStruct {d : ℕ} : VAdd (EuclideanSpace ℝ (Fin d)) (SpaceStruct d)

Equations

• instVAddEuclideanSpaceRealFinSpaceStruct = { vadd := fun (v : EuclideanSpace ℝ (Fin d)) (s : SpaceStruct d) => { val := v + s.val } }

Instances on Space

noncomputable instance instAddGroupSpaceStruct {d : ℕ} : AddGroup (SpaceStruct d)

Equations

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

noncomputable instance instAddCommMonoidSpaceStruct {d : ℕ} : AddCommMonoid (SpaceStruct d)

Equations

• instAddCommMonoidSpaceStruct = { toAddMonoid := instAddGroupSpaceStruct.toAddMonoid, add_comm := ⋯ }

noncomputable instance instAddCommGroupSpaceStruct {d : ℕ} : AddCommGroup (SpaceStruct d)

Equations

• instAddCommGroupSpaceStruct = { toAddGroup := instAddGroupSpaceStruct, add_comm := ⋯ }

Inner product

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