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.RCLike.BasicUnits on Mass
A unit of mass corresponds to a choice of translationally-invariant
metric on the mass manifold (to be defined diffeomorphic to ℝ≥0).
Such a choice is (non-canonically) equivalent to a
choice of positive real number. We define the type MassUnit to be equivalent to the
positive reals.
On MassUnit there is an instance of division giving a real number, corresponding to the
ratio of the two scales of mass unit.
To define specific mass units, we first state the existence of a a given mass unit, and then construct all other mass units from it. We choose to state the existence of the mass unit of kilograms, and construct all other mass units from that.
@[expose] public sectionThe choices of translationally-invariant metrics on the mass-manifold. Such a choice corresponds to a choice of units for mass.
The underlying scale of the unit.
structure MassUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : MassUnit) : x.val ≠ 0 := x:MassUnit⊢ x.val ≠ 0
All goals completed! 🐙lemma val_pos (x : MassUnit) : 0 < x.val := x.propertyinstance : Inhabited MassUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩Division of MassUnit
lemma div_eq_val (x y : MassUnit) :
x / y = (⟨x.val / y.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt y.val_pos)⟩ : ℝ≥0) := rflx:MassUnity:MassUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0
x:MassUnity:MassUnit⊢ ↑⟨x.val / y.val, ⋯⟩ ≠ 0
All goals completed! 🐙@[simp]
lemma div_pos (x y : MassUnit) : (0 : ℝ≥0) < x/ y := x:MassUnity:MassUnit⊢ 0 < x / y
x:MassUnity:MassUnit⊢ 0 ≤ x / yx:MassUnity:MassUnit⊢ 0 ≠ x / y
x:MassUnity:MassUnit⊢ 0 ≤ x / y All goals completed! 🐙
x:MassUnity:MassUnit⊢ 0 ≠ x / y All goals completed! 🐙@[simp]
lemma div_self (x : MassUnit) :
x / x = (1 : ℝ≥0) := x:MassUnit⊢ x / x = 1
x:MassUnit⊢ ⟨1, ⋯⟩ = 1
All goals completed! 🐙All goals completed! 🐙@[simp]
lemma div_mul_div_coe (x y z : MassUnit) :
(x / y : ℝ) * (y / z : ℝ) = x / z := x:MassUnity:MassUnitz:MassUnit⊢ ↑(x / y) * ↑(y / z) = ↑(x / z)
x:MassUnity:MassUnitz:MassUnit⊢ x.val / y.val * (y.val / z.val) = x.val / z.val
All goals completed! 🐙The scaling of a mass unit
The scaling of a mass unit by a positive real.
def scale (r : ℝ) (x : MassUnit) (hr : 0 < r := by norm_num) : MassUnit :=
⟨r * x.val, mul_pos hr x.val_pos⟩@[simp]
lemma scale_div_self (x : MassUnit) (r : ℝ) (hr : 0 < r) :
scale r x hr / x = (⟨r, le_of_lt hr⟩ : ℝ≥0) := x:MassUnitr:ℝhr:0 < r⊢ scale r x hr / x = ⟨r, ⋯⟩
All goals completed! 🐙@[simp]
lemma self_div_scale (x : MassUnit) (r : ℝ) (hr : 0 < r) :
x / scale r x hr = (⟨1/r, _root_.div_nonneg (x:MassUnitr:ℝhr:0 < r⊢ 0 ≤ 1 All goals completed! 🐙) (le_of_lt hr)⟩ : ℝ≥0) := x:MassUnitr:ℝhr:0 < r⊢ x / scale r x hr = ⟨1 / r, ⋯⟩
x:MassUnitr:ℝhr:0 < r⊢ ⟨x.val / (r * x.val), ⋯⟩ = ⟨r⁻¹, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_one (x : MassUnit) : scale 1 x = x := x:MassUnit⊢ scale 1 x ⋯ = x
All goals completed! 🐙x1:MassUnitx2:MassUnitr1:ℝ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 : MassUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) :
scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x (mul_pos hr1 hr2) := x:MassUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯
x:MassUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ r1 * (r2 * x.val) = r1 * r2 * x.val
All goals completed! 🐙Specific choices of mass units
To define a specific mass units.
We first define the notion of a kilogram to correspond to the mass unit with underlying value
equal to 1. This is really down to a choice in the isomorphism between the set of metrics
on the mass manifold and the positive reals.
From this choice of kilograms, we can define other length units by scaling kilograms.
The definition of a mass unit of kilograms.
def kilograms : MassUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩Relations between mass units
⊢ ↑⟨0.45359237, ⋯⟩ / ↑⟨28349523125e-12, ⋯⟩ = 16; All goals completed! 🐙⊢ ↑⟨2000 * 0.45359237, ⋯⟩ = 907.18474; All goals completed! 🐙⊢ ↑⟨2240 * 0.45359237, ⋯⟩ = 1016.0469088; All goals completed! 🐙