Time

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

A. The definition of Time

structure Time : Type

The type Time represents the time in a given (but arbitrary) set of units, and with a given (but arbitrary) choice of origin.

• val : ℝ

  The underlying real number associated with a point in time.

theorem Time.ext {x y : Time} (val : x.val = y.val) : x = y

theorem Time.ext_iff {x y : Time} : x = y ↔ x.val = y.val

theorem Time.val_injective : Function.Injective val

B. Instances on Time

B.1. Natural numbers as elements of Time

instance Time.instNatCast : NatCast Time

Equations

• Time.instNatCast = { natCast := fun (n : ℕ) => { val := ↑n } }

instance Time.instOfNat {n : ℕ} : OfNat Time 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).

Equations

• Time.instOfNat = { ofNat := { val := ↑n } }

@[simp]

theorem Time.natCast_val {n : ℕ} : (↑n).val = ↑n

@[simp]

theorem Time.natCast_zero : ↑0 = 0

@[simp]

theorem Time.natCast_one : ↑1 = 1

@[simp]

theorem Time.ofNat_val {n : ℕ} : val (OfNat.ofNat n) = ↑n

theorem Time.one_ne_zero : 1 ≠ 0

@[simp]

theorem Time.zero_val : val 0 = 0

@[simp]

theorem Time.eq_zero_iff (t : Time) : t = 0 ↔ t.val = 0

@[simp]

theorem Time.one_val : val 1 = 1

@[simp]

theorem Time.eq_one_iff (t : Time) : t = 1 ↔ t.val = 1

B.2. Real numbers as elements of Time

instance Time.instCoeReal : Coe ℝ Time

Equations

• Time.instCoeReal = { coe := fun (r : ℝ) => { val := r } }

instance Time.instCoeReal_1 : Coe Time ℝ

Equations

• Time.instCoeReal_1 = { coe := Time.val }

theorem Time.realCast_val {r : ℝ} : { val := r }.val = r

@[simp]

theorem Time.realCast_of_natCast {n : ℕ} : { val := ↑n } = ↑n

B.3. Time is inhabited

instance Time.instInhabited : Inhabited Time

Equations

• Time.instInhabited = { default := 0 }

@[simp]

theorem Time.default_eq_zero : default = 0

B.4. The order on Time

instance Time.instLE : LE Time

The choice of an orientation on Time.

Equations

• Time.instLE = { le := fun (t1 t2 : Time) => t1.val ≤ t2.val }

theorem Time.le_def (t1 t2 : Time) : t1 ≤ t2 ↔ t1.val ≤ t2.val

instance Time.instPartialOrder : PartialOrder Time

Equations

• One or more equations did not get rendered due to their size.

theorem Time.lt_def (t1 t2 : Time) : t1 < t2 ↔ t1.val < t2.val

B.5. Addition of times

instance Time.instAdd : Add Time

Equations

• Time.instAdd = { add := fun (t1 t2 : Time) => { val := t1.val + t2.val } }

@[simp]

theorem Time.add_val (t1 t2 : Time) : (t1 + t2).val = t1.val + t2.val

B.6. Negation of times

instance Time.instNeg : Neg Time

Equations

• Time.instNeg = { neg := fun (t : Time) => { val := -t.val } }

@[simp]

theorem Time.neg_val (t : Time) : (-t).val = -t.val

B.7. Subtraction of times

instance Time.instSub : Sub Time

Equations

• Time.instSub = { sub := fun (t1 t2 : Time) => { val := t1.val - t2.val } }

@[simp]

theorem Time.sub_val (t1 t2 : Time) : (t1 - t2).val = t1.val - t2.val

B.8. Scalar multiplication of time

instance Time.instSMulReal : SMul ℝ Time

Equations

• Time.instSMulReal = { smul := fun (k : ℝ) (t : Time) => { val := k * t.val } }

@[simp]

theorem Time.smul_real_val (k : ℝ) (t : Time) : (k • t).val = k * t.val

B.9. Module on Time

instance Time.instAddGroup : AddGroup Time

Equations

• One or more equations did not get rendered due to their size.

instance Time.instAddCommGroup : AddCommGroup Time

Equations

• Time.instAddCommGroup = { toAddGroup := Time.instAddGroup, add_comm := Time.instAddCommGroup._proof_1 }

instance Time.instModuleReal : Module ℝ Time

Equations

• One or more equations did not get rendered due to their size.

B.10. Norm of time

instance Time.instNorm : Norm Time

Equations

• Time.instNorm = { norm := fun (t : Time) => ‖t.val‖ }

instance Time.instDist : Dist Time

Equations

• Time.instDist = { dist := fun (t1 t2 : Time) => ‖t1 - t2‖ }

theorem Time.dist_eq_val (t1 t2 : Time) : dist t1 t2 = ‖t1.val - t2.val‖

theorem Time.dist_eq_real_dist (t1 t2 : Time) : dist t1 t2 = dist t1.val t2.val

instance Time.instSeminormedAddCommGroup : SeminormedAddCommGroup Time

Equations

• One or more equations did not get rendered due to their size.

instance Time.instNormedAddCommGroup : NormedAddCommGroup Time

Equations

• One or more equations did not get rendered due to their size.

instance Time.instNormedSpaceReal : NormedSpace ℝ Time

Equations

• Time.instNormedSpaceReal = { toModule := Time.instModuleReal, norm_smul_le := Time.instNormedSpaceReal._proof_1 }

B.11. Inner product on Time

instance Time.instInnerReal : Inner ℝ Time

Equations

• Time.instInnerReal = { inner := fun (t1 t2 : Time) => t1.val * t2.val }

@[simp]

theorem Time.inner_def (t1 t2 : Time) : inner ℝ t1 t2 = t1.val * t2.val

noncomputable instance Time.instInnerProductSpaceReal : InnerProductSpace ℝ Time

Equations

• One or more equations did not get rendered due to their size.

B.12. Decidability of Time

noncomputable instance Time.instDecidableEq : DecidableEq Time

Equations

• t1.instDecidableEq t2 = decidable_of_iff (t1.val = t2.val) ⋯

B.13. Measurability of Time

instance Time.instMeasurableSpace : MeasurableSpace Time

Equations

• Time.instMeasurableSpace = borel Time

instance Time.instBorelSpace : BorelSpace Time

C. Basis of Time

noncomputable def Time.basis : OrthonormalBasis (Fin 1) ℝ Time

The orthonomral basis on Time defined by 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Time.basis_apply_eq_one (i : Fin 1) : basis i = 1

@[simp]

theorem Time.rank_eq_one : Module.rank ℝ Time = 1

@[simp]

theorem Time.finRank_eq_one : Module.finrank ℝ Time = 1

instance Time.instFiniteDimensionalReal : FiniteDimensional ℝ Time

theorem Time.volume_eq_basis_addHaar : MeasureTheory.volume = basis.toBasis.addHaar

D. Maps from Time to ℝ

noncomputable def Time.toRealCLM : Time →L[ℝ] ℝ

The continuous linear map from Time to ℝ.

Equations

• Time.toRealCLM = LinearMap.toContinuousLinearMap { toFun := Time.val, map_add' := Time.toRealCLM._proof_8, map_smul' := Time.toRealCLM._proof_9 }

noncomputable def Time.toRealCLE : Time ≃L[ℝ] ℝ

The continuous linear equivalence from Time to ℝ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Time.toRealLIE : Time ≃ₗᵢ[ℝ] ℝ

The linear isometry equivalence from Time to ℝ.

Equations

• One or more equations did not get rendered due to their size.

theorem Time.eq_one_smul (t : Time) : t = t.val • 1

theorem Time.val_measurable : Measurable val

theorem Time.val_measurableEmbedding : MeasurableEmbedding val

theorem Time.val_measurePreserving : MeasureTheory.MeasurePreserving val MeasureTheory.volume MeasureTheory.volume

theorem Time.val_differentiable : Differentiable ℝ val

@[simp]

theorem Time.fderiv_val (t : Time) : (fderiv ℝ val t) 1 = 1