Units of measure

A unit of measure over a set B of base units is a ℚ-valued exponent vector: a function B → ℚ recording the power of each base unit.

Units are written multiplicatively (m * s⁻¹, m ^ (-1/2 : ℚ)), so the carrier is Multiplicative ℚ pointwise. Unit multiplication is then exponent addition, and Pi.commGroup supplies the whole abelian group structure.

Why ℚ and not ℤ

Two independent reasons, recorded because the choice looks like an extravagance and is not:

• It is forced by the domain. A normalized three-dimensional wavefunction carries m ^ (-3/2); volatility carries Time ^ (-1/2). Neither is expressible with integer exponents, which is why no existing static units system can type either one.
• It makes the solver simpler, not harder. Over ℤ the unit group is a lattice and unification needs Hermite or Smith normal form; over ℚ it is a vector space and unification is Gaussian elimination.

@[reducible, inline]

abbrev LambdaS.Uom (B : Type u_1) : Type u_1

A unit of measure over base units B: a ℚ-valued exponent vector, written multiplicatively.

Equations

• LambdaS.Uom B = (B → Multiplicative ℚ)

def LambdaS.Uom.exp {B : Type u_1} (u : Uom B) (b : B) : ℚ

The exponent of base unit b in u.

Equations

• u.exp b = Multiplicative.toAdd (u b)

def LambdaS.Uom.ofExp {B : Type u_1} (f : B → ℚ) : Uom B

Build a unit from an exponent vector.

Equations

• LambdaS.Uom.ofExp f b = Multiplicative.ofAdd (f b)

@[simp]

theorem LambdaS.Uom.exp_ofExp {B : Type u_1} (f : B → ℚ) (b : B) : (ofExp f).exp b = f b

@[simp]

theorem LambdaS.Uom.exp_one {B : Type u_1} (b : B) : exp 1 b = 0

@[simp]

theorem LambdaS.Uom.exp_mul {B : Type u_1} (u v : Uom B) (b : B) : (u * v).exp b = u.exp b + v.exp b

@[simp]

theorem LambdaS.Uom.exp_inv {B : Type u_1} (u : Uom B) (b : B) : u⁻¹.exp b = -u.exp b

@[simp]

theorem LambdaS.Uom.exp_div {B : Type u_1} (u v : Uom B) (b : B) : (u / v).exp b = u.exp b - v.exp b

theorem LambdaS.Uom.ext {B : Type u_1} {u v : Uom B} (h : ∀ (b : B), u.exp b = v.exp b) : u = v

Two units are equal exactly when all their exponents agree. This is the only extensionality principle the development needs.

theorem LambdaS.Uom.ext_iff {B : Type u_1} {u v : Uom B} : u = v ↔ ∀ (b : B), u.exp b = v.exp b

theorem LambdaS.Uom.ext_iff' {B : Type u_1} {u v : Uom B} : u = v ↔ ∀ (b : B), u.exp b = v.exp b

def LambdaS.Uom.rpow {B : Type u_1} (u : Uom B) (q : ℚ) : Uom B

Raising a unit to a rational power. This is the operation integer-exponent systems cannot provide, and it is total: every unit has an n-th root.

Equations

• u.rpow q = LambdaS.Uom.ofExp fun (b : B) => q * u.exp b

@[instance_reducible]

instance LambdaS.Uom.instHPowRat {B : Type u_1} : HPow (Uom B) ℚ (Uom B)

Rational powers are written u ^ q, exactly as on paper.

Equations

• LambdaS.Uom.instHPowRat = { hPow := LambdaS.Uom.rpow }

@[simp]

theorem LambdaS.Uom.exp_rpow {B : Type u_1} (u : Uom B) (q : ℚ) (b : B) : (u ^ q).exp b = q * u.exp b

@[simp]

theorem LambdaS.Uom.rpow_one {B : Type u_1} (u : Uom B) : u ^ 1 = u

@[simp]

theorem LambdaS.Uom.rpow_zero {B : Type u_1} (u : Uom B) : u ^ 0 = 1

theorem LambdaS.Uom.rpow_add {B : Type u_1} (u : Uom B) (p q : ℚ) : u ^ (p + q) = u ^ p * u ^ q

theorem LambdaS.Uom.rpow_mul {B : Type u_1} (u : Uom B) (p q : ℚ) : u ^ (p * q) = (u ^ q) ^ p

theorem LambdaS.Uom.rpow_nth_root {B : Type u_1} (u : Uom B) {n : ℚ} (hn : n ≠ 0) : (u ^ (1 / n)) ^ n = u

Every unit has an n-th root for n ≠ 0. Over ℤ this fails, which is precisely why the square root of a dimensioned quantity is inexpressible there.

theorem LambdaS.Uom.eq_inv_iff_one {B : Type u_1} {u : Uom B} : u = u⁻¹ ↔ u = 1

The exponent group is torsion-free, over ℚ here and over ℤ equally, so a unit equal to its own inverse is trivial.

This single fact is what forces the Cholesky factor into the dimensionless space in LambdaS.Map. The contrast it needs is a group with torsion, say ℤ/2ℤ-graded exponents, not the integer exponents of [Kennedy 1997]; for what the rational exponents do buy, see rpow_nth_root above.