Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.BasicUnits 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.
@[expose] public sectionThe choices of translationally-invariant metrics on the space-manifold. Such a choice corresponds to a choice of units for length.
The underlying scale of the unit.
structure LengthUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : LengthUnit) : x.val ≠ 0 := x:LengthUnit⊢ x.val ≠ 0
All goals completed! 🐙lemma val_pos (x : LengthUnit) : 0 < x.val := x.propertyinstance : Inhabited LengthUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩Division of LengthUnit
lemma div_eq_val (x y : LengthUnit) :
(x / y) = (⟨x.val / y.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt y.val_pos)⟩ : ℝ≥0) := rflx:LengthUnity:LengthUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0
x:LengthUnity:LengthUnit⊢ ↑⟨x.val / y.val, ⋯⟩ ≠ 0
All goals completed! 🐙@[simp]
lemma div_pos (x y : LengthUnit) : (0 : ℝ≥0) < x/ y := x:LengthUnity:LengthUnit⊢ 0 < x / y
x:LengthUnity:LengthUnit⊢ 0 ≤ x / yx:LengthUnity:LengthUnit⊢ 0 ≠ x / y
x:LengthUnity:LengthUnit⊢ 0 ≤ x / y All goals completed! 🐙
x:LengthUnity:LengthUnit⊢ 0 ≠ x / y All goals completed! 🐙@[simp]
lemma div_self (x : LengthUnit) :
x / x = (1 : ℝ≥0) := x:LengthUnit⊢ x / x = 1
x:LengthUnit⊢ ⟨1, ⋯⟩ = 1
All goals completed! 🐙All goals completed! 🐙@[simp]
lemma div_mul_div_coe (x y z : LengthUnit) :
(x / y : ℝ) * (y / z : ℝ) = x / z := x:LengthUnity:LengthUnitz:LengthUnit⊢ ↑(x / y) * ↑(y / z) = ↑(x / z)
x:LengthUnity:LengthUnitz:LengthUnit⊢ x.val / y.val * (y.val / z.val) = x.val / z.val
All goals completed! 🐙The scaling of a length unit
The scaling of a length unit by a positive real.
def scale (r : ℝ) (x : LengthUnit) (hr : 0 < r := by norm_num) : LengthUnit :=
⟨r * x.val, mul_pos hr x.val_pos⟩@[simp]
lemma scale_div_self (x : LengthUnit) (r : ℝ) (hr : 0 < r) :
scale r x hr / x = (⟨r, le_of_lt hr⟩ : ℝ≥0) := x:LengthUnitr:ℝhr:0 < r⊢ scale r x hr / x = ⟨r, ⋯⟩
All goals completed! 🐙@[simp]
lemma self_div_scale (x : LengthUnit) (r : ℝ) (hr : 0 < r) :
x / scale r x hr = (⟨1/r, _root_.div_nonneg (x:LengthUnitr:ℝhr:0 < r⊢ 0 ≤ 1 All goals completed! 🐙) (le_of_lt hr)⟩ : ℝ≥0) := x:LengthUnitr:ℝhr:0 < r⊢ x / scale r x hr = ⟨1 / r, ⋯⟩
x:LengthUnitr:ℝhr:0 < r⊢ ⟨x.val / (r * x.val), ⋯⟩ = ⟨r⁻¹, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_one (x : LengthUnit) : scale 1 x = x := x:LengthUnit⊢ scale 1 x ⋯ = x
All goals completed! 🐙x1:LengthUnitx2:LengthUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_scale (x : LengthUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) :
scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x (mul_pos hr1 hr2) := x:LengthUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯
x:LengthUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ r1 * (r2 * x.val) = r1 * r2 * x.val
All goals completed! 🐙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.
The references for the numerical definitions used below are:
the BIPM SI Brochure for the meter, the speed of light, and SI prefixes: https://www.bipm.org/documents/d/guest/si-brochure-9-en-pdf
NIST Handbook 44, Appendix C, for the international foot-based units and the international nautical mile: https://doi.org/10.6028/NIST.HB.44-2023
IAU 2012 Resolution B2 for the astronomical unit: https://iauarchive.eso.org/static/resolutions/IAU2012_English.pdf
the IAU Style Manual recommendations for the Julian year convention used in the light-year: https://iauarchive.eso.org/publications/proceedings_rules/units/
IAU 2015 Resolution B2 for the exact parsec convention: https://iauarchive.eso.org/static/resolutions/IAU2015_English.pdf
The definition of a length unit of meters.
def meters : LengthUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩Relations between length units
There are exactly 1760 yards in a mile.
⊢ ↑⟨1609.344, ⋯⟩ / ↑⟨0.9144, ⋯⟩ = ↑⟨1760, ⋯⟩; All goals completed! 🐙There are exactly 220 yards in a furlong.
⊢ ↑⟨201.168, ⋯⟩ / ↑⟨0.9144, ⋯⟩ = ↑⟨220, ⋯⟩; All goals completed! 🐙