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 Physlib.SpaceAndTime.Time.TimeUnit
public import Physlib.SpaceAndTime.Space.LengthUnit
public import Physlib.ClassicalMechanics.Mass.MassUnit
public import Physlib.Electromagnetism.Charge.ChargeUnit
public import Physlib.Thermodynamics.Temperature.TemperatureUnits
public import Physlib.Units.LTMCTDimensionBase
public import Physlib.Meta.TODO.Basic
public import Mathlib.Analysis.SpecialFunctions.Pow.NNRealDimensions and unit
A unit in physics arises from choice of something in physics which is non-canonical.
An example is the choice of translationally-invariant metric on the time manifold TimeMan.
A dimension is a property of a quantity related to how it changes with respect to a change in the unit.
The fundamental choices one has in physics are related to:
Time
Length
Mass
Charge
Temperature
(In fact temperature is not really a fundamental choice, however we leave this as a TODO.)
From these fundamental choices one can construct all other units and dimensions.
Implementation details
Units within Physlib are implemented with the following convention:
The fundamental units, and the choices they correspond to, are defined within the appropriate physics directory, in particular:
Physlib/SpaceAndTime/Time/TimeUnit.lean
Physlib/SpaceAndTime/Space/LengthUnit.lean
Physlib/ClassicalMechanics/Mass/MassUnit.lean
Physlib/Electromagnetism/Charge/ChargeUnit.lean
Physlib/Thermodynamics/Temperature/TemperatureUnit.lean
In this Units directory, we define the necessary structures and properties
to work derived units and dimensions.
References
Zulip chats discussing units:
https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/physical.20units
https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Dimensional.20Analysis.20Revisited/with/530238303
Note
A lot of the results around units is still experimental and should be adapted based on needs.
Other implementations of units
There are other implementations of units in Lean, in particular:
https://github.com/ATOMSLab/LeanDimensionalAnalysis/tree/main
https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SI.lean
https://github.com/ecyrbe/lean-units
Each of these have their own advantages and specific use-cases.
For example both (1) and (3) allow for or work in Floats, allowing computability and the use
of #eval. This is currently not possible with the more theoretical implementation here
in Physlib which is based exclusively on Reals.
@[expose] public sectionUnits
The choice of units.
The length unit.
The time unit.
The mass unit.
The charge unit.
The temperature unit.
@[ext]
structure LTMCTUnitChoices where length : LengthUnit time : TimeUnit mass : MassUnit charge : ChargeUnit temperature : TemperatureUnitlemma dimScale_apply (u1 u2 : LTMCTUnitChoices) (d : Dimension LTMCTDimensionBase) :
dimScale u1 u2 d =
(u1.length / u2.length) ^ (d.length : ℝ) *
(u1.time / u2.time) ^ (d.time : ℝ) *
(u1.mass / u2.mass) ^ (d.mass : ℝ) *
(u1.charge / u2.charge) ^ (d.charge : ℝ) *
(u1.temperature / u2.temperature) ^ (d.temperature : ℝ) := rfl@[simp]
lemma dimScale_self (u : LTMCTUnitChoices) (d : Dimension LTMCTDimensionBase) :
dimScale u u d = 1 := u:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u.dimScale u) d = 1
All goals completed! 🐙@[simp]
lemma dimScale_one (u1 u2 : LTMCTUnitChoices) :
dimScale u1 u2 1 = 1 := u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (u1.dimScale u2) 1 = 1
All goals completed! 🐙u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu3:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (↑⟨u1.length.val / u2.length.val, ⋯⟩ * ↑⟨u2.length.val / u3.length.val, ⋯⟩) ^ ↑d.length *
(↑⟨u1.time.val / u2.time.val, ⋯⟩ * ↑⟨u2.time.val / u3.time.val, ⋯⟩) ^ ↑d.time *
(↑⟨u1.mass.val / u2.mass.val, ⋯⟩ * ↑⟨u2.mass.val / u3.mass.val, ⋯⟩) ^ ↑d.mass *
(↑⟨u1.charge.val / u2.charge.val, ⋯⟩ * ↑⟨u2.charge.val / u3.charge.val, ⋯⟩) ^ ↑d.charge *
(↑⟨u1.temperature.val / u2.temperature.val, ⋯⟩ * ↑⟨u2.temperature.val / u3.temperature.val, ⋯⟩) ^ ↑d.temperature =
↑⟨u1.length.val / u3.length.val, ⋯⟩ ^ ↑d.length * ↑⟨u1.time.val / u3.time.val, ⋯⟩ ^ ↑d.time *
↑⟨u1.mass.val / u3.mass.val, ⋯⟩ ^ ↑d.mass *
↑⟨u1.charge.val / u3.charge.val, ⋯⟩ ^ ↑d.charge *
↑⟨u1.temperature.val / u3.temperature.val, ⋯⟩ ^ ↑d.temperature
All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙
All goals completed! 🐙@[simp]
lemma dimScale_ne_zero (u1 u2 : LTMCTUnitChoices) (d : Dimension LTMCTDimensionBase) :
dimScale u1 u2 d ≠ 0 := u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.dimScale u2) d ≠ 0
All goals completed! 🐙All goals completed! 🐙lemma dimScale_of_inv_eq_swap (u1 u2 : LTMCTUnitChoices) (d : Dimension LTMCTDimensionBase) :
dimScale u1 u2 d⁻¹ = dimScale u2 u1 d := u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.dimScale u2) d⁻¹ = (u2.dimScale u1) d
u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ ((u1.dimScale u2) d)⁻¹ = (u2.dimScale u1) d
conv_rhs => u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase| ((u1.dimScale u2) d)⁻¹@[simp]
lemma smul_dimScale_injective {M : Type} [MulAction ℝ≥0 M] (u1 u2 : LTMCTUnitChoices)
(d : Dimension LTMCTDimensionBase) (m1 m2 : M) :
(u1.dimScale u2 d) • m1 = (u1.dimScale u2 d) • m2 ↔ m1 = m2:= M:Typeinst✝:MulAction ℝ≥0 Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBasem1:Mm2:M⊢ (u1.dimScale u2) d • m1 = (u1.dimScale u2) d • m2 ↔ m1 = m2
M:Typeinst✝:MulAction ℝ≥0 Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBasem1:Mm2:M⊢ IsUnit ((u1.dimScale u2) d)
M:Typeinst✝:MulAction ℝ≥0 Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBasem1:Mm2:M⊢ ∃ b, (u1.dimScale u2) d * b = 1
M:Typeinst✝:MulAction ℝ≥0 Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBasem1:Mm2:M⊢ (u1.dimScale u2) d * (u1.dimScale u2) d⁻¹ = 1
All goals completed! 🐙@[simp]
lemma dimScale_pos (u1 u2 : LTMCTUnitChoices) (d : Dimension LTMCTDimensionBase) :
0 < (dimScale u1 u2 d) := u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ 0 < (u1.dimScale u2) d
u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ 0 ≤ (u1.dimScale u2) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ 0 ≠ (u1.dimScale u2) d
u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ 0 ≤ (u1.dimScale u2) d All goals completed! 🐙
u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ 0 ≠ (u1.dimScale u2) d All goals completed! 🐙TODO "Make SI : LTMCTUnitChoices computable, probably by
replacing the axioms defining the units. See here:
https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/physical.20units/near/534914807"@[simp]
lemma SI_length : SI.length = LengthUnit.meters := rfl@[simp]
lemma SI_time : SI.time = TimeUnit.seconds := rfl@[simp]
lemma SI_mass : SI.mass = MassUnit.kilograms := rfl@[simp]
lemma SI_charge : SI.charge = ChargeUnit.coulombs := rfl@[simp]
lemma SI_temperature : SI.temperature = TemperatureUnit.kelvin := rfl@[simp]
lemma dimScale_SI_SIPrimed (d : Dimension LTMCTDimensionBase) :
dimScale SI SIPrimed d =
(2⁻¹ : ℝ≥0) ^ (d.length : ℝ) *
(3⁻¹ : ℝ≥0) ^ (d.time : ℝ) *
(5⁻¹ : ℝ≥0) ^ (d.mass : ℝ) *
(7⁻¹ : ℝ≥0) ^ (d.charge : ℝ) *
(11⁻¹ : ℝ≥0) ^ (d.temperature : ℝ) := d:Dimension LTMCTDimensionBase⊢ (SI.dimScale SIPrimed) d = 2⁻¹ ^ ↑d.length * 3⁻¹ ^ ↑d.time * 5⁻¹ ^ ↑d.mass * 7⁻¹ ^ ↑d.charge * 11⁻¹ ^ ↑d.temperature
d:Dimension LTMCTDimensionBase⊢ ⟨2⁻¹, ⋯⟩ ^ ↑d.length * ⟨3⁻¹, ⋯⟩ ^ ↑d.time * ⟨5⁻¹, ⋯⟩ ^ ↑d.mass * ⟨7⁻¹, ⋯⟩ ^ ↑d.charge * ⟨11⁻¹, ⋯⟩ ^ ↑d.temperature =
2⁻¹ ^ ↑d.length * 3⁻¹ ^ ↑d.time * 5⁻¹ ^ ↑d.mass * 7⁻¹ ^ ↑d.charge * 11⁻¹ ^ ↑d.temperature
All goals completed! 🐙@[simp]
lemma dimScale_SIPrimed_SI (d : Dimension LTMCTDimensionBase) :
dimScale SIPrimed SI d =
(2 : ℝ≥0) ^ (d.length : ℝ) *
(3 : ℝ≥0) ^ (d.time : ℝ) *
(5 : ℝ≥0) ^ (d.mass : ℝ) *
(7 : ℝ≥0) ^ (d.charge : ℝ) *
(11 : ℝ≥0) ^ (d.temperature : ℝ) := d:Dimension LTMCTDimensionBase⊢ (SIPrimed.dimScale SI) d = 2 ^ ↑d.length * 3 ^ ↑d.time * 5 ^ ↑d.mass * 7 ^ ↑d.charge * 11 ^ ↑d.temperature
d:Dimension LTMCTDimensionBase⊢ ⟨2, ⋯⟩ ^ ↑d.length * ⟨3, ⋯⟩ ^ ↑d.time * ⟨5, ⋯⟩ ^ ↑d.mass * ⟨7, ⋯⟩ ^ ↑d.charge * ⟨11, ⋯⟩ ^ ↑d.temperature =
2 ^ ↑d.length * 3 ^ ↑d.time * 5 ^ ↑d.mass * 7 ^ ↑d.charge * 11 ^ ↑d.temperature
All goals completed! 🐙Types carrying dimensions
Dimensions are assigned to types with the following type-classes
HasDim for any type M with an associated dimension
CarriesDimension for a type that also has an instance of MulAction ℝ≥0 M
This typeclass indicates that there is a dimension dim M : Dimension
associated with the type M.
The dimension associated with a type M.
class HasDim (M : Type) where d : Dimension LTMCTDimensionBasealias dim := HasDim.d
A type M carries a dimension d if every element of M is supposed to have
this dimension. For example, the type Time will carry a dimension T𝓭.
class abbrev CarriesDimension (M : Type) := HasDim M, MulAction ℝ≥0 MTerms of the current dimension
Given a type M which carries a dimension d,
we are interested in elements of M which depend on a choice of units, i.e. functions
LTMCTUnitChoices → M.
We define both a proposition
HasDimension f which says that f scales correctly with units,
and a type
Dimensionful M which is the subtype of functions which HasDimension.
A quantity of type M which depends on a choice of units LTMCTUnitChoices is said to be
of dimension d if it scales by LTMCTUnitChoices.dimScale u1 u2 d under a change in units.
def HasDimension {M : Type} [CarriesDimension M] (f : LTMCTUnitChoices → M) : Prop :=
∀ u1 u2 : LTMCTUnitChoices, f u2 = LTMCTUnitChoices.dimScale u1 u2 (dim M) • f u1lemma hasDimension_iff {M : Type} [CarriesDimension M] (f : LTMCTUnitChoices → M) :
HasDimension f ↔ ∀ u1 u2 : LTMCTUnitChoices, f u2 =
LTMCTUnitChoices.dimScale u1 u2 (dim M) • f u1 := M:Typeinst✝:CarriesDimension Mf:LTMCTUnitChoices → M⊢ HasDimension f ↔ ∀ (u1 u2 : LTMCTUnitChoices), f u2 = (u1.dimScale u2) (dim M) • f u1
All goals completed! 🐙
The subtype of functions LTMCTUnitChoices → M, for which M carries a dimension,
which HasDimension.
def Dimensionful (M : Type) [CarriesDimension M] := Subtype (HasDimension (M := M))instance {M : Type} [CarriesDimension M] :
CoeFun (Dimensionful M) (fun _ => LTMCTUnitChoices → M) where
coe := Subtype.val@[ext]
lemma Dimensionful.ext {M : Type} [CarriesDimension M] (f1 f2 : Dimensionful M)
(h : f1.val = f2.val) : f1 = f2 := M:Typeinst✝:CarriesDimension Mf1:Dimensionful Mf2:Dimensionful Mh:↑f1 = ↑f2⊢ f1 = f2
M:Typeinst✝:CarriesDimension Mf2:Dimensionful Mval✝:LTMCTUnitChoices → Mproperty✝:HasDimension val✝h:↑⟨val✝, property✝⟩ = ↑f2⊢ ⟨val✝, property✝⟩ = f2
M:Typeinst✝:CarriesDimension Mval✝¹:LTMCTUnitChoices → Mproperty✝¹:HasDimension val✝val✝:LTMCTUnitChoices → Mproperty✝:HasDimension val✝h:↑⟨val✝¹, property✝¹⟩ = ↑⟨val✝, property✝⟩⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩
All goals completed! 🐙All goals completed! 🐙@[simp]
lemma Dimensionful.smul_apply {M : Type} [CarriesDimension M]
(a : ℝ≥0) (f : Dimensionful M) (u : LTMCTUnitChoices) :
(a • f).1 u = a • f.1 u := rfllemma CarriesDimension.toDimensionful_apply_apply
{M : Type} [CarriesDimension M] (u1 u2 : LTMCTUnitChoices) (m : M) :
(toDimensionful u1 m).1 u2 = (u1.dimScale u2 (dim M)) • m := M:Typeinst✝:CarriesDimension Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm:M⊢ ↑((toDimensionful u1) m) u2 = (u1.dimScale u2) (dim M) • m All goals completed! 🐙