The quantity calculus

A quantity is a magnitude together with a dimension: 0.9 g is a magnitude in the dimension of mass, 0.9 g/mL one in the dimension of density, and 9 is a pure number, a magnitude in the identity dimension. This file sets up the quantity calculus that measure-phrase semantics computes in. Dimensions are the group QuantityDimension; quantities are pairs K × QuantityDimension of a magnitude and a dimension and multiply and divide componentwise, so that dividing two quantities of one dimension yields a pure number.

Main definitions

• Quantity, Quantity.pure, Quantity.unit: quantities, pure numbers, unit quantities.
• DimensionedMeasure.quantity: the value of a measure function as a quantity.

References

• [de-boer-1995]
• [coppock-2021]

@[reducible, inline]

abbrev Degree.Quantity (K : Type u_1) : Type u_1

A quantity, a magnitude in K with a dimension. Quantities multiply and divide componentwise.

Equations

• Degree.Quantity K = (K × Degree.QuantityDimension)

def Degree.Quantity.pure {K : Type u_1} (n : K) : Quantity K

The pure number n, a quantity (n, 1) of the identity dimension.

Equations

• Degree.Quantity.pure n = (n, 1)

def Degree.Quantity.unit {K : Type u_1} [One K] (d : Dimension) : Quantity K

The unit quantity (1, d) of the base dimension d.

Equations

• Degree.Quantity.unit d = (1, Degree.QuantityDimension.of d)

@[simp]

theorem Degree.Quantity.pure_fst {K : Type u_1} (n : K) : (pure n).1 = n

@[simp]

theorem Degree.Quantity.pure_snd {K : Type u_1} (n : K) : (pure n).2 = 1

@[simp]

theorem Degree.Quantity.unit_fst {K : Type u_1} [One K] (d : Dimension) : (unit d).1 = 1

@[simp]

theorem Degree.Quantity.unit_snd {K : Type u_1} [One K] (d : Dimension) : (unit d).2 = QuantityDimension.of d

theorem Degree.Quantity.pure_mul_div_pure_mul {K : Type u_1} [CommGroupWithZero K] {k : K} (hk : k ≠ 0) (q r : Quantity K) : pure k * q / (pure k * r) = q / r

Scaling both quantities by the same nonzero pure number leaves their quotient unchanged: 0.1 kg / L = 0.1 g / mL.

theorem Degree.Quantity.div_eq_div_iff_eq_mul_div {K : Type u_1} [CommGroupWithZero K] {a b q r : Quantity K} (hb : b.1 ≠ 0) (hr : r.1 ≠ 0) : a / b = q / r ↔ a = q * (b / r)

a / b = q / r ↔ a = q * (b / r) when the magnitudes of b and r are nonzero.

theorem Degree.Quantity.div_eq_pure_iff {K : Type u_1} [CommGroupWithZero K] {a q : Quantity K} {n : K} (hq : q.1 ≠ 0) (h : a.2 = q.2) : a / q = pure n ↔ pure n * q = a

The quotient of two quantities of one dimension is the pure number n with n ⋅ q = a.

def Degree.DimensionedMeasure.quantity {E : Type u_1} {K : Type} (μ : DimensionedMeasure E K) (x : E) : Quantity K

The value of μ at x as a quantity of μ's dimension.

Equations

• μ.quantity x = (μ.apply x, Degree.QuantityDimension.of μ.dimension)

@[simp]

theorem Degree.DimensionedMeasure.quantity_fst {E : Type u_1} {K : Type} (μ : DimensionedMeasure E K) (x : E) : (μ.quantity x).1 = μ.apply x

@[simp]

theorem Degree.DimensionedMeasure.quantity_snd {E : Type u_1} {K : Type} (μ : DimensionedMeasure E K) (x : E) : (μ.quantity x).2 = QuantityDimension.of μ.dimension

theorem Degree.DimensionedMeasure.quantity_eq_pure_mul_unit_iff {E : Type u_1} {K : Type} [MulOneClass K] [Preorder K] (μ : DimensionedMeasure E K) (n : K) (x : E) : μ.quantity x = Quantity.pure n * Quantity.unit μ.dimension ↔ μ.applyNumeral n x

Measuring n units is having the quantity n times the unit.