Time

In this module we define the type Time, corresponding to time in a given (but arbitary) set of units, with a given (but arbitary) 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.

structure Time : Type

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

• val : ℝ

  The underlying real number associated with a point in time.

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

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

theorem Time.val_injective : Function.Injective val

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 } }

instance Time.instCoeReal : Coe ℝ Time

Equations

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

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

instance Time.instInhabited : Inhabited Time

Equations

• Time.instInhabited = { default := 0 }

@[simp]

theorem Time.default_eq_zero : default = 0

Coercions

@[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.realCast_of_natCast {n : ℕ} : { val := ↑n } = ↑n

The choice of zero, one, and orientation

@[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

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

Basic operations on Time.

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

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

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

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

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.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

Instances 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.

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 }

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

noncomputable instance Time.instDecidableEq : DecidableEq Time

Equations

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

instance Time.instMeasurableSpace : MeasurableSpace Time

Equations

• Time.instMeasurableSpace = borel Time

instance Time.instBorelSpace : BorelSpace Time

instance Time.instFiniteDimensionalReal : FiniteDimensional ℝ Time

noncomputable instance Time.instInnerProductSpaceReal : InnerProductSpace ℝ Time

Equations

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

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 isomentry equivalence from Time to ℝ.

Equations

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

instance Time.instCoeReal_1 : Coe Time ℝ

Equations

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

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

Derivatives

noncomputable def Time.deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (f : Time → M) : Time → M

Given a function f : Time → M the derivative of f.

Equations

• Time.deriv f t = (fderiv ℝ f t) 1

def Time.«term∂ₜ» : Lean.ParserDescr

Given a function f : Time → M the derivative of f.

Equations

• Time.«term∂ₜ» = Lean.ParserDescr.node `Time.«term∂ₜ» 1024 (Lean.ParserDescr.symbol "∂ₜ")

theorem Time.deriv_eq {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (f : Time → M) (t : Time) : deriv f t = (fderiv ℝ f t) 1

theorem Time.deriv_smul {d : ℕ} {t : Time} (f : Time → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : deriv (fun (t : Time) => k • f t) t = k • deriv (fun (t : Time) => f t) t

theorem Time.deriv_neg {M : Type} {t : Time} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) : deriv (-f) t = -deriv f t

theorem Time.val_differentiable : Differentiable ℝ val

@[simp]

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