Units on time

A unit of time corresponds to a choice of translationally-invariant metric on the time manifold TimeTransMan. Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type TimeUnit to be equivalent to the positive reals.

On TimeUnit there is an instance of division giving a real number, corresponding to the ratio of the two scales of time unit.

We define HasTimeDimension to be a property of a function from TimeUnit to a type M which is a function that scales with the time unit with respect to the rational power d.

To define specific time units, we first state the existence of a a given time unit, and then construct all other time units from it. We choose to state the existence of the time unit of seconds, and construct all other time units from that.

structure TimeUnit : Type

The choices of translationally-invariant metrics on the manifold TimeTransMan. Such a choice corresponds to a choice of units for time.

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

theorem TimeUnit.val_neq_zero (x : TimeUnit) : x.val ≠ 0

theorem TimeUnit.val_pos (x : TimeUnit) : 0 < x.val

instance TimeUnit.instInhabited : Inhabited TimeUnit

Equations

• TimeUnit.instInhabited = { default := { val := 1, property := TimeUnit.instInhabited._proof_1 } }

Division of TimeUnit

noncomputable instance TimeUnit.instHDivNNReal : HDiv TimeUnit TimeUnit NNReal

Equations

• TimeUnit.instHDivNNReal = { hDiv := fun (x t : TimeUnit) => ⟨x.val / t.val, ⋯⟩ }

theorem TimeUnit.div_eq_val (x y : TimeUnit) : x / y = ⟨x.val / y.val, ⋯⟩

@[simp]

theorem TimeUnit.div_neq_zero (x y : TimeUnit) : ¬x / y = 0

@[simp]

theorem TimeUnit.div_pos (x y : TimeUnit) : 0 < x / y

@[simp]

theorem TimeUnit.div_self (x : TimeUnit) : x / x = 1

theorem TimeUnit.div_symm (x y : TimeUnit) : x / y = (y / x)⁻¹

@[simp]

theorem TimeUnit.div_mul_div_coe (x y z : TimeUnit) : ↑(x / y) * ↑(y / z) = ↑(x / z)

The scaling of a time unit

def TimeUnit.scale (r : ℝ) (x : TimeUnit) (hr : 0 < r := by norm_num) : TimeUnit

The scaling of a time unit by a positive real.

Equations

• TimeUnit.scale r x hr = { val := r * x.val, property := ⋯ }

@[simp]

theorem TimeUnit.scale_div_self (x : TimeUnit) (r : ℝ) (hr : 0 < r) : scale r x hr / x = ⟨r, ⋯⟩

@[simp]

theorem TimeUnit.scale_one (x : TimeUnit) : scale 1 x ⋯ = x

@[simp]

theorem TimeUnit.scale_div_scale (x1 x2 : TimeUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 x1 hr1 / scale r2 x2 hr2 = ⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2)

@[simp]

theorem TimeUnit.self_div_scale (x : TimeUnit) (r : ℝ) (hr : 0 < r) : x / scale r x hr = ⟨1 / r, ⋯⟩

@[simp]

theorem TimeUnit.scale_scale (x : TimeUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯

Specific choices of time units

To define a specific time units. We first define the notion of a second to correspond to the length unit with underlying value equal to 1. This is really down to a choice in the isomorphism between the set of metrics on the time manifold and the positive reals. From this choice of second, we can define other length units by scaling second.

def TimeUnit.seconds : TimeUnit

The definition of a time unit of seconds.

Equations

• TimeUnit.seconds = { val := 1, property := TimeUnit.instInhabited._proof_1 }

noncomputable def TimeUnit.femtoseconds : TimeUnit

The time unit of femtoseconds (10⁻¹⁵ of a second).

Equations

• TimeUnit.femtoseconds = TimeUnit.scale ((1 / 10) ^ 15) TimeUnit.seconds TimeUnit.femtoseconds._proof_2

noncomputable def TimeUnit.picoseconds : TimeUnit

The time unit of picoseconds (10⁻¹² of a second).

Equations

• TimeUnit.picoseconds = TimeUnit.scale ((1 / 10) ^ 12) TimeUnit.seconds TimeUnit.picoseconds._proof_1

noncomputable def TimeUnit.nanoseconds : TimeUnit

The time unit of nanoseconds (10⁻⁹ of a second).

Equations

• TimeUnit.nanoseconds = TimeUnit.scale ((1 / 10) ^ 9) TimeUnit.seconds TimeUnit.nanoseconds._proof_1

noncomputable def TimeUnit.microseconds : TimeUnit

The time unit of microseconds (10⁻⁶ of a second).

Equations

• TimeUnit.microseconds = TimeUnit.scale ((1 / 10) ^ 6) TimeUnit.seconds TimeUnit.microseconds._proof_1

noncomputable def TimeUnit.milliseconds : TimeUnit

The time unit of milliseconds (10⁻³ of a second).

Equations

• TimeUnit.milliseconds = TimeUnit.scale ((1 / 10) ^ 3) TimeUnit.seconds TimeUnit.milliseconds._proof_1

noncomputable def TimeUnit.centiseconds : TimeUnit

The time unit of centiseconds (10⁻² of a second).

Equations

• TimeUnit.centiseconds = TimeUnit.scale ((1 / 10) ^ 2) TimeUnit.seconds TimeUnit.centiseconds._proof_1

noncomputable def TimeUnit.deciseconds : TimeUnit

The time unit of deciseconds (10⁻¹ of a second).

Equations

• TimeUnit.deciseconds = TimeUnit.scale ((1 / 10) ^ 1) TimeUnit.seconds TimeUnit.deciseconds._proof_1

noncomputable def TimeUnit.minutes : TimeUnit

The time unit of minutes.

Equations

• TimeUnit.minutes = TimeUnit.scale 60 TimeUnit.seconds TimeUnit.minutes._proof_2

noncomputable def TimeUnit.hours : TimeUnit

The time unit of hours.

Equations

• TimeUnit.hours = TimeUnit.scale (60 * 60) TimeUnit.seconds TimeUnit.hours._proof_1

noncomputable def TimeUnit.days : TimeUnit

The time unit of 24 hour days.

Equations

• TimeUnit.days = TimeUnit.scale (24 * 60 * 60) TimeUnit.seconds TimeUnit.days._proof_2

noncomputable def TimeUnit.weeks : TimeUnit

The time unit of 7 day weeks.

Equations

• TimeUnit.weeks = TimeUnit.scale (7 * 24 * 60 * 60) TimeUnit.seconds TimeUnit.weeks._proof_2

Relations between time units

theorem TimeUnit.minutes_div_seconds : minutes / seconds = 60

theorem TimeUnit.hours_div_seconds : hours / seconds = 3600

theorem TimeUnit.days_div_seconds : days / seconds = 86400

theorem TimeUnit.weeks_div_seconds : weeks / seconds = 604800

theorem TimeUnit.days_div_minutes : days / minutes = 1440

theorem TimeUnit.weeks_div_minutes : weeks / minutes = 10080

theorem TimeUnit.days_div_hours : days / hours = 24

theorem TimeUnit.weeks_div_hours : weeks / hours = 168