# `TimeTranslation.lean` — Informal Summary

> **Source**: [`OSforGFF/Spacetime/TimeTranslation.lean`](../../OSforGFF/Spacetime/TimeTranslation.lean)
> **Generated**: 2026-03-03 00:00
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Defines time translation operators $T_s$ on spacetime points, Schwartz test functions
(real and complex), and tempered distributions, forming a one-parameter group of
automorphisms. The main technical result is a locally-uniform Lipschitz seminorm bound
$$\lVert T_h f - f \rVert_{k,n} \leq \lvert h\rvert \cdot (1+\lvert h\rvert)^k \cdot 2^k \cdot (\lVert f\rVert_{k,n+1} + \lVert f\rVert_{0,n+1} + 1),$$
proved via the Mean Value Theorem, Peetre's inequality, and the chain rule for
iterated Fréchet derivatives. This implies that $s \mapsto T_s f$ is continuous in
the Schwartz topology, as required by the OS4 (Ergodicity) axiom.

## Status

**Main result**: Fully proven

None — file is sorry-free.

**Length**: 907 lines, 9 definition(s) + 19 theorem(s)/lemma(s)

---

## Time Translation on Spacetime Points

### `timeIndex` — Definition

**Lean signature**
```lean
def timeIndex : Fin STDimension
```
**Informal**: The index $0 \in \mathrm{Fin}\,4$ identifying the time coordinate in $\mathbb{R}^4$.

---

### `getTime` — Definition

**Lean signature**
```lean
def getTime (u : SpaceTime) : ℝ
```
**Informal**: Extracts the time coordinate $u_0$ from a spacetime point $u \in \mathbb{R}^4$.

---

### `timeShift` — Definition

**Lean signature**
```lean
def timeShift (s : ℝ) (u : SpaceTime) : SpaceTime
```
**Informal**: Time translation of a spacetime point by $s$: $(T_s u)_0 = u_0 + s$ and $(T_s u)_i = u_i$ for $i \neq 0$.

---

### [`timeShift_time`](../../OSforGFF/Spacetime/TimeTranslation.lean#L74) — Lemma

**Statement**: The time component of the shifted point satisfies $\mathrm{getTime}(T_s u) = \mathrm{getTime}(u) + s$.

**Proof uses**: *(direct tactic proof)*

---

### [`timeShift_spatial`](../../OSforGFF/Spacetime/TimeTranslation.lean#L80) — Lemma

**Statement**: Spatial components are unchanged: $(T_s u)_i = u_i$ for any $i$ with $i \neq 0$.

**Proof uses**: *(direct tactic proof)*

---

### [`timeShift_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L86) — Lemma

**Statement**: Time shifts compose as $T_{s+t} = T_s \circ T_t$.

**Proof uses**: *(direct tactic proof)*

---

### [`timeShift_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L97) — Lemma

**Statement**: $T_0 = \mathrm{id}$.

**Proof uses**: *(direct tactic proof)*

---

### [`timeShift_comm`](../../OSforGFF/Spacetime/TimeTranslation.lean#L104) — Lemma

**Statement**: Time shifts commute: $T_s \circ T_t = T_t \circ T_s$.

**Proof uses**: [`timeShift_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L86)

---

### [`timeShift_contDiff`](../../OSforGFF/Spacetime/TimeTranslation.lean#L110) — Lemma

**Statement**: The map $u \mapsto T_s u$ is smooth (of class $C^\infty$) as a map $\mathbb{R}^4 \to \mathbb{R}^4$.

**Proof uses**: `contDiff_piLp'`, `contDiff_apply`

---

### [`timeShift_dist`](../../OSforGFF/Spacetime/TimeTranslation.lean#L122) — Lemma

**Statement**: Time shift is an isometry: $\mathrm{dist}(T_s u, T_s v) = \mathrm{dist}(u, v)$.

**Proof uses**: `EuclideanSpace.dist_eq`

---

### [`timeShift_isometry`](../../OSforGFF/Spacetime/TimeTranslation.lean#L133) — Lemma

**Statement**: $T_s$ is an isometry of $\mathbb{R}^4$.

**Proof uses**: [`timeShift_dist`](../../OSforGFF/Spacetime/TimeTranslation.lean#L122)

---

### [`timeShift_antilipschitz`](../../OSforGFF/Spacetime/TimeTranslation.lean#L138) — Lemma

**Statement**: $T_s$ is antilipschitz with constant $1$ (follows immediately from being an isometry).

**Proof uses**: [`timeShift_isometry`](../../OSforGFF/Spacetime/TimeTranslation.lean#L133)

---

### `timeShiftConst` — Definition

**Lean signature**
```lean
def timeShiftConst (s : ℝ) : SpaceTime
```
**Informal**: The constant vector $(s, 0, 0, 0) \in \mathbb{R}^4$ used to express the time shift as $T_s u = u + \mathrm{timeShiftConst}(s)$.

---

### [`timeShift_eq_add_const`](../../OSforGFF/Spacetime/TimeTranslation.lean#L146) — Lemma

**Statement**: $T_s u = u + \mathrm{timeShiftConst}(s)$ for all $u \in \mathbb{R}^4$.

**Proof uses**: *(direct tactic proof)*

---

### [`timeShift_hasTemperateGrowth`](../../OSforGFF/Spacetime/TimeTranslation.lean#L155) — Lemma

**Statement**: The time shift $T_s$ has temperate growth as a map $\mathbb{R}^4 \to \mathbb{R}^4$, which is needed for composition with Schwartz functions.

**Proof uses**: [`timeShift_eq_add_const`](../../OSforGFF/Spacetime/TimeTranslation.lean#L146), `Function.HasTemperateGrowth.of_fderiv`, `Function.HasTemperateGrowth.const`

---

## Time Translation on Schwartz Functions

### `timeTranslationSchwartzCLM` — Definition

**Lean signature**
```lean
def timeTranslationSchwartzCLM (s : ℝ) : TestFunction →L[ℝ] TestFunction
```
**Informal**: Time translation as a continuous $\mathbb{R}$-linear map on real Schwartz functions, constructed via `SchwartzMap.compCLMOfAntilipschitz` using the isometry and temperate-growth properties of `timeShift s`.

---

### `timeTranslationSchwartz` — Definition

**Lean signature**
```lean
def timeTranslationSchwartz (s : ℝ) (f : TestFunction) : TestFunction
```
**Informal**: The time-translated Schwartz function $(T_s f)(u) = f(T_s u) = f(u_0 + s, u_1, u_2, u_3)$.

---

### `timeTranslationSchwartzℂCLM` — Definition

**Lean signature**
```lean
def timeTranslationSchwartzℂCLM (s : ℝ) : TestFunctionℂ →L[ℂ] TestFunctionℂ
```
**Informal**: Time translation as a continuous $\mathbb{C}$-linear map on complex Schwartz functions.

---

### `timeTranslationSchwartzℂ` — Definition

**Lean signature**
```lean
def timeTranslationSchwartzℂ (s : ℝ) (f : TestFunctionℂ) : TestFunctionℂ
```
**Informal**: Time translation of a complex Schwartz function: $(T_s f)(u) = f(T_s u)$.

---

### [`timeTranslationSchwartz_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L226) — Lemma

**Statement**: The translated function evaluates as $(T_s f)(u) = f(T_s u)$.

**Proof uses**: `SchwartzMap.compCLMOfAntilipschitz_apply`

---

### [`timeTranslationSchwartzℂ_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L232) — Lemma

**Statement**: The complex translated function evaluates as $(T_s f)(u) = f(T_s u)$.

**Proof uses**: `SchwartzMap.compCLMOfAntilipschitz_apply`

---

### [`timeTranslationSchwartz_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L239) — Lemma

**Statement**: Group homomorphism property: $T_{s+t} f = T_s(T_t f)$ for real Schwartz functions.

**Proof uses**: [`timeTranslationSchwartz_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L226), [`timeShift_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L86), [`timeShift_comm`](../../OSforGFF/Spacetime/TimeTranslation.lean#L104)

---

### [`timeTranslationSchwartzℂ_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L245) — Lemma

**Statement**: Group homomorphism for complex functions: $T_{s+t} f = T_s(T_t f)$.

**Proof uses**: [`timeTranslationSchwartzℂ_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L232), [`timeShift_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L86), [`timeShift_comm`](../../OSforGFF/Spacetime/TimeTranslation.lean#L104)

---

### [`timeTranslationSchwartz_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L252) — Lemma

**Statement**: $T_0 f = f$ for real Schwartz functions.

**Proof uses**: [`timeShift_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L97)

---

### [`timeTranslationSchwartzℂ_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L259) — Lemma

**Statement**: $T_0 f = f$ for complex Schwartz functions.

**Proof uses**: [`timeShift_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L97)

---

## Fundamental Theorem of Calculus for Time Translation

### `unitTimeDir` — Definition

**Lean signature**
```lean
def unitTimeDir : SpaceTime
```
**Informal**: The unit vector $e_0 = (1, 0, 0, 0) \in \mathbb{R}^4$ in the time direction, used to express the path $t \mapsto x + t \cdot e_0$ in the MVT proof.

---

### [`continuous_timeShift_param`](../../OSforGFF/Spacetime/TimeTranslation.lean#L288) — Lemma

**Statement**: For any fixed $x \in \mathbb{R}^4$, the map $s \mapsto T_s x$ is continuous from $\mathbb{R}$ to $\mathbb{R}^4$.

**Proof uses**: [`unitTimeDir`](../../OSforGFF/Spacetime/TimeTranslation.lean#L285)

---

### [`peetre_weight_bound`](../../OSforGFF/Spacetime/TimeTranslation.lean#L301) — Lemma

**Statement**: Peetre's inequality for polynomial weights: $(1 + \lVert x \rVert)^k \leq (1 + \lVert x + y \rVert)^k \cdot (1 + \lVert y \rVert)^k$ for all $x, y \in \mathbb{R}^4$.

**Proof uses**: *(direct tactic proof)*

---

### [`iteratedFDeriv_timeTranslationSchwartz`](../../OSforGFF/Spacetime/TimeTranslation.lean#L317) — Lemma

**Statement**: Iterated derivatives commute with time translation: $\partial^n(T_h f)(x) = \partial^n f(x + h \cdot e_0)$.

**Proof uses**: [`timeTranslationSchwartz_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L226), [`timeShift_eq_add_const`](../../OSforGFF/Spacetime/TimeTranslation.lean#L146), `iteratedFDeriv_comp_add_right`

---

### [`schwartz_timeTranslation_lipschitz_seminorm`](../../OSforGFF/Spacetime/TimeTranslation.lean#L358) — Theorem

**Statement**: For any Schwartz function $f$ and time shift $h$, the Schwartz seminorm of $T_h f - f$ satisfies:
$$\lVert T_h f - f \rVert_{k,n} \leq \lvert h\rvert \cdot (1+\lvert h\rvert)^k \cdot 2^k \cdot \bigl(\lVert f\rVert_{k,n+1} + \lVert f\rVert_{0,n+1} + 1\bigr).$$

**Proof uses**: `SchwartzMap.seminorm_le_bound`, [`iteratedFDeriv_timeTranslationSchwartz`](../../OSforGFF/Spacetime/TimeTranslation.lean#L317), [`peetre_weight_bound`](../../OSforGFF/Spacetime/TimeTranslation.lean#L301), `fderiv_iteratedFDeriv`, `LinearIsometryEquiv.norm_map`, `SchwartzMap.le_seminorm`, `Convex.norm_image_sub_le_of_norm_deriv_le`, `Real.mul_iSup_of_nonneg`

---

### [`continuous_timeTranslationSchwartz`](../../OSforGFF/Spacetime/TimeTranslation.lean#L746) — Lemma

**Statement**: For any Schwartz function $f$, the map $s \mapsto T_s f$ is continuous from $\mathbb{R}$ to the Schwartz space.

**Proof uses**: [`schwartz_timeTranslation_lipschitz_seminorm`](../../OSforGFF/Spacetime/TimeTranslation.lean#L358), [`timeTranslationSchwartzCLM`](../../OSforGFF/Spacetime/TimeTranslation.lean#L199), `schwartz_withSeminorms`, `schwartzSeminormFamily`

---

## Time Translation on Tempered Distributions

### `timeTranslationDistribution` — Definition

**Lean signature**
```lean
def timeTranslationDistribution (s : ℝ) (ω : FieldConfiguration) : FieldConfiguration
```
**Informal**: Time translation of a tempered distribution $\omega$ by duality: $\langle T_s \omega, f \rangle = \langle \omega, T_{-s} f \rangle$, implemented as $\omega \circ T_{-s}$.

---

### [`timeTranslationDistribution_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L879) — Lemma

**Statement**: The defining pairing property: $(T_s \omega)(f) = \omega(T_{-s} f)$.

**Proof uses**: *(direct tactic proof)*

---

### [`timeTranslationDistribution_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L883) — Lemma

**Statement**: Group homomorphism on distributions: $T_{s+t} \omega = T_s(T_t \omega)$.

**Proof uses**: [`timeTranslationDistribution_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L879), [`timeTranslationSchwartz_add`](../../OSforGFF/Spacetime/TimeTranslation.lean#L239)

---

### [`timeTranslationDistribution_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L900) — Lemma

**Statement**: $T_0 \omega = \omega$ for tempered distributions.

**Proof uses**: [`timeTranslationDistribution_apply`](../../OSforGFF/Spacetime/TimeTranslation.lean#L879), [`timeTranslationSchwartz_zero`](../../OSforGFF/Spacetime/TimeTranslation.lean#L252)

---

*This file has **9** definitions and **19** theorems/lemmas (0 with sorry).*