Dimensions and unit

A unit in physics arises from choice of something in physics which is non-canonical. An example is the choice of translationally-invariant metric on the time manifold TimeMan.

A dimension is a property of a quantity related to how it changes with respect to a change in the unit.

The fundamental choices one has in physics are related to:

• Time
• Length
• Mass
• Charge
• Temperature

(In fact temperature is not really a fundamental choice, however we leave this as a TODO.)

From these fundamental choices one can construct all other units and dimensions.

Implementation details

Units within PhysLean are implemented with the following convention:

• The fundamental units, and the choices they correspond to, are defined within the appropriate physics directory, in particular:
  • PhysLean/SpaceAndTime/Time/TimeUnit.lean
  • PhysLean/SpaceAndTime/Space/LengthUnit.lean
  • PhysLean/ClassicalMechanics/Mass/MassUnit.lean
  • PhysLean/Electromagnetism/Charge/ChargeUnit.lean
  • PhysLean/Thermodynamics/Temperature/TemperatureUnit.lean
• In this Units directory, we define the necessary structures and properties to work derived units and dimensions.

References

Zulip chats discussing units:

• https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/physical.20units
• https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Dimensional.20Analysis.20Revisited/with/530238303

Note

A lot of the results around units is still experimental and should be adapted based on needs.

Defining dimensions

structure Dimension : Type

The foundational dimensions. Defined in the order ⟨length, time, mass, charge, temperature⟩

• length : ℚ

  The length dimension.

• time : ℚ

  The time dimension.

• mass : ℚ

  The mass dimension.

• charge : ℚ

  The charge dimension.

• temperature : ℚ

  The temperature dimension.

instance Dimension.instZero : Zero Dimension

Equations

• Dimension.instZero = { zero := { length := 0, time := 0, mass := 0, charge := 0, temperature := 0 } }

theorem Dimension.zero_eq : 0 = { length := 0, time := 0, mass := 0, charge := 0, temperature := 0 }

instance Dimension.instMul : Mul Dimension

Equations

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

@[simp]

theorem Dimension.time_mul (d1 d2 : Dimension) : (d1 * d2).time = d1.time + d2.time

@[simp]

theorem Dimension.length_mul (d1 d2 : Dimension) : (d1 * d2).length = d1.length + d2.length

@[simp]

theorem Dimension.mass_mul (d1 d2 : Dimension) : (d1 * d2).mass = d1.mass + d2.mass

@[simp]

theorem Dimension.charge_mul (d1 d2 : Dimension) : (d1 * d2).charge = d1.charge + d2.charge

@[simp]

theorem Dimension.temperature_mul (d1 d2 : Dimension) : (d1 * d2).temperature = d1.temperature + d2.temperature

instance Dimension.instInv : Inv Dimension

Equations

• Dimension.instInv = { inv := fun (d : Dimension) => { length := -d.length, time := -d.time, mass := -d.mass, charge := -d.charge, temperature := -d.temperature } }

@[simp]

theorem Dimension.inv_length (d : Dimension) : d⁻¹.length = -d.length

@[simp]

theorem Dimension.inv_time (d : Dimension) : d⁻¹.time = -d.time

@[simp]

theorem Dimension.inv_mass (d : Dimension) : d⁻¹.mass = -d.mass

@[simp]

theorem Dimension.inv_charge (d : Dimension) : d⁻¹.charge = -d.charge

@[simp]

theorem Dimension.inv_temperature (d : Dimension) : d⁻¹.temperature = -d.temperature

instance Dimension.instPowRat : Pow Dimension ℚ

Equations

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

def Dimension.L𝓭 : Dimension

The dimension corresponding to length.

Equations

• Dimension.L𝓭 = { length := 1, time := 0, mass := 0, charge := 0, temperature := 0 }

@[simp]

theorem Dimension.L𝓭_length : L𝓭.length = 1

@[simp]

theorem Dimension.L𝓭_time : L𝓭.time = 0

@[simp]

theorem Dimension.L𝓭_mass : L𝓭.mass = 0

@[simp]

theorem Dimension.L𝓭_charge : L𝓭.charge = 0

@[simp]

theorem Dimension.L𝓭_temperature : L𝓭.temperature = 0

def Dimension.T𝓭 : Dimension

The dimension corresponding to time.

Equations

• Dimension.T𝓭 = { length := 0, time := 1, mass := 0, charge := 0, temperature := 0 }

@[simp]

theorem Dimension.T𝓭_length : T𝓭.length = 0

@[simp]

theorem Dimension.T𝓭_time : T𝓭.time = 1

@[simp]

theorem Dimension.T𝓭_mass : T𝓭.mass = 0

@[simp]

theorem Dimension.T𝓭_charge : T𝓭.charge = 0

@[simp]

theorem Dimension.T𝓭_temperature : T𝓭.temperature = 0

def Dimension.M𝓭 : Dimension

The dimension corresponding to mass.

Equations

• Dimension.M𝓭 = { length := 0, time := 0, mass := 1, charge := 0, temperature := 0 }

def Dimension.C𝓭 : Dimension

The dimension corresponding to charge.

Equations

• Dimension.C𝓭 = { length := 0, time := 0, mass := 0, charge := 1, temperature := 0 }

def Dimension.Θ𝓭 : Dimension

The dimension corresponding to temperature.

Equations

• Dimension.Θ𝓭 = { length := 0, time := 0, mass := 0, charge := 0, temperature := 1 }

Units

structure UnitChoices : Type

The choice of units.

• length : LengthUnit

  The length unit.

• time : TimeUnit

  The time unit.

• mass : MassUnit

  The mass unit.

• charge : ChargeUnit

  The charge unit.

• temperature : TemperatureUnit

  The temperature unit.

noncomputable def UnitChoices.dimScale (u1 u2 : UnitChoices) (d : Dimension) : NNReal

Given two choices of units u1 and u2 and a dimension d, the element of ℝ≥0 corresponding to the scaling (by definition) of a quantity of dimension d when changing from units u1 to u2.

Equations

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

@[simp]

theorem UnitChoices.dimScale_self (u : UnitChoices) (d : Dimension) : u.dimScale u d = 1

@[simp]

theorem UnitChoices.dimScale_zero (u1 u2 : UnitChoices) : u1.dimScale u2 0 = 1

theorem UnitChoices.dimScale_transitive (u1 u2 u3 : UnitChoices) (d : Dimension) : u1.dimScale u2 d * u2.dimScale u3 d = u1.dimScale u3 d

@[simp]

theorem UnitChoices.dimScale_mul (u1 u2 : UnitChoices) (d1 d2 : Dimension) : u1.dimScale u2 (d1 * d2) = u1.dimScale u2 d1 * u1.dimScale u2 d2

@[simp]

theorem UnitChoices.dimScale_neq_zero (u1 u2 : UnitChoices) (d : Dimension) : u1.dimScale u2 d ≠ 0

theorem UnitChoices.dimScale_inv (u1 u2 : UnitChoices) (d : Dimension) : u1.dimScale u2 d⁻¹ = (u1.dimScale u2 d)⁻¹

theorem UnitChoices.dimScale_symm (u1 u2 : UnitChoices) (d : Dimension) : u1.dimScale u2 d = (u2.dimScale u1 d)⁻¹

noncomputable def UnitChoices.SI : UnitChoices

The choice of units corresponding to SI units, that is

• meters,
• seconds,
• kilograms,
• columbs,
• kelvin.

Equations

• UnitChoices.SI = { length := LengthUnit.meters, time := TimeUnit.seconds, mass := MassUnit.kilograms, charge := ChargeUnit.coulombs, temperature := TemperatureUnit.kelvin }

@[simp]

theorem UnitChoices.SI_length : SI.length = LengthUnit.meters

@[simp]

theorem UnitChoices.SI_time : SI.time = TimeUnit.seconds

@[simp]

theorem UnitChoices.SI_mass : SI.mass = MassUnit.kilograms

@[simp]

theorem UnitChoices.SI_charge : SI.charge = ChargeUnit.coulombs

@[simp]

theorem UnitChoices.SI_temperature : SI.temperature = TemperatureUnit.kelvin

Dimensionful

Given a type M with a dimension d, a dimensionful quantity is a map from UnitChoices to M, which scales with the choice of unit according to d.

See: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/physical.20units/near/530520545

def HasDimension (d : Dimension) {M : Type} [SMul NNReal M] (f : UnitChoices → M) : Prop

A quantity of type M which depends on a choice of units UnitChoices is said to be of dimension d if it scales by UnitChoices.dimScale u1 u2 d under a change in units.

Equations

• HasDimension d f = ∀ (u1 u2 : UnitChoices), f u2 = u1.dimScale u2 d • f u1

theorem hasDimension_iff {d : Dimension} {M : Type} [SMul NNReal M] (f : UnitChoices → M) : HasDimension d f ↔ ∀ (u1 u2 : UnitChoices), f u2 = u1.dimScale u2 d • f u1

def Dimensionful (d : Dimension) (M : Type) [SMul NNReal M] : Type

The type of maps from UnitChoices to M which have dimension d.

Equations

• Dimensionful d M = { f : UnitChoices → M // HasDimension d f }

instance Dimensionful.instCoeFunForallUnitChoices {d : Dimension} {M : Type} [SMul NNReal M] : CoeFun (Dimensionful d M) fun (x : Dimensionful d M) => UnitChoices → M

Applying an element of Dimensionful d M to a unit choice gives an element of M.

Equations

• Dimensionful.instCoeFunForallUnitChoices = { coe := fun (f : Dimensionful d M) => ↑f }

theorem Dimensionful.coe_hasDimension {d : Dimension} {M : Type} [SMul NNReal M] (f : Dimensionful d M) : HasDimension d ↑f

Equality lemmas

theorem Dimensionful.eq_of_val {d : Dimension} {M : Type} [SMul NNReal M] {f1 f2 : Dimensionful d M} (h : ↑f1 = ↑f2) : f1 = f2

theorem Dimensionful.eq_of_apply {d : Dimension} {M : Type} [SMul NNReal M] {f1 f2 : Dimensionful d M} (h : ∀ (u : UnitChoices), ↑f1 u = ↑f2 u) : f1 = f2

theorem Dimensionful.eq_of_unitChoices {d : Dimension} {M : Type} [SMul NNReal M] {f1 f2 : Dimensionful d M} (u : UnitChoices) (h : ↑f1 u = ↑f2 u) : f1 = f2

theorem Dimensionful.eq_of_SI {d : Dimension} {M : Type} [SMul NNReal M] {f1 f2 : Dimensionful d M} (h : ↑f1 UnitChoices.SI = ↑f2 UnitChoices.SI) : f1 = f2

MulAction

instance Dimensionful.instMulActionNNReal {d : Dimension} {M : Type} [MulAction NNReal M] : MulAction NNReal (Dimensionful d M)

Equations

• Dimensionful.instMulActionNNReal = { smul := fun (a : NNReal) (f : Dimensionful d M) => ⟨fun (u : UnitChoices) => a • ↑f u, ⋯⟩, one_smul := ⋯, mul_smul := ⋯ }

instance Dimensionful.instMulActionReal {d : Dimension} {M : Type} [MulAction ℝ M] : MulAction ℝ (Dimensionful d M)

Equations

• Dimensionful.instMulActionReal = { smul := fun (a : ℝ) (f : Dimensionful d M) => ⟨fun (u : UnitChoices) => a • ↑f u, ⋯⟩, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem Dimensionful.smul_apply {d : Dimension} {M : Type} [MulAction NNReal M] (f : Dimensionful d M) (u : UnitChoices) (a : NNReal) : ↑(a • f) u = a • ↑f u

@[simp]

theorem Dimensionful.smul_real_apply {d : Dimension} {M : Type} [MulAction ℝ M] (f : Dimensionful d M) (u : UnitChoices) (a : ℝ) : ↑(a • f) u = a • ↑f u

ofUnit

noncomputable def Dimensionful.ofUnit (d : Dimension) {M : Type} [MulAction NNReal M] (m : M) (u : UnitChoices) : Dimensionful d M

The creation of an element f : Dimensionful d M given a m : M and a choice of units u : UnitChoices, defined such that f u = m.

Equations

• Dimensionful.ofUnit d m u = ⟨fun (u1 : UnitChoices) => u.dimScale u1 d • m, ⋯⟩

theorem Dimensionful.ofUnit_eq_mul_dimScale {d : Dimension} {M : Type} [MulAction NNReal M] (m : M) (u1 u2 : UnitChoices) : ofUnit d m u1 = u1.dimScale u2 d • ofUnit d m u2

@[simp]

theorem Dimensionful.ofUnit_apply_self {d : Dimension} {M : Type} [MulAction NNReal M] (m : M) (u : UnitChoices) : ↑(ofUnit d m u) u = m

theorem Dimensionful.ofUnit_apply {d : Dimension} {M : Type} [MulAction NNReal M] (m : M) (u1 u2 : UnitChoices) : ↑(ofUnit d m u1) u2 = u1.dimScale u2 d • m

LE

instance Dimensionful.instLENNReal {d : Dimension} : LE (Dimensionful d NNReal)

Equations

• Dimensionful.instLENNReal = { le := fun (f1 f2 : Dimensionful d NNReal) => ∀ (u : UnitChoices), ↑f1 u ≤ ↑f2 u }

theorem Dimensionful.le_nnReals_of_unitChoice {d : Dimension} {f1 f2 : Dimensionful d NNReal} (u : UnitChoices) (h : ↑f1 u ≤ ↑f2 u) : f1 ≤ f2

Addition and module structure

instance Dimensionful.instAddZeroClass {d : Dimension} {M : Type} [AddZeroClass M] [DistribSMul NNReal M] : AddZeroClass (Dimensionful d M)

Equations

• Dimensionful.instAddZeroClass = { zero := ⟨fun (x : UnitChoices) => 0, ⋯⟩, add := fun (f1 f2 : Dimensionful d M) => ⟨fun (u : UnitChoices) => ↑f1 u + ↑f2 u, ⋯⟩, zero_add := ⋯, add_zero := ⋯ }

@[simp]

theorem Dimensionful.add_apply {d : Dimension} {M : Type} [AddZeroClass M] [DistribSMul NNReal M] (f1 f2 : Dimensionful d M) (u : UnitChoices) : ↑(f1 + f2) u = ↑f1 u + ↑f2 u

instance Dimensionful.instAddCommGroup {d : Dimension} {M : Type} [AddCommGroup M] [DistribSMul NNReal M] : AddCommGroup (Dimensionful d M)

Equations

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

@[simp]

theorem Dimensionful.neg_apply {d : Dimension} {M : Type} [AddCommGroup M] [DistribSMul NNReal M] (f : Dimensionful d M) (u : UnitChoices) : ↑(-f) u = -↑f u

@[simp]

theorem Dimensionful.zero_apply {d : Dimension} {M : Type} [AddZeroClass M] [DistribSMul NNReal M] (u : UnitChoices) : ↑0 u = 0

instance Dimensionful.instModuleReal {d : Dimension} {M : Type} [AddCommGroup M] [Module ℝ M] : Module ℝ (Dimensionful d M)

Equations

• Dimensionful.instModuleReal = { toMulAction := Dimensionful.instMulActionReal, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem Dimensionful.sub_apply {d : Dimension} {M : Type} [AddCommGroup M] [DistribSMul NNReal M] (f1 f2 : Dimensionful d M) (u : UnitChoices) : ↑(f1 - f2) u = ↑f1 u - ↑f2 u

### Multiplication

instance Dimensionful.instHMulRealHMulDimension {d1 d2 : Dimension} : HMul (Dimensionful d1 ℝ) (Dimensionful d2 ℝ) (Dimensionful (d1 * d2) ℝ)

Equations

• Dimensionful.instHMulRealHMulDimension = { hMul := fun (x : Dimensionful d1 ℝ) (y : Dimensionful d2 ℝ) => ⟨fun (u : UnitChoices) => ↑x u * ↑y u, ⋯⟩ }

@[simp]

theorem Dimensionful.mul_real_apply {d1 d2 : Dimension} (x : Dimensionful d1 ℝ) (y : Dimensionful d2 ℝ) (u : UnitChoices) : ↑(x * y) u = ↑x u * ↑y u

Division

noncomputable instance Dimensionful.instHDivRealHMulDimensionInv {d1 d2 : Dimension} : HDiv (Dimensionful d1 ℝ) (Dimensionful d2 ℝ) (Dimensionful (d1 * d2⁻¹) ℝ)

Equations

• Dimensionful.instHDivRealHMulDimensionInv = { hDiv := fun (x : Dimensionful d1 ℝ) (y : Dimensionful d2 ℝ) => ⟨fun (u : UnitChoices) => ↑x u / ↑y u, ⋯⟩ }

@[simp]

theorem Dimensionful.hdiv_apply {d1 d2 : Dimension} (x : Dimensionful d1 ℝ) (y : Dimensionful d2 ℝ) (u : UnitChoices) : ↑(x / y) u = ↑x u / ↑y u

noncomputable instance Dimensionful.instHDivRealInvDimension {d2 : Dimension} : HDiv ℝ (Dimensionful d2 ℝ) (Dimensionful d2⁻¹ ℝ)

Equations

• Dimensionful.instHDivRealInvDimension = { hDiv := fun (x : ℝ) (y : Dimensionful d2 ℝ) => ⟨fun (u : UnitChoices) => x / ↑y u, ⋯⟩ }

SMul

noncomputable instance Dimensionful.instHSMulRealHMulDimension {d1 d2 : Dimension} {M : Type} [AddCommGroup M] [Module ℝ M] : HSMul (Dimensionful d1 ℝ) (Dimensionful d2 M) (Dimensionful (d1 * d2) M)

Equations

• Dimensionful.instHSMulRealHMulDimension = { hSMul := fun (x : Dimensionful d1 ℝ) (y : Dimensionful d2 M) => ⟨fun (u : UnitChoices) => ↑x u • ↑y u, ⋯⟩ }

@[simp]

theorem Dimensionful.hsmul_apply {d1 d2 : Dimension} {M : Type} [AddCommGroup M] [Module ℝ M] (x : Dimensionful d1 ℝ) (y : Dimensionful d2 M) (u : UnitChoices) : ↑(x • y) u = ↑x u • ↑y u

Inner product

We define the inner product in SI units.

noncomputable instance Dimensionful.instSeminormedAddCommGroup {M : Type} {d : Dimension} [SeminormedAddCommGroup M] [InnerProductSpace ℝ M] : SeminormedAddCommGroup (Dimensionful d M)

Equations

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

noncomputable instance Dimensionful.instInnerProductSpaceReal {M : Type} {d : Dimension} [SeminormedAddCommGroup M] [InnerProductSpace ℝ M] : InnerProductSpace ℝ (Dimensionful d M)

Equations

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

Derivatives

noncomputable def Dimensionful.deriv {d1 d2 : Dimension} (f : Dimensionful d1 ℝ → Dimensionful d2 ℝ) (atLocation : Dimensionful d1 ℝ) : Dimensionful (d2 * d1⁻¹) ℝ

The derivative using dimensionalful quantities.

Equations

• Dimensionful.deriv f atLocation = ⟨fun (u : UnitChoices) => ↑((fderiv ℝ f atLocation) (Dimensionful.ofUnit d1 1 u)) u, ⋯⟩

valCast

noncomputable def Dimensionful.valCast {d : Dimension} {M : Type} [SMul NNReal M] (f : Dimensionful d M) (hd : d = 0 := by rfl) : M

The casting of a quantity in Dimensionful 0 M to its underlying element in M.

Equations

• f.valCast hd = ↑f UnitChoices.SI

theorem Dimensionful.valCast_eq_unitChoices {d : Dimension} {M : Type} [MulAction NNReal M] {f : Dimensionful d M} {hd : d = 0} (u : UnitChoices) : f.valCast hd = ↑f u

Measured quantities

We defined Measured d M to be a type of measured quantity of type M and of dimension d, the terms of Measured d M are corresponds to values of the quantity in a given but arbitary set of units.

If M has the type of a vector space, then the type Measured d M inherits this structure.

Likewise if M has the type of an inner product space, then the type Measured d M inherits this structure. However, note that the inner product space does not explicit track the dimension, mapping down to ℝ. This is in theory fine, as it is still dimensionful, in the sense that it scales with the choice of unit.

The type Measured d M can be seen as a convienent way to work with and keep track of dimensions. However, working with Measured d M does not formally prove anything about dimensions, which can only be done with Dimensionful d M, or other manifest considerations of UnitChoices.

structure Measured (d : Dimension) (M : Type) [SMul NNReal M] : Type

A measured quantity is a quantity which carries a dimension d, but which lives in a given (but arbitary) set of units.

• val : M

  The value of the measured quantity.

theorem Measured.eq_of_val {d : Dimension} {M : Type} [SMul NNReal M] {m1 m2 : Measured d M} (h : m1.val = m2.val) : m1 = m2

theorem Measured.eq_of_val_iff {d : Dimension} {M : Type} [SMul NNReal M] {m1 m2 : Measured d M} : m1 = m2 ↔ m1.val = m2.val

Basic instances carried from underlying type.

instance Measured.instSMul {d : Dimension} {α M : Type} [SMul NNReal M] [SMul α M] : SMul α (Measured d M)

Equations

• Measured.instSMul = { smul := fun (r : α) (m : Measured d M) => { val := r • m.val } }

@[simp]

theorem Measured.smul_val {d : Dimension} {α M : Type} [SMul NNReal M] [SMul α M] (r : α) (m : Measured d M) : (r • m).val = r • m.val

instance Measured.instHMulHMulDimension {d1 d2 : Dimension} {M1 M2 M : Type} [SMul NNReal M1] [SMul NNReal M2] [SMul NNReal M] [HMul M1 M2 M] : HMul (Measured d1 M1) (Measured d2 M2) (Measured (d1 * d2) M)

Equations

• Measured.instHMulHMulDimension = { hMul := fun (x : Measured d1 M1) (y : Measured d2 M2) => { val := x.val * y.val } }

instance Measured.instHSMulHMulDimension {d1 d2 : Dimension} {M1 M2 M : Type} [SMul NNReal M1] [SMul NNReal M2] [SMul NNReal M] [HSMul M1 M2 M] : HSMul (Measured d1 M1) (Measured d2 M2) (Measured (d1 * d2) M)

Equations

• Measured.instHSMulHMulDimension = { hSMul := fun (x : Measured d1 M1) (y : Measured d2 M2) => { val := x.val • y.val } }

instance Measured.instLE {d : Dimension} {M : Type} [SMul NNReal M] [LE M] : LE (Measured d M)

Equations

• Measured.instLE = { le := fun (x y : Measured d M) => x.val ≤ y.val }

theorem Measured.le_eq_le_val {d : Dimension} {M : Type} [SMul NNReal M] [LE M] (x y : Measured d M) : x ≤ y ↔ x.val ≤ y.val

noncomputable instance Measured.instHSMulUnitChoicesDimensionful {d : Dimension} {M : Type} [MulAction NNReal M] : HSMul (Measured d M) UnitChoices (Dimensionful d M)

Equations

• Measured.instHSMulUnitChoicesDimensionful = { hSMul := fun (m : Measured d M) (u : UnitChoices) => ⟨fun (u1 : UnitChoices) => u.dimScale u1 d • m.val, ⋯⟩ }

@[simp]

theorem Measured.smul_unitChoices_apply {d : Dimension} {M : Type} [MulAction NNReal M] (m : Measured d M) (u u1 : UnitChoices) : ↑(m • u) u1 = u.dimScale u1 d • m.val