From 4d56ce067e93973c6061588398d55e5f61f3edf7 Mon Sep 17 00:00:00 2001 From: RaunakChhatwal Date: Wed, 23 Sep 2026 20:51:55 -0500 Subject: [PATCH] refactor(Time): add manifold structure and remove TimeTransMan --- Physlib.lean | 1 - Physlib/SpaceAndTime/Time/API-map.yaml | 17 +- Physlib/SpaceAndTime/Time/Basic.lean | 30 +- .../SpaceAndTime/Time/InnerProductSpace.lean | 16 - Physlib/SpaceAndTime/Time/TimeTransMan.lean | 448 ------------------ Physlib/SpaceAndTime/Time/TimeUnit.lean | 4 +- scripts/MetaPrograms/module_doc_no_lint.txt | 1 - 7 files changed, 32 insertions(+), 485 deletions(-) delete mode 100644 Physlib/SpaceAndTime/Time/TimeTransMan.lean diff --git a/Physlib.lean b/Physlib.lean index 87750fed4b..3df0c49e83 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -529,7 +529,6 @@ public import Physlib.SpaceAndTime.Time.Derivatives public import Physlib.SpaceAndTime.Time.InnerProductSpace public import Physlib.SpaceAndTime.Time.MatrixDerivatives public import Physlib.SpaceAndTime.Time.TimeMan -public import Physlib.SpaceAndTime.Time.TimeTransMan public import Physlib.SpaceAndTime.Time.TimeUnit public import Physlib.SpaceAndTime.TimeAndSpace.Basic public import Physlib.SpaceAndTime.TimeAndSpace.ConstantTimeDist diff --git a/Physlib/SpaceAndTime/Time/API-map.yaml b/Physlib/SpaceAndTime/Time/API-map.yaml index af14febaa2..b874330eb8 100644 --- a/Physlib/SpaceAndTime/Time/API-map.yaml +++ b/Physlib/SpaceAndTime/Time/API-map.yaml @@ -9,9 +9,8 @@ Overview: | time, and no instant is canonically zero. Choosing the implicit origin `Time.mk 0` gives the version of time most often used in non-relativistic physics, forming a 1d real inner-product space. The API also contains the time - derivative `∂ₜ` of functions on `Time`, and the related types `TimeMan`, - `TimeTransMan` and `TimeUnit`, versions of time with fewer choices made, - related to `Time` via a choice of units or origin. + derivative `∂ₜ` of functions on `Time`, the oriented time manifold `TimeMan`, + and the type `TimeUnit` of choices of time unit. ParentAPIs: - "Space (Physlib/SpaceAndTime/Space)" @@ -65,10 +64,6 @@ Requirements: done: true location: "Physlib/SpaceAndTime/Time/TimeUnit.lean (TimeUnit, HDiv TimeUnit TimeUnit ℝ≥0, scale, seconds, hours_div_seconds)" - - description: "The API contains the time manifold `TimeTransMan` with a transitive action of `ℝ`, an orientation, unit-dependent differences and translations (`diff`, `addTime`, `neg`), and the homeomorphism `toTime` to `Time` given a choice of origin and unit." - done: true - location: "Physlib/SpaceAndTime/Time/TimeTransMan.lean (TimeTransMan, AddAction ℝ TimeTransMan, diff, addTime, neg, toTime)" - - description: "The API shall contain an action of the translation group on `Time`." done: false location: N/A @@ -80,11 +75,3 @@ Requirements: - description: "The API shall contain derivatives of distributions from `Time` to manifolds." done: false location: N/A - - - description: "The API shall show that the homeomorphism `toTime` from `TimeTransMan` to `Time` is a diffeomorphism." - done: false - location: N/A - - - description: "The API shall show that translationally-invariant metrics on `TimeTransMan` are in one-to-one correspondence with the positive reals (choices of `TimeUnit`)." - done: false - location: N/A diff --git a/Physlib/SpaceAndTime/Time/Basic.lean b/Physlib/SpaceAndTime/Time/Basic.lean index d8b24f01af..2910958371 100644 --- a/Physlib/SpaceAndTime/Time/Basic.lean +++ b/Physlib/SpaceAndTime/Time/Basic.lean @@ -5,7 +5,9 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.Basic.Real.Basic +public import Mathlib.Analysis.Normed.Group.AddTorsor +public import Mathlib.Analysis.Normed.Group.Real +public import Mathlib.Geometry.Manifold.IsManifold.Basic public import Mathlib.LinearAlgebra.AffineSpace.Defs /-! # Time @@ -18,9 +20,12 @@ The field `Time.val` is an implementation coordinate, not a frame-relative time coordinate. A reference frame chooses its own time origin. Import `Physlib.SpaceAndTime.Time.InnerProductSpace` to use the inner product space structure with the implicit origin `Time.mk 0`, including addition of instants, norms, and derivatives. + -/ -@[expose] public section +@[expose] public noncomputable section + +open scoped Manifold ContDiff /-! # A. The `Time` type @@ -60,4 +65,25 @@ instance : AddTorsor ℝ Time where vsub_vadd' t₁ t₂ := by ext; simp vadd_vsub' dt t := by simp +/-! +# C. The metric and manifold structure +-/ + +instance : MetricSpace Time := metricSpaceOfNormedAddCommGroupOfAddTorsor ℝ Time + +instance : NormedAddTorsor ℝ Time where + dist_eq_norm' _ _ := rfl + +instance : ChartedSpace ℝ Time := + let chartAt t := (Homeomorph.vaddConst t).symm.toOpenPartialHomeomorph + { chartAt, + atlas := Set.range chartAt, + mem_chart_source := Set.mem_univ, + chart_mem_atlas := by simp } + +instance : IsManifold 𝓘(ℝ, ℝ) ω Time := by + apply isManifold_of_contDiffOn + rintro _ _ ⟨_, rfl⟩ ⟨_, rfl⟩ + exact contDiff_id.add contDiff_const |>.sub contDiff_const |>.contDiffOn + end Time diff --git a/Physlib/SpaceAndTime/Time/InnerProductSpace.lean b/Physlib/SpaceAndTime/Time/InnerProductSpace.lean index 771a7c466e..ddbcb62a2c 100644 --- a/Physlib/SpaceAndTime/Time/InnerProductSpace.lean +++ b/Physlib/SpaceAndTime/Time/InnerProductSpace.lean @@ -32,10 +32,6 @@ the angular frequency `ω` are consistent. With this choice, `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 - `toRealCLE` : The continuous linear equivalence from `Time` to `ℝ`. @@ -254,9 +250,6 @@ instance : Norm Time where lemma norm_eq_val (t : Time) : ‖t‖ = ‖t.val‖ := rfl -instance : Dist Time where - dist t1 t2 := ‖t1 - t2‖ - lemma dist_eq_val (t1 t2 : Time) : dist t1 t2 = ‖t1.val - t2.val‖ := rfl @@ -264,21 +257,12 @@ lemma dist_eq_real_dist (t1 t2 : Time) : dist t1 t2 = dist t1.val t2.val := by rfl instance : SeminormedAddCommGroup Time where - dist_self t := by simp [dist_eq_real_dist] - dist_comm t1 t2 := by simp [dist_eq_real_dist, dist_comm] - dist_triangle := by simp [dist_eq_real_dist, dist_triangle] dist_eq t1 t2 := by simp [dist_eq_val, norm_eq_val] rw [abs_eq_iff_mul_self_eq] ring instance : NormedAddCommGroup Time where - eq_of_dist_eq_zero := by - intro a b h - simp [dist, norm] at h - ext - rw [sub_eq_zero] at h - exact h dist_eq t1 t2 := by simp [dist_eq_val, norm_eq_val] rw [abs_eq_iff_mul_self_eq] diff --git a/Physlib/SpaceAndTime/Time/TimeTransMan.lean b/Physlib/SpaceAndTime/Time/TimeTransMan.lean deleted file mode 100644 index ec80c5dbb5..0000000000 --- a/Physlib/SpaceAndTime/Time/TimeTransMan.lean +++ /dev/null @@ -1,448 +0,0 @@ -/- -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.Geometry.Manifold.Diffeomorph -public import Physlib.Meta.TODO.Basic -public import Physlib.SpaceAndTime.Time.InnerProductSpace -public import Physlib.SpaceAndTime.Time.TimeUnit -/-! - -# The time manifold with a transitive action of `ℝ` - -In this module we define the type `TimeTransMan`. This type physically corresponds to -the manifold of time (diffeomorphic to `ℝ`) with the following additional structure: -1. a transitive action of `ℝ`, -2. a choice of orientation. - -The manifold `TimeTransMan` is not equipped with a translationally-invariant metric. -Such metrics are in one-to-one correspondence (to be shown) with positive reals, and -as such we define the type `TimeUnit` (equivalent to the positive reals) to -represent the choice of metric on `TimeTransMan`. This is defined in a different module. - -From the point of view of physics, this choice of metric corresponds to a choice of units, -hence the name, and we will use the phrase 'units of time' interchangeably 'choice of metric'. - -Given a `x : TimeUnit`, and the structure above, we can define the following -operations on `TimeTransMan`: -- `diff x t1 t2`, for `t1 t2 : TimeTransMan` gives the signed difference between two points in - time in the units `x`. -- `addTime x r t`, for `r : ℝ` and `t : TimeTransMan`, gives the point in `TimeTransMan` - that separated from `t`, by `r` in the unit `x`. For example, if `x` is the unit of seconds, - then `addTime x 1 t` gives the point in `TimeTransMan` that is one second after `t`. -- `neg zero t`, for a given `zero : TimeTransMan`, gives the point in `TimeTransMan` - that is the same distance away from `zero` as `t` but in the opposite direction. - This is defined using a choice of units, but is independent of the choice. - -Recall that the type `Time` corresponds to the manifold of time with a -given (but arbitrary) choice of units and origin (and therefore has a structure -of a module over `ℝ`). Here we define the homeomorphism: -- `toTime zero x` from `TimeTransMan` to `Time` where - `zero : TimeTransMan` is the choice of origin and `x : TimeUnit` is the choice of units. -This map is a diffeomorphism (to be shown). - --/ - -@[expose] public section - -TODO "Remove `TimeTransMan` in favor of affine `Time`." - -/-- The type `TimeTransMan` represents the time manifold with an orientation and - a transitive action of the reals. -/ -structure TimeTransMan where - /-- The choice of a map from `TimeTransMan` to `ℝ`. -/ - val : ℝ - -namespace TimeTransMan - -@[ext] -lemma ext_of {t1 t2 : TimeTransMan} (h : t1.val = t2.val) : - t1 = t2 := by - cases t1; cases t2; simp_all - -/-! - -## The topology on TimeTransMan. - -The topology on `TimeTransMan` is induced from the topology on `ℝ`, via the choice -of map `TimeTransMan.val`. - --/ - -/-- The instance of a topological space on `TimeTransMan` induced by the map `TimeTransMan.val`. -/ -instance : TopologicalSpace TimeTransMan := TopologicalSpace.induced TimeTransMan.val - PseudoMetricSpace.toUniformSpace.toTopologicalSpace - -lemma val_surjective : Function.Surjective TimeTransMan.val := by - intro t - use { val := t } - -@[simp] -lemma val_range : Set.range val = Set.univ := by - refine Set.range_eq_univ.mpr val_surjective - -lemma val_inducing : Topology.IsInducing TimeTransMan.val where - eq_induced := rfl - -lemma val_injective : Function.Injective TimeTransMan.val := by - intro t1 t2 h - cases t1 - cases t2 - simp_all - -lemma val_isOpenEmbedding : Topology.IsOpenEmbedding TimeTransMan.val where - eq_induced := rfl - isOpen_range := by - simp - injective := val_injective - -lemma isOpen_iff {s : Set TimeTransMan} : - IsOpen s ↔ IsOpen (TimeTransMan.val '' s) := - Topology.IsOpenEmbedding.isOpen_iff_image_isOpen val_isOpenEmbedding - -/-- The choice of map `Time.val` from `TimeTransMan` to `ℝ` as a homeomorphism. -/ -def valHomeomorphism : TimeTransMan ≃ₜ ℝ where - toFun := TimeTransMan.val - invFun := fun t => { val := t } - left_inv := by - intro t - cases t - rfl - right_inv := by - intro t - rfl - continuous_toFun := by fun_prop - continuous_invFun := by - refine { isOpen_preimage := ?_ } - intro s hs - rw [isOpen_iff] at hs - rw [← Set.image_eq_preimage_of_inverse] - · exact hs - · intro t - rfl - · intro x - simp - -/-! - -## The manifold structure on TimeTransMan - --/ - -/-- The structure of a charted space on `TimeTransMan` -/ -instance : ChartedSpace ℝ TimeTransMan where - atlas := { valHomeomorphism.toOpenPartialHomeomorph } - chartAt _ := valHomeomorphism.toOpenPartialHomeomorph - mem_chart_source := by - simp - chart_mem_atlas := by - intro x - simp - -open Manifold ContDiff - -/-- The structure of a manifold on `TimeTransMan` induced by the choice of map `Time.val`. -/ -instance : IsManifold 𝓘(ℝ, ℝ) ω TimeTransMan where - compatible := by - intro e1 e2 h1 h2 - simp [atlas, ChartedSpace.atlas] at h1 h2 - subst h1 h2 - exact symm_trans_mem_contDiffGroupoid valHomeomorphism.toOpenPartialHomeomorph - -lemma val_contDiff : ContMDiff 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ω TimeTransMan.val := by - refine contMDiffOn_univ.mp ?_ - exact contMDiffOn_chart (x := (⟨0⟩ : TimeTransMan)) - -/-- The choice of map `Time.val` from `TimeTransMan` to `ℝ` as a diffeomorphism. -/ -noncomputable def valDiffeomorphism : TimeTransMan ≃ₘ^ω⟮𝓘(ℝ, ℝ), 𝓘(ℝ, ℝ)⟯ ℝ where - toEquiv := valHomeomorphism.toEquiv - contMDiff_toFun := val_contDiff - contMDiff_invFun := by - refine contMDiffOn_univ.mp ?_ - exact contMDiffOn_chart_symm (x := (⟨0⟩ : TimeTransMan)) - -/-! - -## The transitive group action on TimeTransMan - --/ - -instance : VAdd ℝ TimeTransMan where - vadd p t := { val := p + t.val } - -@[simp] -lemma vadd_val (p : ℝ) (t : TimeTransMan) : - (p +ᵥ t).val = p + t.val := rfl - -instance : AddAction ℝ TimeTransMan where - zero_vadd t := by - cases t - ext - simp - add_vadd p1 p2 t := by - ext - simp only [vadd_val] - ring - -/-! - -## A choice of orientation on TimeTransMan - --/ - -instance : LE TimeTransMan where - le x y := x.val ≤ y.val - -lemma le_def (t1 t2 : TimeTransMan) : - t1 ≤ t2 ↔ t1.val ≤ t2.val := Iff.rfl - -instance : Nonempty TimeTransMan := Nonempty.intro ⟨0⟩ - -/-! - -## Functions based on a choice of unit - --/ - -open TimeUnit - -/-- The distance between two points in `TimeTransMan` in the units of `x : TimeUnit`. -/ -noncomputable def dist (x : TimeUnit) (t1 t2 : TimeTransMan) : ℝ := - 1/(PositiveRealUnitCore.val x) * ‖t2.val - t1.val‖ - -/-! - -### Signed difference - --/ - -/-- The signed difference between two points in on the manifold `TimeTransMan` - in the units of `x : TimeUnit`. -/ -noncomputable def diff (x : TimeUnit) (t2 t1 : TimeTransMan) : ℝ := - if t1 ≤ t2 then dist x t1 t2 else - dist x t1 t2 - -lemma diff_eq_val (x : TimeUnit) (t1 t2 : TimeTransMan) : - diff x t1 t2 = 1/(PositiveRealUnitCore.val x) * (t1.val - t2.val) := by - by_cases h : t2 ≤ t1 - · simp [diff, dist, h] - simpa [le_def] using h - · simp [diff, dist, h] - simp [le_def] at h - rw [abs_of_neg] - have hx : (PositiveRealUnitCore.val x) ≠ 0 := (PositiveRealUnitCore.val_ne_zero x) - field_simp - linarith - -@[simp] -lemma diff_self (x : TimeUnit) (t : TimeTransMan) : - diff x t t = 0 := by - simp [diff_eq_val] - -lemma diff_fst_injective (x : TimeUnit) (t : TimeTransMan) : Function.Injective (diff x · t) := by - intro t1 t2 h - simp [diff] at h - by_cases h1 : t ≤ t1 - <;> by_cases h2 : t ≤ t2 - · simp_all [dist, le_def] - rw [abs_of_nonneg (by linarith), abs_of_nonneg (by linarith)] at h - simp at h - ext - exact h - · simp_all [dist, le_def] - rw [abs_of_nonneg (by linarith), abs_of_neg (by linarith)] at h - simp [← mul_neg] at h - ext - exact h - · simp_all [dist, le_def] - rw [abs_of_neg (by linarith), abs_of_nonneg (by linarith)] at h - simp [← mul_neg] at h - ext - exact h - · simp_all [dist, le_def] - rw [abs_of_neg (by linarith), abs_of_neg (by linarith)] at h - simp at h - ext - exact h - -lemma diff_fst_surjective (x : TimeUnit) (t : TimeTransMan) : - Function.Surjective (diff x · t) := by - intro r - simp [diff, dist] - use (PositiveRealUnitCore.val x) * r +ᵥ t - simp [abs_mul] - rw [abs_of_nonneg (le_of_lt (PositiveRealUnitCore.pos x))] - simp only [ne_eq, PositiveRealUnitCore.val_ne_zero, not_false_eq_true, inv_mul_cancel_left₀] - by_cases h : 0 ≤ r - · rw [ite_eq_left] - exact abs_of_nonneg h - simp [le_def] - apply mul_nonneg (le_of_lt (PositiveRealUnitCore.pos x)) h - · rw [ite_eq_right] - rw [abs_of_neg (by simpa using h)] - simp only [neg_neg] - simp [le_def] - refine mul_neg_of_pos_of_neg (PositiveRealUnitCore.pos x) (by simpa using h) - -lemma diff_fst_bijective (x : TimeUnit) (t : TimeTransMan) : - Function.Bijective (diff x · t) := - ⟨diff_fst_injective x t, diff_fst_surjective x t⟩ - -/-! - -### Adding time - --/ - -/-- Given a time unit `x : TimeUnit`, `addTime x r t`, for a real `ℝ` and `t : TimeTransMan`, - is the point in `TimeTransMan` separated from `t` by a difference of `r` in the units `x`. - For example, if `x` corresponds to seconds `addTime x 1 t` is the time 1 second more then `t`. -/ -noncomputable def addTime (x : TimeUnit) (r : ℝ) (t : TimeTransMan) : TimeTransMan := - Function.invFun (diff x · t) r - -lemma addTime_eq_val (x : TimeUnit) (r : ℝ) (t : TimeTransMan) : - (addTime x r t) = ⟨(PositiveRealUnitCore.val x) * r + t.val⟩ := by - apply diff_fst_injective x t - change (diff x · t) (Function.invFun ((diff x · t)) r) = _ - rw [Function.rightInverse_invFun (diff_fst_surjective x t)] - simp [diff_eq_val] - -lemma addTime_val (x : TimeUnit) (r : ℝ) (t : TimeTransMan) : - (addTime x r t).val = (PositiveRealUnitCore.val x) * r + t.val := by - rw [addTime_eq_val] - -/-! - -## Negation of time around a zero - --/ - -/-- Given a `zero` and an `x : TimeUnit`, `negMetric zero x t` is the time the same distance - away from `zero` as `t` in units `x` but in the opposite direction. - This does actually depend on `x`, as a result see `neg` and `neg_eq_negMetric`. -/ -noncomputable def negMetric (zero : TimeTransMan) (x : TimeUnit) - (t : TimeTransMan) : TimeTransMan := - addTime x (diff x zero t) zero - -/-- Given a `zero`, `neg zero t` is the time the same distance - away from `zero` as `t` in any units but in the opposite direction. -/ -noncomputable def neg (zero : TimeTransMan) (t : TimeTransMan) : TimeTransMan := - negMetric zero default t - -lemma neg_eq_negMetric (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : - neg zero t = negMetric zero x t := by - simp [neg, negMetric] - ext - simp [addTime_val, diff_eq_val] - -/-! - -### The map from TimeTransMan to Time - --/ -/-- With a choice of zero `zero : TimeTransMan` and a choice of units `x : TimeUnit`, - `toTime` is the homeomorphism between the type `TimeTransMan` and `Time`. -/ -noncomputable def toTime (zero : TimeTransMan) (x : TimeUnit) : TimeTransMan ≃ₜ Time where - toFun := fun t => ⟨diff x t zero⟩ - invFun := fun r => addTime x r zero - left_inv t := by - ext - simp [addTime_val, diff_eq_val] - right_inv r := by - ext - simp [addTime_val, diff_eq_val] - continuous_invFun := by - rw [← Homeomorph.comp_continuous_iff valHomeomorphism] - have h1 : (⇑valHomeomorphism ∘ (fun r : Time => addTime x r.val zero)) = fun r => - ((PositiveRealUnitCore.val x) * r.val + zero.val) := by - ext - simp [valHomeomorphism, addTime_val] - rw [h1] - · apply Continuous.add - · apply Continuous.fun_mul - · fun_prop - · apply Differentiable.continuous (𝕜 := ℝ) - fun_prop - · fun_prop - - continuous_toFun := by - rw [← Homeomorph.comp_continuous_iff Time.toRealCLE.toHomeomorph] - have h1 : (⇑Time.toRealCLE.toHomeomorph ∘ (fun t => ⟨diff x t zero⟩)) = fun t => - (1/(PositiveRealUnitCore.val x)) * (t.val - zero.val) := by - ext - simp [Time.toRealCLE, diff_eq_val] - rw [h1] - fun_prop - -@[simp] -lemma toTime_zero (zero : TimeTransMan) (x : TimeUnit) : - toTime zero x zero = 0 := by - ext - simp [toTime, diff_eq_val] - -@[simp] -lemma toTime_symm_zero_add (zero : TimeTransMan) (x : TimeUnit) : - (toTime zero x).symm 0 = zero := by - ext - simp [toTime, addTime_val, diff_eq_val] - -lemma toTime_val (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : - (toTime zero x t).val = diff x t zero := by rfl - -lemma toTime_symm_val (zero : TimeTransMan) (x : TimeUnit) (r : Time) : - (toTime zero x).symm r = addTime x r zero := by - ext - simp [toTime, addTime_val, diff_eq_val] - -@[simp] -lemma toTime_addTime (zero : TimeTransMan) (x : TimeUnit) (r : ℝ) (τ : TimeTransMan) : - toTime zero x (addTime x r τ) = ⟨r⟩ + toTime zero x τ:= by - ext - simp [toTime_val, diff_eq_val, addTime_val] - field_simp - ring - -lemma toTime_symm_add (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) : - (toTime zero x).symm (t1 + t2) = addTime x (diff x ((toTime zero x).symm t1) zero) - ((toTime zero x).symm t2) := by - ext - simp [addTime_val, diff_eq_val, toTime_symm_val] - ring - -lemma toTime_symm_add' (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) : - (toTime zero x).symm (t1 + t2) = addTime x (diff x ((toTime zero x).symm t2) zero) - ((toTime zero x).symm t1) := by - ext - simp [addTime_val, diff_eq_val, toTime_symm_val] - ring - -lemma diff_eq_toTime_sub (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : TimeTransMan) : - diff x t2 t1 = toTime zero x t2 - toTime zero x t1 := by - simp [toTime_val, diff_eq_val] - field_simp - ring - -lemma toTime_neg (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : - (toTime zero x) (neg zero t) = - toTime zero x t := by - rw [neg_eq_negMetric zero x] - ext - simp only [negMetric, diff_eq_val, one_div, toTime_addTime, toTime_zero, - add_zero, Time.neg_val, toTime_val] - ring - -lemma toTime_symm_neg (zero : TimeTransMan) (x : TimeUnit) (t : Time) : - (toTime zero x).symm (- t) = neg zero ((toTime zero x).symm t) := by - ext - simp [toTime_symm_val, addTime_val, diff_eq_val, neg, negMetric] - -lemma toTime_symm_sub (zero : TimeTransMan) (x : TimeUnit) - (t1 t2 : Time) : (toTime zero x).symm (t1 - t2) = - addTime x (diff x zero ((toTime zero x).symm t2)) - ((toTime zero x).symm t1) := by - ext - simp [addTime_val, diff_eq_val, toTime_symm_val] - ring - -end TimeTransMan diff --git a/Physlib/SpaceAndTime/Time/TimeUnit.lean b/Physlib/SpaceAndTime/Time/TimeUnit.lean index 952bd520c0..be648cd80e 100644 --- a/Physlib/SpaceAndTime/Time/TimeUnit.lean +++ b/Physlib/SpaceAndTime/Time/TimeUnit.lean @@ -12,7 +12,7 @@ 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 +metric on the time manifold. 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. @@ -32,7 +32,7 @@ existence of the time unit of seconds, and construct all other time units from t open NNReal -/-- The choices of translationally-invariant metrics on the manifold `TimeTransMan`. +/-- The choices of translationally-invariant metrics on the time manifold. Such a choice corresponds to a choice of units for time. -/ structure TimeUnit : Type where /-- The underlying scale of the unit. -/ diff --git a/scripts/MetaPrograms/module_doc_no_lint.txt b/scripts/MetaPrograms/module_doc_no_lint.txt index a56c78b8be..297f27a0a7 100644 --- a/scripts/MetaPrograms/module_doc_no_lint.txt +++ b/scripts/MetaPrograms/module_doc_no_lint.txt @@ -287,7 +287,6 @@ Physlib/SpaceAndTime/Space/LengthUnit.lean Physlib/SpaceAndTime/Space/Translations.lean Physlib/SpaceAndTime/SpaceTime/TimeSlice.lean Physlib/SpaceAndTime/Time/TimeMan.lean -Physlib/SpaceAndTime/Time/TimeTransMan.lean Physlib/SpaceAndTime/Time/TimeUnit.lean Physlib/StatisticalMechanics/BoltzmannConstant.lean Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean