@[reducible, inline]

abbrev FieldTransformation.Spacetime (n : ℕ) : Type

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

@[reducible, inline]

abbrev FieldTransformation.ScalarField (n : ℕ) : Type

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

@[reducible, inline]

abbrev FieldTransformation.SpacetimeMetric (n : ℕ) : Type

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

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

The spacetime gradient of a scalar field $\varphi$: $(\nabla \varphi)_\mu = \partial_\mu \varphi$.

noncomputable def FieldTransformation.jacobianMatrix {n : ℕ} (Ψ : Spacetime n → Spacetime n) (x : Spacetime n) (μ ν : Fin (n + 1)) : ℝ

Component $\partial \Psi^\mu / \partial x^\nu$ of the Jacobian of a spacetime diffeomorphism $\Psi$ at $x$.

def FieldTransformation.transformedField {n : ℕ} (φ : ScalarField n) (Ψinv : Spacetime n → Spacetime n) (xt : Spacetime n) : ℝ

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

noncomputable def FieldTransformation.transformedGradient {n : ℕ} (φ : ScalarField n) (Ψinv : Spacetime n → Spacetime n) (xt : Spacetime n) (μ : Fin (n + 1)) : ℝ

Transformed gradient of a scalar field under a change of coordinates (Definition 2.0.6): $\widetilde{\nabla}_\mu \widetilde{\varphi}(\widetilde{x}) = (M^{-1})_\mu{}^\alpha \nabla_\alpha \varphi(\Psi^{-1}(\widetilde{x}))$.

noncomputable def FieldTransformation.transformedMetric {n : ℕ} (m : SpacetimeMetric n) (Ψinv : Spacetime n → Spacetime n) (xt : Spacetime n) (μ ν : Fin (n + 1)) : ℝ

Transformed metric under a change of coordinates (Definition 2.0.6): $\widetilde{m}_{\mu\nu}(\widetilde{x}) = (M^{-1})_\mu{}^\alpha (M^{-1})_\nu{}^\beta m_{\alpha\beta}(\Psi^{-1}(\widetilde{x}))$.

noncomputable def FieldTransformation.transformedInverseMetric {n : ℕ} (mInv : SpacetimeMetric n) (Ψ Ψinv : Spacetime n → Spacetime n) (xt : Spacetime n) (μ ν : Fin (n + 1)) : ℝ

Transformed inverse metric under a change of coordinates (Definition 2.0.6): $(\widetilde{m}^{-1})^{\mu\nu}(\widetilde{x}) = M_\alpha{}^\mu M_\beta{}^\nu (m^{-1})^{\alpha\beta}(\Psi^{-1}(\widetilde{x}))$.