@[reducible, inline]

abbrev ODEFlow.Spacetime (n : ℕ) : Type

A spacetime point in $\mathbb{R}^{1+n}$.

@[reducible, inline]

abbrev ODEFlow.ScalarField (n : ℕ) : Type

A real-valued scalar field on $\mathbb{R}^{1+n}$.

@[reducible, inline]

abbrev ODEFlow.VectorField (n : ℕ) : Type

A vector field on $\mathbb{R}^{1+n}$, i.e. a map from spacetime points to vectors.

@[reducible, inline]

abbrev ODEFlow.Metric (n : ℕ) : Type

A spacetime metric: at each point of $\mathbb{R}^{1+n}$, a function $m_{\mu\nu}$ on pairs of indices.

noncomputable def ODEFlow.spacetimeGradient {n : ℕ} (φ : ScalarField n) (x : Spacetime n) : Fin (n + 1) → ℝ

The spacetime gradient of a scalar field $\varphi$: the index-$\mu$ component is the partial derivative $\partial_\mu \varphi$.

noncomputable def ODEFlow.jacobian {n : ℕ} (F : Spacetime n → Spacetime n) (x : Spacetime n) : Fin (n + 1) → Fin (n + 1) → ℝ

The Jacobian of a map $F : \mathbb{R}^{1+n} \to \mathbb{R}^{1+n}$ at $x$: $(\partial F^\mu / \partial x^\nu)(x)$.

def ODEFlow.kroneckerDelta (n : ℕ) (μ ν : Fin (n + 1)) : ℝ

The Kronecker delta $\delta_{\mu\nu}$, equal to $1$ if $\mu = \nu$ and $0$ otherwise.

noncomputable def ODEFlow.divergence {n : ℕ} (Y : VectorField n) (x : Spacetime n) : ℝ

The (spacetime) divergence of a vector field $Y$: $\nabla \cdot Y = \sum_\alpha \partial_\alpha Y^\alpha$.

noncomputable def ODEFlow.jacobianMatrix {n : ℕ} (G : Spacetime n → Spacetime n) (x : Spacetime n) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The Jacobian of a spacetime map packaged as a matrix.

def ODEFlow.HasBoundedDerivatives {n : ℕ} (Y : VectorField n) (C : ℝ) : Prop

A vector field $Y$ has all partial derivatives uniformly bounded by $C > 0$: $|\partial_\mu Y^\nu(x)| \leq C$ for all $x, \mu, \nu$.

structure ODEFlow.FlowMapData (n : ℕ) : Type

Data packaging the ODE flow generated by a vector field $Y$ on spacetime $\mathbb{R}^{1+n}$ (Proposition 2.0.1): the flow map $F_\epsilon$ on $[-\epsilon_0, \epsilon_0]$, its smoothness, the one-parameter group properties, the Taylor expansion, and the corresponding expansion of the Jacobian.

• Y : VectorField n
• Y_smooth : ContDiff ℝ ⊤ self.Y
• C_bound : ℝ
• Y_bounded : HasBoundedDerivatives self.Y self.C_bound
• F : ℝ → Spacetime n → Spacetime n
• ε₀ : ℝ
• ε₀_pos : 0 < self.ε₀
• F_smooth (ε : ℝ) : |ε| ≤ self.ε₀ → ContDiff ℝ ⊤ (self.F ε)
• F_ode (x : Spacetime n) (μ : Fin (n + 1)) (ε : ℝ) : |ε| ≤ self.ε₀ → deriv (fun (ε' : ℝ) => self.F ε' x μ) ε = self.Y (self.F ε x) μ
• F_initial (x : Spacetime n) : self.F 0 x = x
• F_inverse (ε : ℝ) : |ε| ≤ self.ε₀ → ∀ (x : Spacetime n), self.F (-ε) (self.F ε x) = x
• F_group (ε₁ ε₂ : ℝ) : |ε₁| + |ε₂| ≤ self.ε₀ → ∀ (x : Spacetime n), self.F ε₁ (self.F ε₂ x) = self.F (ε₁ + ε₂) x
• F_commutative (ε₁ ε₂ : ℝ) : |ε₁| + |ε₂| ≤ self.ε₀ → ∀ (x : Spacetime n), self.F ε₂ (self.F ε₁ x) = self.F (ε₁ + ε₂) x
• R : ℝ → Spacetime n → Spacetime n
• R_smooth : ContDiff ℝ ⊤ fun (p : ℝ × Spacetime n) => self.R p.1 p.2
• F_taylor (ε : ℝ) (x : Spacetime n) (μ : Fin (n + 1)) : self.F ε x μ = x μ + ε * self.Y x μ + ε ^ 2 * self.R ε x μ
• jacobian_expansion (ε : ℝ) : |ε| ≤ self.ε₀ → ∀ (x : Spacetime n) (μ ν : Fin (n + 1)), jacobian (self.F ε) x μ ν = kroneckerDelta n μ ν + ε * jacobian self.Y x μ ν + ε ^ 2 * jacobian (self.R ε) x μ ν

def ODEFlow.transformScalar {n : ℕ} (φ : ScalarField n) (Finv : Spacetime n → Spacetime n) : ScalarField n

Transformation of a scalar field under a change of coordinates: $\widetilde{\varphi}(\widetilde{x}) = \varphi(F^{-1}(\widetilde{x}))$ (cf. Definition 2.0.6).

noncomputable def ODEFlow.transformGradient {n : ℕ} (φ : ScalarField n) (Finv : Spacetime n → Spacetime n) (xt : Spacetime n) : Fin (n + 1) → ℝ

Transformation of the spacetime gradient of a scalar field under a change of coordinates (Definition 2.0.6): $\widetilde{\nabla}_\mu \widetilde{\varphi} = (M^{-1})_\mu{}^\alpha \nabla_\alpha \varphi$, expressed using the Jacobian of $F^{-1}$.

noncomputable def ODEFlow.transformMetric {n : ℕ} (m : Metric n) (Finv : Spacetime n → Spacetime n) : Metric n

Transformation of a metric under a change of coordinates (Definition 2.0.6): $\widetilde{m}_{\mu\nu} = (M^{-1})_\mu{}^\alpha (M^{-1})_\nu{}^\beta m_{\alpha\beta}$, expressed using the Jacobian of $F^{-1}$.

def ODEFlow.MetricLagrangian (n : ℕ) : Type

A Lagrangian as a function of $(\varphi, \nabla \varphi, m)$: the scalar field value, its gradient, and the metric components.

def ODEFlow.IsCoordinateInvariant {n : ℕ} (L : MetricLagrangian n) : Prop

A Lagrangian $\mathcal{L}(\varphi, \nabla \varphi, m)$ is coordinate invariant (Definition 2.0.7) if for every smooth diffeomorphism $\Psi$ and every scalar field $\varphi$ and metric $m$, the value $\mathcal{L}$ evaluated on the original fields at $x$ equals $\mathcal{L}$ evaluated on the transformed fields at $\widetilde{x} = \Psi(x)$.