Types which depend on dimensions

In addition to types which carry a dimension, we also have types whose elements depend on a choice of a units. For example a function f : M1 → M2 between two types M1 and M2 which carry dimensions does not itself carry a dimensions, but is dependent on a choice of units.

We define three versions

• UnitDependent M having a function scaleUnit : UnitChoices → UnitChoices → M → M subject to two conditions scaleUnit_trans and scaleUnit_id
• LinearUnitDependent M extends UnitDependent M with additional linearity conditions on scaleUnit.
• ContinuousLinearUnitDependent M extends LinearUnitDependent M with an additional continuity condition on scaleUnit.

class UnitDependent (M : Type) : Type

A type carries the instance UnitDependent M if it depends on a choice of units. This dependence is manifested in scaleUnit u1 u2 which describes how elements of M change under a scaling of units which would take u1 to u2.

This type is used for functions, and propositions etc.

• scaleUnit : UnitChoices → UnitChoices → M → M

  scaleUnit u1 u2 is the map transforming elements of M under a scaling of units which would take the unit u1 to the unit u2. This is not to say that in scaleUnit u1 u2 m that m should be interpreted as being in the units u1, although this is often the case.

• scaleUnit_trans (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u2 u3 (scaleUnit u1 u2 m) = scaleUnit u1 u3 m
• scaleUnit_trans' (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u1 u2 (scaleUnit u2 u3 m) = scaleUnit u1 u3 m
• scaleUnit_id (u : UnitChoices) (m : M) : scaleUnit u u m = m

class MulUnitDependent (M : Type) [MulAction NNReal M] extends UnitDependent M : Type

A type M with an instance of UnitDependent M such that scaleUnit u1 u2 is compatible with the MulAction ℝ≥0 M instance on M.

• scaleUnit : UnitChoices → UnitChoices → M → M
• scaleUnit_trans (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u2 u3 (scaleUnit u1 u2 m) = scaleUnit u1 u3 m
• scaleUnit_trans' (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u1 u2 (scaleUnit u2 u3 m) = scaleUnit u1 u3 m
• scaleUnit_id (u : UnitChoices) (m : M) : scaleUnit u u m = m
• scaleUnit_mul (u1 u2 : UnitChoices) (r : NNReal) (m : M) : UnitDependent.scaleUnit u1 u2 (r • m) = r • UnitDependent.scaleUnit u1 u2 m

class LinearUnitDependent (M : Type) [AddCommMonoid M] [Module ℝ M] extends UnitDependent M : Type

A type M with an instance of UnitDependent M such that scaleUnit u1 u2 is compatible with the Module ℝ M instance on M.

• scaleUnit : UnitChoices → UnitChoices → M → M
• scaleUnit_trans (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u2 u3 (scaleUnit u1 u2 m) = scaleUnit u1 u3 m
• scaleUnit_trans' (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u1 u2 (scaleUnit u2 u3 m) = scaleUnit u1 u3 m
• scaleUnit_id (u : UnitChoices) (m : M) : scaleUnit u u m = m
• scaleUnit_add (u1 u2 : UnitChoices) (m1 m2 : M) : UnitDependent.scaleUnit u1 u2 (m1 + m2) = UnitDependent.scaleUnit u1 u2 m1 + UnitDependent.scaleUnit u1 u2 m2
• scaleUnit_smul (u1 u2 : UnitChoices) (r : ℝ) (m : M) : UnitDependent.scaleUnit u1 u2 (r • m) = r • UnitDependent.scaleUnit u1 u2 m

class ContinuousLinearUnitDependent (M : Type) [AddCommMonoid M] [Module ℝ M] [TopologicalSpace M] extends LinearUnitDependent M : Type

A type M with an instance of UnitDependent M such that scaleUnit u1 u2 is compatible with the Module ℝ M instance on M, and is continuous.

• scaleUnit : UnitChoices → UnitChoices → M → M
• scaleUnit_trans (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u2 u3 (scaleUnit u1 u2 m) = scaleUnit u1 u3 m
• scaleUnit_trans' (u1 u2 u3 : UnitChoices) (m : M) : scaleUnit u1 u2 (scaleUnit u2 u3 m) = scaleUnit u1 u3 m
• scaleUnit_id (u : UnitChoices) (m : M) : scaleUnit u u m = m
• scaleUnit_add (u1 u2 : UnitChoices) (m1 m2 : M) : UnitDependent.scaleUnit u1 u2 (m1 + m2) = UnitDependent.scaleUnit u1 u2 m1 + UnitDependent.scaleUnit u1 u2 m2
• scaleUnit_smul (u1 u2 : UnitChoices) (r : ℝ) (m : M) : UnitDependent.scaleUnit u1 u2 (r • m) = r • UnitDependent.scaleUnit u1 u2 m
• scaleUnit_cont (u1 u2 : UnitChoices) : Continuous (UnitDependent.scaleUnit u1 u2)

## Basic properties of scaleUnit

@[simp]

theorem UnitDependent.scaleUnit_symm_apply {M : Type} [UnitDependent M] (u1 u2 : UnitChoices) (m : M) : scaleUnit u2 u1 (scaleUnit u1 u2 m) = m

@[simp]

theorem UnitDependent.scaleUnit_injective {M : Type} [UnitDependent M] (u1 u2 : UnitChoices) (m1 m2 : M) : scaleUnit u1 u2 m1 = scaleUnit u1 u2 m2 ↔ m1 = m2

### Variations on the map scaleUnit

def UnitDependent.scaleUnitEquiv {M : Type} [UnitDependent M] (u1 u2 : UnitChoices) : M ≃ M

For an M with an instance of UnitDependent M, scaleUnit u1 u2 as an equivalence.

Equations

• UnitDependent.scaleUnitEquiv u1 u2 = { toFun := fun (m : M) => UnitDependent.scaleUnit u1 u2 m, invFun := fun (m : M) => UnitDependent.scaleUnit u2 u1 m, left_inv := ⋯, right_inv := ⋯ }

def LinearUnitDependent.scaleUnitLinear {M : Type} [AddCommMonoid M] [Module ℝ M] [LinearUnitDependent M] (u1 u2 : UnitChoices) : M →ₗ[ℝ] M

For an M with an instance of LinearUnitDependent M, scaleUnit u1 u2 as a linear map.

Equations

• LinearUnitDependent.scaleUnitLinear u1 u2 = { toFun := fun (m : M) => UnitDependent.scaleUnit u1 u2 m, map_add' := ⋯, map_smul' := ⋯ }

def LinearUnitDependent.scaleUnitLinearEquiv {M : Type} [AddCommMonoid M] [Module ℝ M] [LinearUnitDependent M] (u1 u2 : UnitChoices) : M ≃ₗ[ℝ] M

For an M with an instance of LinearUnitDependent M, scaleUnit u1 u2 as a linear equivalence.

Equations

• LinearUnitDependent.scaleUnitLinearEquiv u1 u2 = LinearEquiv.ofLinear (LinearUnitDependent.scaleUnitLinear u1 u2) (LinearUnitDependent.scaleUnitLinear u2 u1) ⋯ ⋯

def ContinuousLinearUnitDependent.scaleUnitContLinear {M : Type} [AddCommMonoid M] [Module ℝ M] [TopologicalSpace M] [ContinuousLinearUnitDependent M] (u1 u2 : UnitChoices) : M →L[ℝ] M

For an M with an instance of ContinuousLinearUnitDependent M, scaleUnit u1 u2 as a continuous linear map.

Equations

• ContinuousLinearUnitDependent.scaleUnitContLinear u1 u2 = { toLinearMap := LinearUnitDependent.scaleUnitLinear u1 u2, cont := ⋯ }

def ContinuousLinearUnitDependent.scaleUnitContLinearEquiv {M : Type} [AddCommMonoid M] [Module ℝ M] [TopologicalSpace M] [ContinuousLinearUnitDependent M] (u1 u2 : UnitChoices) : M ≃L[ℝ] M

For an M with an instance of ContinuousLinearUnitDependent M, scaleUnit u1 u2 as a continuous linear equivalence.

Equations

• ContinuousLinearUnitDependent.scaleUnitContLinearEquiv u1 u2 = { toLinearEquiv := LinearUnitDependent.scaleUnitLinearEquiv u1 u2, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_apply {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] [ContinuousLinearUnitDependent M] (u1 u2 : UnitChoices) (m : M) : (scaleUnitContLinearEquiv u1 u2) m = UnitDependent.scaleUnit u1 u2 m

@[simp]

theorem ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_symm_apply {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] [ContinuousLinearUnitDependent M] (u1 u2 : UnitChoices) (m : M) : (scaleUnitContLinearEquiv u1 u2).symm m = UnitDependent.scaleUnit u2 u1 m

Instances of the type classes

We construct instance of the UnitDependent, LinearUnitDependent and ContinuousLinearUnitDependent type classes based on CarriesDimension and functions.

noncomputable instance instUnitDependentUnitChoices : UnitDependent UnitChoices

Equations

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

@[simp]

theorem UnitChoices.scaleUnit_apply_fst (u1 u2 : UnitChoices) : UnitDependent.scaleUnit u1 u2 u1 = u2

@[simp]

theorem UnitChoices.dimScale_scaleUnit {u1 u2 u : UnitChoices} (d : Dimension) : (u.dimScale (UnitDependent.scaleUnit u1 u2 u)) d = (u1.dimScale u2) d

theorem Dimensionful.of_scaleUnit {M : Type} [CarriesDimension M] {u1 u2 u : UnitChoices} (c : Dimensionful M) : ↑c (UnitDependent.scaleUnit u1 u2 u) = (u1.dimScale u2) (dim M) • ↑c u

noncomputable instance instMulUnitDependent {M1 : Type} [CarriesDimension M1] : MulUnitDependent M1

Equations

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

theorem HasDim.scaleUnit_apply {M : Type} [CarriesDimension M] (u1 u2 : UnitChoices) (m : M) : UnitDependent.scaleUnit u1 u2 m = (u1.dimScale u2) (dim M) • m

noncomputable instance instLinearUnitDependentOfHasDim {M : Type} [AddCommMonoid M] [Module ℝ M] [HasDim M] : LinearUnitDependent M

Equations

• instLinearUnitDependentOfHasDim = { toUnitDependent := instMulUnitDependent.toUnitDependent, scaleUnit_add := ⋯, scaleUnit_smul := ⋯ }

noncomputable instance instContinuousLinearUnitDependentOfHasDimOfContinuousConstSMulReal {M : Type} [AddCommMonoid M] [Module ℝ M] [HasDim M] [TopologicalSpace M] [ContinuousConstSMul ℝ M] : ContinuousLinearUnitDependent M

Equations

• instContinuousLinearUnitDependentOfHasDimOfContinuousConstSMulReal = { toLinearUnitDependent := instLinearUnitDependentOfHasDim, scaleUnit_cont := ⋯ }

Functions

noncomputable instance instUnitDependentForall {M1 M2 : Type} [UnitDependent M2] : UnitDependent (M1 → M2)

Equations

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

@[simp]

theorem UnitDependent.scaleUnit_apply_fun_right {M1 M2 : Type} [UnitDependent M2] (u1 u2 : UnitChoices) (f : M1 → M2) (m1 : M1) : scaleUnit u1 u2 f m1 = scaleUnit u1 u2 (f m1)

noncomputable instance instLinearUnitDependentLinearMapRealId {M1 M2 : Type} [AddCommMonoid M1] [Module ℝ M1] [AddCommMonoid M2] [Module ℝ M2] [LinearUnitDependent M2] : LinearUnitDependent (M1 →ₗ[ℝ] M2)

Equations

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

noncomputable instance instContinuousLinearUnitDependentContinuousLinearMapRealId {M1 M2 : Type} [AddCommGroup M1] [Module ℝ M1] [TopologicalSpace M1] [AddCommGroup M2] [Module ℝ M2] [TopologicalSpace M2] [ContinuousConstSMul ℝ M2] [IsTopologicalAddGroup M2] [ContinuousLinearUnitDependent M2] : ContinuousLinearUnitDependent (M1 →L[ℝ] M2)

Equations

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

noncomputable instance instUnitDependentForall_1 {M1 M2 : Type} [UnitDependent M1] : UnitDependent (M1 → M2)

Equations

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

@[simp]

theorem UnitDependent.scaleUnit_apply_fun_left {M1 M2 : Type} [UnitDependent M1] (u1 u2 : UnitChoices) (f : M1 → M2) (m1 : M1) : scaleUnit u1 u2 f m1 = f (scaleUnit u2 u1 m1)

noncomputable instance instUnitDependentTwoSided {M1 M2 : Type} [UnitDependent M1] [UnitDependent M2] : UnitDependent (M1 → M2)

Equations

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

@[simp]

theorem UnitDependent.scaleUnit_apply_fun {M1 M2 : Type} [UnitDependent M1] [UnitDependent M2] (u1 u2 : UnitChoices) (f : M1 → M2) (m1 : M1) : scaleUnit u1 u2 f m1 = scaleUnit u1 u2 (f (scaleUnit u2 u1 m1))

noncomputable instance instUnitDependentTwoSidedMul {M1 M2 : Type} [UnitDependent M1] [MulAction NNReal M2] [MulUnitDependent M2] : MulUnitDependent (M1 → M2)

Equations

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

noncomputable instance instContinuousLinearUnitDependentMap {M1 M2 : Type} [AddCommGroup M1] [Module ℝ M1] [TopologicalSpace M1] [ContinuousLinearUnitDependent M1] [AddCommGroup M2] [Module ℝ M2] [TopologicalSpace M2] [ContinuousConstSMul ℝ M2] [IsTopologicalAddGroup M2] [ContinuousLinearUnitDependent M2] : ContinuousLinearUnitDependent (M1 →L[ℝ] M2)

Equations

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

@[simp]

theorem ContinuousLinearUnitDependent.scaleUnit_apply_fun {M1 M2 : Type} [AddCommGroup M1] [Module ℝ M1] [TopologicalSpace M1] [ContinuousLinearUnitDependent M1] [AddCommGroup M2] [Module ℝ M2] [TopologicalSpace M2] [ContinuousConstSMul ℝ M2] [IsTopologicalAddGroup M2] [ContinuousLinearUnitDependent M2] (u1 u2 : UnitChoices) (f : M1 →L[ℝ] M2) (m1 : M1) : (UnitDependent.scaleUnit u1 u2 f) m1 = UnitDependent.scaleUnit u1 u2 (f (UnitDependent.scaleUnit u2 u1 m1))

isDimensionallyCorrect

def IsDimensionallyCorrect {M : Type} [UnitDependent M] (m : M) : Prop

A term of type M carrying an instance of UnitDependent M is said to be dimensionally correct if under a change of units it remains the same.

More colloquially, something is dimensionally correct if it (e.g. it's value or its truth for a proposition) does not depend on the units it is written in.

For the case of m : M with CarriesDimension M then IsDimensionallyCorrect m corresponds to the statement that m does not depend on units, e.g. is zero or the dimension of M is zero.

Equations

• IsDimensionallyCorrect m = ∀ (u1 u2 : UnitChoices), UnitDependent.scaleUnit u1 u2 m = m

theorem isDimensionallyCorrect_iff {M : Type} [UnitDependent M] (m : M) : IsDimensionallyCorrect m ↔ ∀ (u1 u2 : UnitChoices), UnitDependent.scaleUnit u1 u2 m = m

@[simp]

theorem isDimensionallyCorrect_fun_iff {M1 M2 : Type} [UnitDependent M1] [UnitDependent M2] {f : M1 → M2} : IsDimensionallyCorrect f ↔ ∀ (u1 u2 : UnitChoices) (m : M1), UnitDependent.scaleUnit u1 u2 (f (UnitDependent.scaleUnit u2 u1 m)) = f m

@[simp]

theorem isDimensionallyCorrect_fun_left {M1 M2 : Type} [UnitDependent M1] {f : M1 → M2} : IsDimensionallyCorrect f ↔ ∀ (u1 u2 : UnitChoices) (m : M1), f (UnitDependent.scaleUnit u2 u1 m) = f m

@[simp]

theorem isDimensionallyCorrect_fun_right {M1 M2 : Type} [UnitDependent M2] {f : M1 → M2} : IsDimensionallyCorrect f ↔ ∀ (u1 u2 : UnitChoices) (m : M1), UnitDependent.scaleUnit u1 u2 (f m) = f m

Some type classes to help track dimensions

class DMul (M1 M2 M3 : Type) [CarriesDimension M1] [CarriesDimension M2] [CarriesDimension M3] extends HMul M1 M2 M3 : Type

The multiplication of an element of M1 with an element of M2 to get an element of M3 in such a way that dimensions are preserved.

• hMul : M1 → M2 → M3
• mul_dim (m1 : Dimensionful M1) (m2 : Dimensionful M2) : HasDimension fun (u : UnitChoices) => ↑m1 u * ↑m2 u

@[simp]

theorem DMul.hMul_scaleUnit {M1 M2 M3 : Type} [CarriesDimension M1] [CarriesDimension M2] [CarriesDimension M3] [DMul M1 M2 M3] (m1 : M1) (m2 : M2) (u1 u2 : UnitChoices) : UnitDependent.scaleUnit u1 u2 m1 * UnitDependent.scaleUnit u1 u2 m2 = UnitDependent.scaleUnit u1 u2 (m1 * m2)

Dim Subtype

def DimSet (M : Type) [MulAction NNReal M] [MulUnitDependent M] (d : Dimension) : Set M

Given a type M that depends on units, e.g. the function type M1 → M2 between two types carrying a dimension, the subtype of M which scales according to the dimension d.

Equations

• DimSet M d = {m : M | ∀ (u1 u2 : UnitChoices), UnitDependent.scaleUnit u1 u2 m = (u1.dimScale u2) d • m}

instance instMulActionNNRealElemDimSet (M : Type) [MulAction NNReal M] [MulUnitDependent M] (d : Dimension) : MulAction NNReal ↑(DimSet M d)

Equations

• instMulActionNNRealElemDimSet M d = { smul := fun (a : NNReal) (f : ↑(DimSet M d)) => ⟨a • ↑f, ⋯⟩, one_smul := ⋯, mul_smul := ⋯ }

instance instCarriesDimensionElemDimSet (M : Type) [MulAction NNReal M] [MulUnitDependent M] (d : Dimension) : CarriesDimension ↑(DimSet M d)

Equations

• instCarriesDimensionElemDimSet M d = { d := d, toMulAction := instMulActionNNRealElemDimSet M d }

@[simp]

theorem scaleUnit_dimSet_val {M : Type} [MulAction NNReal M] [MulUnitDependent M] (d : Dimension) (m : ↑(DimSet M d)) (u1 u2 : UnitChoices) : ↑(UnitDependent.scaleUnit u1 u2 m) = UnitDependent.scaleUnit u1 u2 ↑m

theorem DimSet.mem_iff {M : Type} [MulAction NNReal M] [MulUnitDependent M] (d : Dimension) (m : M) : m ∈ DimSet M d ↔ ∀ (u1 u2 : UnitChoices), UnitDependent.scaleUnit u1 u2 m = (u1.dimScale u2) d • m