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.

Other implementations of units

There are other implementations of units in Lean, in particular:

1. https://github.com/ATOMSLab/LeanDimensionalAnalysis/tree/main
2. https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SI.lean
3. https://github.com/ecyrbe/lean-units Each of these have their own advantages and specific use-cases. For example both (1) and (3) allow for or work in Floats, allowing computability and the use of #eval. This is currently not possible with the more theoretical implementation here in PhysLean which is based exclusively on Reals.

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.

theorem UnitChoices.ext {x y : UnitChoices} (length : x.length = y.length) (time : x.time = y.time) (mass : x.mass = y.mass) (charge : x.charge = y.charge) (temperature : x.temperature = y.temperature) : x = y

theorem UnitChoices.ext_iff {x y : UnitChoices} : x = y ↔ x.length = y.length ∧ x.time = y.time ∧ x.mass = y.mass ∧ x.charge = y.charge ∧ x.temperature = y.temperature

noncomputable def UnitChoices.dimScale (u1 u2 : UnitChoices) : 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.

theorem UnitChoices.dimScale_apply (u1 u2 : UnitChoices) (d : Dimension) : (u1.dimScale u2) d = (u1.length / u2.length) ^ ↑d.length * (u1.time / u2.time) ^ ↑d.time * (u1.mass / u2.mass) ^ ↑d.mass * (u1.charge / u2.charge) ^ ↑d.charge * (u1.temperature / u2.temperature) ^ ↑d.temperature

@[simp]

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

@[simp]

theorem UnitChoices.dimScale_one (u1 u2 : UnitChoices) : (u1.dimScale u2) 1 = 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_symm (u1 u2 : UnitChoices) (d : Dimension) : (u1.dimScale u2) d * (u2.dimScale u1) d = 1

@[simp]

theorem UnitChoices.dimScale_coe_mul_symm (u1 u2 : UnitChoices) (d : Dimension) : ↑((u1.dimScale u2) d) * ↑((u2.dimScale u1) d) = 1

@[simp]

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

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

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

@[simp]

theorem UnitChoices.smul_dimScale_injective {M : Type} [MulAction NNReal M] (u1 u2 : UnitChoices) (d : Dimension) (m1 m2 : M) : (u1.dimScale u2) d • m1 = (u1.dimScale u2) d • m2 ↔ m1 = m2

@[simp]

theorem UnitChoices.dimScale_pos (u1 u2 : UnitChoices) (d : Dimension) : 0 < (u1.dimScale u2) 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

noncomputable def UnitChoices.SIPrimed : UnitChoices

A UnitChoices which is related to SI by a prime scaling of each of the underlying units. This is useful in proving that a result is not dimensionally correct.

Equations

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

@[simp]

theorem UnitChoices.dimScale_SI_SIPrimed (d : Dimension) : (SI.dimScale SIPrimed) d = 2⁻¹ ^ ↑d.length * 3⁻¹ ^ ↑d.time * 5⁻¹ ^ ↑d.mass * 7⁻¹ ^ ↑d.charge * 11⁻¹ ^ ↑d.temperature

@[simp]

theorem UnitChoices.dimScale_SIPrimed_SI (d : Dimension) : (SIPrimed.dimScale SI) d = 2 ^ ↑d.length * 3 ^ ↑d.time * 5 ^ ↑d.mass * 7 ^ ↑d.charge * 11 ^ ↑d.temperature

Types carrying dimensions

Dimensions are assigned to types with the following type-classes

• CarriesDimension for a type carrying an instance of MulAction ℝ≥0 M
• ModuleCarriesDimension for a type carrying an instance of Module ℝ M.

The latter is need to prevent a typeclass dimond.

class CarriesDimension (M : Type) extends MulAction NNReal M : Type

A type M carries a dimension d if every element of M is supposed to have this dimension. For example, the type Time will carry a dimension T𝓭.

• smul : NNReal → M → M
• one_smul (b : M) : 1 • b = b
• mul_smul (x y : NNReal) (b : M) : (x * y) • b = x • y • b
• d : Dimension

  The dimension carried by a type M.

class ModuleCarriesDimension (M : Type) [AddCommMonoid M] [Module ℝ M] : Type

A module M carries a dimension d if every element of M is supposed to have this dimension. This is defined in additon to CarriesDimension to prevent a type-casting dimond.

• d : Dimension

  The dimension carried by a module M.

instance instCarriesDimensionOfModuleCarriesDimension {M : Type} [AddCommMonoid M] [Module ℝ M] [ModuleCarriesDimension M] : CarriesDimension M

Equations

• instCarriesDimensionOfModuleCarriesDimension = { toMulAction := NNReal.instMulActionOfReal, d := ModuleCarriesDimension.d M }

@[simp]

theorem ModuleCarriesDimension.d_eq_CarriesDimension_d {M : Type} [AddCommMonoid M] [Module ℝ M] [ModuleCarriesDimension M] : d M = CarriesDimension.d M

Terms of the current dimension

Given a type M which carries a dimension d, we are intrested in elements of M which depend on a choice of units, i.e. functions UnitChoices → M.

We define both a proposition

• HasDimension f which says that f scales correctly with units, and a type
• Dimensionful M which is the subtype of functions which HasDimension.

def HasDimension {M : Type} [CarriesDimension 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 f = ∀ (u1 u2 : UnitChoices), f u2 = (u1.dimScale u2) (CarriesDimension.d M) • f u1

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

def Dimensionful (M : Type) [CarriesDimension M] : Type

The subtype of functions UnitChoices → M, for which M carries a dimension, which HasDimension.

Equations

• Dimensionful M = Subtype HasDimension

instance instCoeFunDimensionfulForallUnitChoices {M : Type} [CarriesDimension M] : CoeFun (Dimensionful M) fun (x : Dimensionful M) => UnitChoices → M

Equations

• instCoeFunDimensionfulForallUnitChoices = { coe := Subtype.val }

theorem Dimensionful.ext {M : Type} [CarriesDimension M] (f1 f2 : Dimensionful M) (h : ↑f1 = ↑f2) : f1 = f2

theorem Dimensionful.ext_iff {M : Type} [CarriesDimension M] {f1 f2 : Dimensionful M} : f1 = f2 ↔ ↑f1 = ↑f2

instance instMulActionNNRealDimensionful {M : Type} [CarriesDimension M] : MulAction NNReal (Dimensionful M)

Equations

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

@[simp]

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

noncomputable def CarriesDimension.toDimensionful {M : Type} [CarriesDimension M] (u : UnitChoices) : M ≃ Dimensionful M

For M carying a dimension d, the equivalence between M and Dimension M, given a choice of units.

Equations

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

theorem CarriesDimension.toDimensionful_apply_apply {M : Type} [CarriesDimension M] (u1 u2 : UnitChoices) (m : M) : ↑((toDimensionful u1) m) u2 = (u1.dimScale u2) (d M) • m