Units on Length

A unit of length corresponds to a choice of translationally-invariant metric on the space manifold (to be defined). Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type LengthUnit to be equivalent to the positive reals.

On LengthUnit there is an instance of division giving a real number, corresponding to the ratio of the two scales of length unit.

To define specific length units, we first state the existence of a a given length unit, and then construct all other length units from it. We choose to state the existence of the length unit of meters, and construct all other length units from that.

structure LengthUnit : Type

The choices of translationally-invariant metrics on the space-manifold. Such a choice corresponds to a choice of units for length.

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

theorem LengthUnit.val_neq_zero (x : LengthUnit) : x.val ≠ 0

theorem LengthUnit.val_pos (x : LengthUnit) : 0 < x.val

instance LengthUnit.instInhabited : Inhabited LengthUnit

Division of LengthUnit

noncomputable instance LengthUnit.instHDivNNReal : HDiv LengthUnit LengthUnit NNReal

theorem LengthUnit.div_eq_val (x y : LengthUnit) : x / y = ⟨x.val / y.val, ⋯⟩

@[simp]

theorem LengthUnit.div_neq_zero (x y : LengthUnit) : ¬x / y = 0

@[simp]

theorem LengthUnit.div_pos (x y : LengthUnit) : 0 < x / y

@[simp]

theorem LengthUnit.div_self (x : LengthUnit) : x / x = 1

theorem LengthUnit.div_symm (x y : LengthUnit) : x / y = (y / x)⁻¹

@[simp]

theorem LengthUnit.div_mul_div_coe (x y z : LengthUnit) : ↑(x / y) * ↑(y / z) = ↑(x / z)

The scaling of a length unit

def LengthUnit.scale (r : ℝ) (x : LengthUnit) (hr : 0 < r := by norm_num) : LengthUnit

The scaling of a length unit by a positive real.

@[simp]

theorem LengthUnit.scale_div_self (x : LengthUnit) (r : ℝ) (hr : 0 < r) : scale r x hr / x = ⟨r, ⋯⟩

@[simp]

theorem LengthUnit.self_div_scale (x : LengthUnit) (r : ℝ) (hr : 0 < r) : x / scale r x hr = ⟨1 / r, ⋯⟩

@[simp]

theorem LengthUnit.scale_one (x : LengthUnit) : scale 1 x ⋯ = x

@[simp]

theorem LengthUnit.scale_div_scale (x1 x2 : LengthUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 x1 hr1 / scale r2 x2 hr2 = ⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2)

@[simp]

theorem LengthUnit.scale_scale (x : LengthUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯

Specific choices of Length units

To define a specific length units. We first define the notion of a meter to correspond to the length unit with underlying value equal to 1. This is really down to a choice in the isomorphism between the set of metrics on the space manifold and the positive reals. From this choice of meters, we can define other length units by scaling meters.

def LengthUnit.meters : LengthUnit

The definition of a length unit of meters.

noncomputable def LengthUnit.femtometers : LengthUnit

The length unit of femtometers (10⁻¹⁵ of a meter).

noncomputable def LengthUnit.picometers : LengthUnit

The length unit of picometers (10⁻¹² of a meter).

noncomputable def LengthUnit.nanometers : LengthUnit

The length unit of nanometers (10⁻⁹ of a meter).

noncomputable def LengthUnit.micrometers : LengthUnit

The length unit of micrometers (10⁻⁶ of a meter).

noncomputable def LengthUnit.millimeters : LengthUnit

The length unit of millimeters (10⁻³ of a meter).

noncomputable def LengthUnit.centimeters : LengthUnit

The length unit of centimeters (10⁻² of a meter).

noncomputable def LengthUnit.inches : LengthUnit

The length unit of inch (0.0254 meters).

noncomputable def LengthUnit.links : LengthUnit

The length unit of link (0.201168 meters).

noncomputable def LengthUnit.feet : LengthUnit

The length unit of feet (0.3048 meters)

noncomputable def LengthUnit.yards : LengthUnit

The length unit of a yard (0.9144 meters)

noncomputable def LengthUnit.rods : LengthUnit

The length unit of a rod (5.0292 meters)

noncomputable def LengthUnit.chains : LengthUnit

The length unit of a chain (20.1168 meters)

noncomputable def LengthUnit.furlongs : LengthUnit

The length unit of a furlong (201.168 meters)

noncomputable def LengthUnit.kilometers : LengthUnit

The length unit of kilometers (10³ meters).

noncomputable def LengthUnit.miles : LengthUnit

The length unit of a mile (1609.344 meters).

noncomputable def LengthUnit.nauticalMiles : LengthUnit

The length unit of a nautical mile (1852 meters).

noncomputable def LengthUnit.astronomicalUnits : LengthUnit

The length unit of an astronomical unit (149,597,870,700 meters).

noncomputable def LengthUnit.lightYears : LengthUnit

The length unit of a light year (9,460,730,472,580,800 meters).

noncomputable def LengthUnit.parsecs : LengthUnit

The length unit of a parsec (648,000/π astronomicalUnits).

Relations between length units

theorem LengthUnit.miles_div_yards : miles / yards = ⟨1760, ⋯⟩

There are exactly 1760 yards in a mile.

theorem LengthUnit.furlongs_div_yards : furlongs / yards = ⟨220, ⋯⟩

There are exactly 220 yards in a furlong.