Time Translation Operators

This file defines time translation operators on spacetime, Schwartz functions, and tempered distributions. These are fundamental for the OS4 (Ergodicity) axiom.

Main Definitions

• timeIndex: The time coordinate index in spacetime (index 0)
• getTime: Extract the time component from a spacetime point
• timeShift: Time translation on spacetime points
• timeTranslationSchwartz: Time translation on real Schwartz functions
• timeTranslationSchwartzℂ: Time translation on complex Schwartz functions
• timeTranslationDistribution: Time translation on tempered distributions

Notation

We work in spacetime ℝ × ℝ³ where:

• The first coordinate is time (index 0)
• The remaining 3 coordinates are space (indices 1,2,3)
• This matches STDimension = 4 from Basic.lean

Main Theorems

• schwartz_timeTranslation_lipschitz_seminorm: Lipschitz bound for time translation on Schwartz seminorms, proved using Mean Value Theorem, chain rule, and continuousMultilinearCurryLeftEquiv isometry.

This is used to prove continuous_timeTranslationSchwartz, which establishes that time translation acts continuously on Schwartz space (a standard textbook fact from Reed-Simon V.3 and Hörmander Ch. 7).

Time Translation on Spacetime Points

Definition 0.2 from the PDF: For any s ∈ ℝ, define the time translation operator. The time coordinate is index 0 in our 4D spacetime.

def TimeTranslation.timeIndex : Fin STDimension

The time coordinate index in spacetime (index 0).

Equations

• TimeTranslation.timeIndex = ⟨0, TimeTranslation.timeIndex._proof_1⟩

def TimeTranslation.getTime (u : SpaceTime) : ℝ

Extract the time component from a spacetime point.

Equations

• TimeTranslation.getTime u = u.ofLp TimeTranslation.timeIndex

def TimeTranslation.timeShift (s : ℝ) (u : SpaceTime) : SpaceTime

Time translation on spacetime points: shifts the time coordinate by s. (timeShift s u)_0 = u_0 + s, and (timeShift s u)_i = u_i for i ≠ 0.

Equations

• TimeTranslation.timeShift s u = WithLp.toLp 2 fun (i : Fin STDimension) => if ↑i = 0 then u.ofLp i + s else u.ofLp i

@[simp]

theorem TimeTranslation.timeShift_time (s : ℝ) (u : SpaceTime) : getTime (timeShift s u) = getTime u + s

@[simp]

theorem TimeTranslation.timeShift_spatial (s : ℝ) (u : SpaceTime) (i : Fin STDimension) (hi : ↑i ≠ 0) : (timeShift s u).ofLp i = u.ofLp i

theorem TimeTranslation.timeShift_add (s t : ℝ) (u : SpaceTime) : timeShift (s + t) u = timeShift s (timeShift t u)

Time shift is a group action: T_{s+t} = T_s ∘ T_t

@[simp]

theorem TimeTranslation.timeShift_zero (u : SpaceTime) : timeShift 0 u = u

Time shift by zero is identity

theorem TimeTranslation.timeShift_comm (s t : ℝ) (u : SpaceTime) : timeShift s (timeShift t u) = timeShift t (timeShift s u)

Time shifts commute: T_s ∘ T_t = T_t ∘ T_s

theorem TimeTranslation.timeShift_contDiff (s : ℝ) : ContDiff ℝ (↑⊤) (timeShift s)

Time shift is smooth as a map SpaceTime → SpaceTime. This is because it's an affine map (linear + constant).

theorem TimeTranslation.timeShift_dist (s : ℝ) (u v : SpaceTime) : dist (timeShift s u) (timeShift s v) = dist u v

Time shift preserves the Euclidean distance (it's an isometry)

theorem TimeTranslation.timeShift_isometry (s : ℝ) : Isometry (timeShift s)

Time shift is an isometry

theorem TimeTranslation.timeShift_antilipschitz (s : ℝ) : AntilipschitzWith 1 (timeShift s)

Time shift is antilipschitz (follows from being an isometry).

def TimeTranslation.timeShiftConst (s : ℝ) : SpaceTime

The constant vector used to express timeShift as id + const.

Equations

• TimeTranslation.timeShiftConst s = WithLp.toLp 2 fun (i : Fin STDimension) => if ↑i = 0 then s else 0

theorem TimeTranslation.timeShift_eq_add_const (s : ℝ) (u : SpaceTime) : timeShift s u = u + timeShiftConst s

timeShift s equals addition of a constant.

theorem TimeTranslation.timeShift_hasTemperateGrowth (s : ℝ) : Function.HasTemperateGrowth (timeShift s)

Time shift has temperate growth (key for Schwartz composition). This follows because timeShift is an affine map (id + constant).

Time Translation on Schwartz Functions

Definition 0.2 from the PDF: For any s ∈ ℝ, define the time translation operator on Schwartz functions T_s : S(ℝ × ℝ³) → S(ℝ × ℝ³) by

(T_s f)(t, x) := f(t + s, x)

We need to show that T_s preserves the Schwartz space. Since timeShift s is an affine isometry, composition with it preserves Schwartz decay.

Note: Time translation is NOT a linear map on spacetime, but composition f ↦ f ∘ (timeShift s) is a linear map on the Schwartz space.

noncomputable def TimeTranslation.timeTranslationSchwartzCLM (s : ℝ) : TestFunction →L[ℝ] TestFunction

Time translation as a continuous linear map on real-valued Schwartz functions. Uses mathlib's compCLMOfAntilipschitz which requires:

1. The composition function has temperate growth
2. The composition function is antilipschitz

Equations

• TimeTranslation.timeTranslationSchwartzCLM s = SchwartzMap.compCLMOfAntilipschitz ℝ ⋯ ⋯

noncomputable def TimeTranslation.timeTranslationSchwartz (s : ℝ) (f : TestFunction) : TestFunction

Time translation on real-valued Schwartz functions. (T_s f)(u) = f(timeShift s u) = f(t + s, x)

Note: The PDF defines (T_s f)(t,x) = f(t+s, x). Since timeShift s shifts the time coordinate by +s, we have (timeShift s)(t,x) = (t+s, x), so f ∘ (timeShift s) gives (T_s f).

This is well-defined because:

1. timeShift s has temperate growth (affine map)
2. timeShift s is antilipschitz (isometry)

Equations

• TimeTranslation.timeTranslationSchwartz s f = (TimeTranslation.timeTranslationSchwartzCLM s) f

noncomputable def TimeTranslation.timeTranslationSchwartzℂCLM (s : ℝ) : TestFunctionℂ →L[ℂ] TestFunctionℂ

Time translation as a continuous linear map on complex-valued Schwartz functions.

Equations

• TimeTranslation.timeTranslationSchwartzℂCLM s = SchwartzMap.compCLMOfAntilipschitz ℂ ⋯ ⋯

noncomputable def TimeTranslation.timeTranslationSchwartzℂ (s : ℝ) (f : TestFunctionℂ) : TestFunctionℂ

Time translation on complex-valued Schwartz functions.

Equations

• TimeTranslation.timeTranslationSchwartzℂ s f = (TimeTranslation.timeTranslationSchwartzℂCLM s) f

@[simp]

theorem TimeTranslation.timeTranslationSchwartz_apply (s : ℝ) (f : TestFunction) (u : SpaceTime) : (timeTranslationSchwartz s f) u = f (timeShift s u)

Time translation evaluated at a point.

@[simp]

theorem TimeTranslation.timeTranslationSchwartzℂ_apply (s : ℝ) (f : TestFunctionℂ) (u : SpaceTime) : (timeTranslationSchwartzℂ s f) u = f (timeShift s u)

Time translation on complex functions evaluated at a point.

theorem TimeTranslation.timeTranslationSchwartz_add (s t : ℝ) (f : TestFunction) : timeTranslationSchwartz (s + t) f = timeTranslationSchwartz s (timeTranslationSchwartz t f)

Time translation is a group homomorphism: T_{s+t} = T_s ∘ T_t

theorem TimeTranslation.timeTranslationSchwartzℂ_add (s t : ℝ) (f : TestFunctionℂ) : timeTranslationSchwartzℂ (s + t) f = timeTranslationSchwartzℂ s (timeTranslationSchwartzℂ t f)

Time translation on complex functions: T_{s+t} = T_s ∘ T_t

@[simp]

theorem TimeTranslation.timeTranslationSchwartz_zero (f : TestFunction) : timeTranslationSchwartz 0 f = f

Time translation by zero is identity

@[simp]

theorem TimeTranslation.timeTranslationSchwartzℂ_zero (f : TestFunctionℂ) : timeTranslationSchwartzℂ 0 f = f

Time translation by zero is identity (complex)

theorem TimeTranslation.timeTranslationSchwartz_add_fun (s : ℝ) (f g : TestFunction) : timeTranslationSchwartz s (f + g) = timeTranslationSchwartz s f + timeTranslationSchwartz s g

Time translation preserves addition of Schwartz functions

theorem TimeTranslation.timeTranslationSchwartz_smul (s c : ℝ) (f : TestFunction) : timeTranslationSchwartz s (c • f) = c • timeTranslationSchwartz s f

Time translation preserves scalar multiplication of Schwartz functions

Fundamental Theorem of Calculus for Time Translation

The following lemmas establish the pointwise FTC formula: (T_h f)(x) - f(x) = ∫₀ʰ (∂_t f)(T_s x) ds

This provides the mathematical foundation for the Lipschitz bound theorem below.

noncomputable def TimeTranslation.unitTimeDir : SpaceTime

The unit time direction vector in SpaceTime.

Equations

• TimeTranslation.unitTimeDir = EuclideanSpace.single TimeTranslation.timeIndex 1

theorem TimeTranslation.continuous_timeShift_param (x : SpaceTime) : Continuous fun (s : ℝ) => timeShift s x

timeShift is continuous in the time parameter s

theorem TimeTranslation.peetre_weight_bound (x y : SpaceTime) (k : ℕ) : (1 + ‖x‖) ^ k ≤ (1 + ‖x + y‖) ^ k * (1 + ‖y‖) ^ k

Peetre's inequality for polynomial weights in SpaceTime. (1 + ‖x‖)^k ≤ (1 + ‖x + y‖)^k * (1 + ‖y‖)^k

This handles weight shifting when translating between seminorms at different points.

theorem TimeTranslation.iteratedFDeriv_timeTranslationSchwartz (n : ℕ) (h : ℝ) (f : TestFunction) (x : SpaceTime) : iteratedFDeriv ℝ n (⇑(timeTranslationSchwartz h f)) x = iteratedFDeriv ℝ n (⇑f) (x + h • unitTimeDir)

The iterated derivative commutes with time translation. D^n(T_h f)(x) = D^n f(x + h·e₀)

theorem TimeTranslation.schwartz_timeTranslation_lipschitz_seminorm (k n : ℕ) (f : TestFunction) (h : ℝ) : (SchwartzMap.seminorm ℝ k n) (timeTranslationSchwartz h f - f) ≤ |h| * (1 + |h|) ^ k * 2 ^ k * ((SchwartzMap.seminorm ℝ k (n + 1)) f + (SchwartzMap.seminorm ℝ 0 (n + 1)) f + 1)

Locally Uniform Lipschitz Bound for Time Translation.

For any Schwartz function f and time shift h, the seminorm of T_h f - f is bounded by |h| times (1+|h|)^k · 2^k times a sum of the (n+1)-th seminorms:

‖T_h f - f‖{k,n} ≤ |h| · (1 + |h|)^k · 2^k · (‖f‖{k,n+1} + ‖f‖_{0,n+1} + 1)

The 2^k factor comes from Peetre's inequality: (1+‖w‖)^k ≤ 2^k · max(1, ‖w‖^k). This bound suffices for proving continuity at h=0, since (1+|h|)^k · 2^k ≤ 4^k for |h| ≤ 1.

Proof Outline:

1. Use seminorm_le_bound: suffices to show pointwise bound for all x
2. Use iteratedFDeriv_comp_add_right: D^n(T_h f)(x) = D^n f(x + h·e₀)
3. Apply MVT: ‖D^n f(x+h·e₀) - D^n f(x)‖ ≤ |h| · sup ‖D^{n+1} f(path)‖
4. Apply Peetre: ‖x‖^k ≤ (1+|h|)^k · (1+‖w‖)^k for path points w
5. Bound (1+‖w‖)^k ≤ 2^k · max(1, ‖w‖^k) and use seminorms

theorem TimeTranslation.continuous_timeTranslationSchwartz (f : TestFunction) : Continuous fun (s : ℝ) => timeTranslationSchwartz s f

Time translation is continuous in the time parameter. For any Schwartz function f, the map s ↦ T_s f is continuous from ℝ to Schwartz space in the Fréchet topology.

Proof Strategy: Reduce to Continuity at Zero

Since T_{s+h} f = T_s(T_h f) by the group action property, and T_s is a continuous linear map, continuity at any point s follows from continuity at 0.

For continuity at 0, we use the Lipschitz bound schwartz_timeTranslation_lipschitz_seminorm: ‖T_h f - f‖{k,n} ≤ |h| · (‖f‖{k,n+1} + ‖f‖_{0,n+1} + 1)

References

Reed-Simon V.3 (Schwartz distributions), Hörmander Ch. 7 (test functions)

Time Translation on Tempered Distributions

Definition 0.2 from the PDF: For φ ∈ S'(ℝ × ℝ³) (tempered distribution), define T_s φ by the pairing:

⟨T_s φ, f⟩ := ⟨φ, T_{-s} f⟩

for all f ∈ S(ℝ × ℝ³).

noncomputable def TimeTranslation.timeTranslationDistribution (s : ℝ) (ω : FieldConfiguration) : FieldConfiguration

Time translation on tempered distributions (field configurations).

The action is defined by duality: ⟨T_s ω, f⟩ = ⟨ω, T_{-s} f⟩

Since FieldConfiguration = WeakDual ℝ TestFunction, and timeTranslationSchwartzCLM (-s) is a continuous linear map, we can simply compose: T_s ω = ω ∘ T_{-s}.

Continuity is automatic since composition of continuous linear maps is continuous.

Equations

• TimeTranslation.timeTranslationDistribution s ω = ω ∘SL TimeTranslation.timeTranslationSchwartzCLM (-s)

@[simp]

theorem TimeTranslation.timeTranslationDistribution_apply (s : ℝ) (ω : FieldConfiguration) (f : TestFunction) : (timeTranslationDistribution s ω) f = ω (timeTranslationSchwartz (-s) f)

The defining property of time translation on distributions.

theorem TimeTranslation.timeTranslationDistribution_add (s t : ℝ) (ω : FieldConfiguration) : timeTranslationDistribution (s + t) ω = timeTranslationDistribution s (timeTranslationDistribution t ω)

Time translation on distributions is a group homomorphism: T_{s+t} = T_s ∘ T_t

@[simp]

theorem TimeTranslation.timeTranslationDistribution_zero (ω : FieldConfiguration) : timeTranslationDistribution 0 ω = ω

Time translation by zero is identity on distributions