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.Calculus.FDeriv.Linear
public import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpaceTime
i. Overview
In this module we define the type Time, corresponding to time in a given
(but arbitrary) set of units, with a given (but arbitrary) choice of origin (time zero),
and a choice of orientation (i.e. a positive time direction).
We note that this is the version of time most often used in undergraduate and non-mathematical physics.
The choice of units or origin can be made on a case-by-case basis, as
long as they are done consistently. However, since the choice of units and origin is
left implicit, Lean will not catch inconsistencies in the choice of units or origin when
working with Time.
For example, for the classical mechanics system corresponding to the harmonic oscillator,
one can take the origin of time to be the time at which the initial conditions are specified,
and the units can be taken as anything as long as the units chosen for time t and
the angular frequency ω are consistent.
With this notion of Time, becomes a 1d vector space over ℝ with an inner product.
Within other modules e.g. TimeMan and TimeTransMan, we define
versions of time with less choices made, and relate them to Time via a choice of units
or origin.
ii. Key results
Time : The type representing time with a choice of units and origin.
iii. Table of contents
A. The definition of Time
B. Instances on Time
B.1. Natural numbers as elements of Time
B.2. Real numbers as elements of Time
B.3. Time is inhabited
B.4. The order on Time
B.5. Addition of times
B.6. Negation of times
B.7. Subtraction of times
B.8. Scalar multiplication of time
B.9. Module on Time
B.10. Norm of time
B.11. Inner product on Time
B.12. Decidability of Time
B.13. Measurability of Time
C. Basis of Time
D. Maps from Time to ℝ
iv. References
@[expose] public section
A. The definition of Time
The type Time represents the time in a given (but arbitrary) set of units, and
with a given (but arbitrary) choice of origin.
The underlying real number associated with a point in time.
@[ext]
structure Time where val : ℝlemma val_injective : Function.Injective val := fun _ _ h => Time.ext hB. Instances on Time
B.1. Natural numbers as elements of Time
instance : NatCast Time where
natCast n := ⟨n⟩
The casting of a natural number to an element of Time. This corresponds to a choice of
(1) zero point in time, and (2) a choice of metric on time (defining 1).
instance {n : ℕ} : OfNat Time n where
ofNat := ⟨n⟩@[simp]
lemma natCast_val {n : ℕ} : val n = n := rfl@[simp]
lemma natCast_zero : ((0 : ℕ) : Time) = 0 := rfl@[simp]
lemma natCast_one : ((1 : ℕ) : Time) = 1 := rfl@[simp]
lemma ofNat_val {n : ℕ} : val (OfNat.ofNat n : Time) = n := rfllemma one_ne_zero : (1 : Time) ≠ (0 : Time) :=
mt (congrArg val) (Nat.cast_injective.ne Nat.one_ne_zero)@[simp]
lemma zero_val : val 0 = 0 := ⊢ val 0 = 0 All goals completed! 🐙@[simp]
lemma eq_zero_iff (t : Time) : t = 0 ↔ t.val = 0 := t:Time⊢ t = 0 ↔ t.val = 0 All goals completed! 🐙@[simp]
lemma one_val : val 1 = 1 := ⊢ val 1 = 1 All goals completed! 🐙@[simp]
lemma eq_one_iff (t : Time) : t = 1 ↔ t.val = 1 := t:Time⊢ t = 1 ↔ t.val = 1 All goals completed! 🐙
B.2. Real numbers as elements of Time
instance : Coe ℝ Time where
coe r := ⟨r⟩instance : Coe Time ℝ where
coe := Time.vallemma realCast_val {r : ℝ} : (r : Time).val = r := rfl@[simp]
lemma realCast_of_natCast {n : ℕ} : ((n : ℝ) : Time) = n := rflB.3. Time is inhabited
instance : Inhabited Time where
default := 0@[simp]
lemma default_eq_zero : default = 0 := rfl
B.4. The order on Time
The choice of an orientation on Time.
lemma le_def (t1 t2 : Time) :
t1 ≤ t2 ↔ t1.val ≤ t2.val := Iff.rflinstance : PartialOrder Time where
le_refl t := t:Time⊢ t ≤ t All goals completed! 🐙
le_trans t1 t2 t3 := t1:Timet2:Timet3:Time⊢ t1 ≤ t2 → t2 ≤ t3 → t1 ≤ t3 t1:Timet2:Timet3:Time⊢ t1.val ≤ t2.val → t2.val ≤ t3.val → t1.val ≤ t3.val; All goals completed! 🐙
le_antisymm t1 t2 h1 h2 := t1:Timet2:Timeh1:t1 ≤ t2h2:t2 ≤ t1⊢ t1 = t2 t1:Timet2:Timeh1:t1.val ≤ t2.valh2:t2.val ≤ t1.val⊢ t1 = t2; t1:Timet2:Timeh1:t1.val ≤ t2.valh2:t2.val ≤ t1.val⊢ t1.val = t2.val; All goals completed! 🐙lemma lt_def (t1 t2 : Time) :
t1 < t2 ↔ t1.val < t2.val := t1:Timet2:Time⊢ t1 < t2 ↔ t1.val < t2.val All goals completed! 🐙B.5. Addition of times
instance : Add Time where
add t1 t2 := ⟨t1.val + t2.val⟩@[simp]
lemma add_val (t1 t2 : Time) :
(t1 + t2).val = t1.val + t2.val := rflB.6. Negation of times
instance : Neg Time where
neg t := ⟨-t.val⟩@[simp]
lemma neg_val (t : Time) :
(-t).val = -t.val := rflB.7. Subtraction of times
instance : Sub Time where
sub t1 t2 := ⟨t1.val - t2.val⟩@[simp]
lemma sub_val (t1 t2 : Time) :
(t1 - t2).val = t1.val - t2.val := rflB.8. Scalar multiplication of time
instance : SMul ℝ Time where
smul k t := ⟨k * t.val⟩@[simp]
lemma smul_real_val (k : ℝ) (t : Time) :
(k • t).val = k * t.val := rfl
B.9. Module on Time
instance : AddGroup Time where
add_assoc t1 t2 t3 := t1:Timet2:Timet3:Time⊢ t1 + t2 + t3 = t1 + (t2 + t3) t1:Timet2:Timet3:Time⊢ (t1 + t2 + t3).val = (t1 + (t2 + t3)).val; All goals completed! 🐙
zero_add t := t:Time⊢ 0 + t = t t:Time⊢ (0 + t).val = t.val; All goals completed! 🐙
add_zero t := t:Time⊢ t + 0 = t t:Time⊢ (t + 0).val = t.val; All goals completed! 🐙
neg_add_cancel t := t:Time⊢ -t + t = 0 t:Time⊢ (-t + t).val = val 0; All goals completed! 🐙
nsmul := nsmulRec
zsmul := zsmulRecinstance : AddCommGroup Time where
add_comm := ⊢ ∀ (a b : Time), a + b = b + a a✝:Timeb✝:Time⊢ a✝ + b✝ = b✝ + a✝; a✝:Timeb✝:Time⊢ (a✝ + b✝).val = (b✝ + a✝).val; All goals completed! 🐙instance : Module ℝ Time where
one_smul t := t:Time⊢ 1 • t = t t:Time⊢ (1 • t).val = t.val; All goals completed! 🐙
smul_add k t1 t2 := k:ℝt1:Timet2:Time⊢ k • (t1 + t2) = k • t1 + k • t2 k:ℝt1:Timet2:Time⊢ (k • (t1 + t2)).val = (k • t1 + k • t2).val; All goals completed! 🐙
smul_zero k := k:ℝ⊢ k • 0 = 0 k:ℝ⊢ (k • 0).val = val 0; All goals completed! 🐙
add_smul k1 k2 t := k1:ℝk2:ℝt:Time⊢ (k1 + k2) • t = k1 • t + k2 • t k1:ℝk2:ℝt:Time⊢ ((k1 + k2) • t).val = (k1 • t + k2 • t).val; All goals completed! 🐙
mul_smul k1 k2 t := k1:ℝk2:ℝt:Time⊢ (k1 * k2) • t = k1 • k2 • t k1:ℝk2:ℝt:Time⊢ ((k1 * k2) • t).val = (k1 • k2 • t).val; All goals completed! 🐙
zero_smul t := t:Time⊢ 0 • t = 0 t:Time⊢ (0 • t).val = val 0; All goals completed! 🐙B.10. Norm of time
instance : Norm Time where
norm t := ‖t.val‖lemma norm_eq_val (t : Time) :
‖t‖ = ‖t.val‖ := rflinstance : Dist Time where
dist t1 t2 := ‖t1 - t2‖lemma dist_eq_val (t1 t2 : Time) :
dist t1 t2 = ‖t1.val - t2.val‖ := rfllemma dist_eq_real_dist (t1 t2 : Time) :
dist t1 t2 = dist t1.val t2.val := t1:Timet2:Time⊢ dist t1 t2 = dist t1.val t2.val All goals completed! 🐙t1:Timet2:Time⊢ (t1.val - t2.val) * (t1.val - t2.val) = (-t1.val + t2.val) * (-t1.val + t2.val)
All goals completed! 🐙t1:Timet2:Time⊢ (t1.val - t2.val) * (t1.val - t2.val) = (-t1.val + t2.val) * (-t1.val + t2.val)
All goals completed! 🐙instance : NormedSpace ℝ Time where
norm_smul_le k t := k:ℝt:Time⊢ ‖k • t‖ ≤ ‖k‖ * ‖t‖ All goals completed! 🐙
B.11. Inner product on Time
instance : Inner ℝ Time where
inner t1 t2 := t1.val * t2.val@[simp]
lemma inner_def (t1 t2 : Time) :
⟪t1, t2⟫_ℝ = t1.val * t2.val := rfl
B.12. Decidability of Time
B.13. Measurability of Time
instance : MeasurableSpace Time := borel Timeinstance : BorelSpace Time where
measurable_eq := ⊢ instMeasurableSpace = borel Time All goals completed! 🐙
C. Basis of Time
@[simp]
lemma basis_apply_eq_one (i : Fin 1) :
basis i = 1 := i:Fin 1⊢ basis i = 1
⊢ basis ((fun i => i) ⟨0, ⋯⟩) = 1
⊢ ({ toFun := fun x => WithLp.toLp 2 fun x_1 => x.val, map_add' := basis._proof_3, map_smul' := basis._proof_4,
invFun := fun f => { val := f.ofLp 0 }, left_inv := basis._proof_6, right_inv := basis._proof_7,
norm_map' := basis._proof_8 }.symm
(EuclideanSpace.single 0 1)).val =
1
All goals completed! 🐙@[simp]
lemma rank_eq_one : Module.rank ℝ Time = 1 :=
rank_eq_one_iff.mpr ⟨1, one_ne_zero, fun v => ⟨v.val, Time.ext (v:Time⊢ (v.val • 1).val = v.val All goals completed! 🐙)⟩⟩@[simp]
lemma finRank_eq_one : Module.finrank ℝ Time = 1 :=
Module.rank_eq_one_iff_finrank_eq_one.mp rank_eq_oneinstance : FiniteDimensional ℝ Time := Module.finite_of_rank_eq_one rank_eq_onelemma volume_eq_basis_addHaar :
(volume (α := Time)) = basis.toBasis.addHaar := basis.addHaar_eq_volume.symm
D. Maps from Time to ℝ
lemma eq_one_smul (t : Time) :
t = t.val • 1 := Time.ext (t:Time⊢ t.val = (t.val • 1).val All goals completed! 🐙)@[fun_prop]
lemma val_measurable : Measurable Time.val := toRealCLE.continuous.measurablelemma val_measurableEmbedding : MeasurableEmbedding Time.val :=
toRealCLE.toHomeomorph.measurableEmbeddinglemma val_measurePreserving : MeasurePreserving Time.val volume volume :=
LinearIsometryEquiv.measurePreserving toRealLIE@[fun_prop]
lemma val_differentiable : Differentiable ℝ Time.val := toRealCLM.differentiablet:Time⊢ toRealCLM 1 = 1
All goals completed! 🐙