Physlib.SpaceAndTime.Time.TimeUnit

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

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.

@[expose] public section

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

The underlying scale of the unit.

structure TimeUnit : Type where

  val : ℝ
  property : 0 < val

              @[simp]
lemma val_ne_zero (x : TimeUnit) : x.val ≠ 0 := byx:TimeUnit⊢ x.val ≠ 0
  exact Ne.symm (ne_of_lt x.property)All goals completed! 🐙lemma val_pos (x : TimeUnit) : 0 < x.val := x.propertyinstance : Inhabited TimeUnit where
  default := ⟨1, by⊢ 0 < 1 norm_numAll goals completed! 🐙⟩

Division of TimeUnit

              lemma div_eq_val (x y : TimeUnit) :
    x / y = (⟨x.val / y.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt y.val_pos)⟩ : ℝ≥0) := rfl

@[simp]
lemma div_ne_zero (x y : TimeUnit) : ¬ x / y = (0 : ℝ≥0) := byx:TimeUnity:TimeUnit⊢ ¬x / y = 0
  rw [div_eq_valx:TimeUnity:TimeUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0x:TimeUnity:TimeUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0]x:TimeUnity:TimeUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0
  refine coe_ne_zero.mp ?_x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ ≠ 0
  simp [toReal]All goals completed! 🐙@[simp]
lemma div_pos (x y : TimeUnit) : (0 : ℝ≥0) < x/ y := byx:TimeUnity:TimeUnit⊢ 0 < x / y
  apply lt_of_le_of_neax:TimeUnity:TimeUnit⊢ 0 ≤ x / yax:TimeUnity:TimeUnit⊢ 0 ≠ x / y
  ·ax:TimeUnity:TimeUnit⊢ 0 ≤ x / y exact zero_leAll goals completed! 🐙
  ·ax:TimeUnity:TimeUnit⊢ 0 ≠ x / y exact Ne.symm (div_ne_zero x y)All goals completed! 🐙@[simp]
lemma div_self (x : TimeUnit) :
    x / x = (1 : ℝ≥0) := byx:TimeUnit⊢ x / x = 1
  simp [div_eq_val, x.val_ne_zero]x:TimeUnit⊢ ⟨1, ⋯⟩ = 1
  rflAll goals completed! 🐙

lemma div_symm (x y : TimeUnit) :
    x / y = (y / x)⁻¹ := NNReal.eq <| byx:TimeUnity:TimeUnit⊢ ↑(x / y) = ↑(y / x)⁻¹
  rw [div_eq_val,x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(y / x)⁻¹x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(1 / ⟨y.val / x.val, ⋯⟩) inv_eq_one_div,x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(1 / (y / x))x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(1 / ⟨y.val / x.val, ⋯⟩) div_eq_valx:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(1 / ⟨y.val / x.val, ⋯⟩)x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(1 / ⟨y.val / x.val, ⋯⟩)]x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = ↑(1 / ⟨y.val / x.val, ⋯⟩)
  simp only [one_div, NNReal.coe_inv]x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = (↑⟨y.val / x.val, ⋯⟩)⁻¹
  rw [toReal,x:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = (↑⟨y.val / x.val, ⋯⟩)⁻¹All goals completed! 🐙 inv_divx:TimeUnity:TimeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ = x.val / y.valAll goals completed! 🐙]All goals completed! 🐙@[simp]
lemma div_mul_div_coe (x y z : TimeUnit) :
    (x / y : ℝ) * (y / z : ℝ) = x / z := byx:TimeUnity:TimeUnitz:TimeUnit⊢ ↑(x / y) * ↑(y / z) = ↑(x / z)
  simp [div_eq_val, toReal]x:TimeUnity:TimeUnitz:TimeUnit⊢ x.val / y.val * (y.val / z.val) = x.val / z.val
  field_simpAll goals completed! 🐙

The scaling of a time unit

The scaling of a time unit by a positive real.

def scale (r : ℝ) (x : TimeUnit) (hr : 0 < r := by norm_num) : TimeUnit :=
  ⟨r * x.val, mul_pos hr x.val_pos⟩

              @[simp]
lemma scale_div_self (x : TimeUnit) (r : ℝ) (hr : 0 < r) :
    scale r x hr / x = (⟨r, le_of_lt hr⟩ : ℝ≥0) := byx:TimeUnitr:ℝhr:0 < r⊢ scale r x hr / x = ⟨r, ⋯⟩
  simp [scale, div_eq_val]All goals completed! 🐙@[simp]
lemma scale_one (x : TimeUnit) : scale 1 x = x := byx:TimeUnit⊢ scale 1 x ⋯ = x
  simp [scale]All goals completed! 🐙

@[simp]
lemma scale_div_scale (x1 x2 : TimeUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) :
    scale r1 x1 hr1 / scale r2 x2 hr2 = (⟨r1, le_of_lt hr1⟩ / ⟨r2, le_of_lt hr2⟩) * (x1 / x2) := byx1:TimeUnitx2:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ scale r1 x1 hr1 / scale r2 x2 hr2 = ⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2)
  refine NNReal.eq ?_x1:TimeUnitx2:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑(scale r1 x1 hr1 / scale r2 x2 hr2) = ↑(⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2))
  simp [scale, div_eq_val]x1:TimeUnitx2:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩
  rw [toRealx1:TimeUnitx2:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩x1:TimeUnitx2:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩]x1:TimeUnitx2:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩
  field_simpAll goals completed! 🐙@[simp]
lemma self_div_scale (x : TimeUnit) (r : ℝ) (hr : 0 < r) :
    x / scale r x hr = (⟨1/r, _root_.div_nonneg (byx:TimeUnitr:ℝhr:0 < r⊢ 0 ≤ 1 simpAll goals completed! 🐙) (le_of_lt hr)⟩ : ℝ≥0) := byx:TimeUnitr:ℝhr:0 < r⊢ x / scale r x hr = ⟨1 / r, ⋯⟩
  simp [scale, div_eq_val]x:TimeUnitr:ℝhr:0 < r⊢ ⟨x.val / (r * x.val), ⋯⟩ = ⟨r⁻¹, ⋯⟩
  field_simpAll goals completed! 🐙@[simp]
lemma scale_scale (x : TimeUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) :
    scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x (mul_pos hr1 hr2) := byx:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯
  simp [scale]x:TimeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ r1 * (r2 * x.val) = r1 * r2 * x.val
  ringAll goals completed! 🐙

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.

The definition of a time unit of seconds.

def seconds : TimeUnit := ⟨1, by⊢ 0 < 1 norm_numAll goals completed! 🐙⟩

Relations between time units

              

lemma minutes_div_seconds : minutes / seconds = (60 : ℝ≥0) := NNReal.eq <| by⊢ ↑(minutes / seconds) = ↑60
  simp [minutes]⊢ ↑⟨60, ⋯⟩ = 60; rw [toReal⊢ ↑⟨60, ⋯⟩ = 60All goals completed! 🐙]All goals completed! 🐙

lemma hours_div_seconds : hours / seconds = (3600 : ℝ≥0) := NNReal.eq <| by⊢ ↑(hours / seconds) = ↑3600
  simp [hours]⊢ ↑⟨60 * 60, ⋯⟩ = 3600; rw [toReal⊢ ↑⟨60 * 60, ⋯⟩ = 3600⊢ ↑⟨60 * 60, ⋯⟩ = 3600]⊢ ↑⟨60 * 60, ⋯⟩ = 3600; norm_numAll goals completed! 🐙

lemma days_div_seconds : days / seconds = (86400 : ℝ≥0) := NNReal.eq <| by⊢ ↑(days / seconds) = ↑86400
  simp [days]⊢ ↑⟨24 * 60 * 60, ⋯⟩ = 86400; rw [toReal⊢ ↑⟨24 * 60 * 60, ⋯⟩ = 86400⊢ ↑⟨24 * 60 * 60, ⋯⟩ = 86400]⊢ ↑⟨24 * 60 * 60, ⋯⟩ = 86400; norm_numAll goals completed! 🐙

lemma weeks_div_seconds : weeks / seconds = (604800 : ℝ≥0) := NNReal.eq <| by⊢ ↑(weeks / seconds) = ↑604800
  simp [weeks]⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ = 604800; rw [toReal⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ = 604800⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ = 604800]⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ = 604800; norm_numAll goals completed! 🐙

lemma days_div_minutes : days / minutes = (1440 : ℝ≥0) := NNReal.eq <| by⊢ ↑(days / minutes) = ↑1440
  simp [days, minutes]⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 1440; rw [toReal⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 1440⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 1440]⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 1440; norm_numAll goals completed! 🐙

lemma weeks_div_minutes : weeks / minutes = (10080 : ℝ≥0) := NNReal.eq <| by⊢ ↑(weeks / minutes) = ↑10080
  simp [weeks, minutes]⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 10080; rw [toReal⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 10080⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 10080]⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60, ⋯⟩ = 10080; norm_numAll goals completed! 🐙

lemma days_div_hours : days / hours = (24 : ℝ≥0) := NNReal.eq <| by⊢ ↑(days / hours) = ↑24
  simp [hours, days]⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 24; rw [toReal⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 24⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 24]⊢ ↑⟨24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 24; norm_numAll goals completed! 🐙

lemma weeks_div_hours : weeks / hours = (168 : ℝ≥0) := NNReal.eq <| by⊢ ↑(weeks / hours) = ↑168
  simp [weeks, hours]⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 168; rw [toReal⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 168⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 168]⊢ ↑⟨7 * 24 * 60 * 60, ⋯⟩ / ↑⟨60 * 60, ⋯⟩ = 168; norm_numAll goals completed! 🐙