@[reducible, inline]

abbrev CM18.Spacetime (n : ℕ) : Type

Spacetime $\mathbb{R}^{1+n}$ modeled as functions $\text{Fin}(n+1) \to \mathbb{R}$. The component indexed by $0$ is time and components $1, \ldots, n$ are spatial.

@[reducible, inline]

abbrev CM18.ScalarField (n : ℕ) : Type

A real-valued scalar field on $(1+n)$-dimensional spacetime.

def CM18.Lagrangian (n : ℕ) : Type

A Lagrangian (Definition 1.0.1) is a function of the field value $\phi \in \mathbb{R}$, its spacetime gradient $\nabla\phi \in \mathbb{R}^{1+n}$, and the spacetime coordinate $x$. We write $\mathcal{L}(\phi, \nabla\phi, x)$.

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

The spacetime gradient $\nabla\phi$ of a scalar field $\phi$ at $x$, given by the components $(\nabla\phi)_\mu = \partial_\mu \phi(x) = (D\phi)_x(e_\mu)$ where $e_\mu$ is the $\mu$-th coordinate vector.

noncomputable def CM18.action {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (K : Set (Spacetime n)) : ℝ

The action (Definition 1.0.2) of a field $\phi$ over a compact set $\mathfrak{K} \subset \mathbb{R}^{1+n}$: $$\mathcal{A}[\phi; \mathfrak{K}] = \int_{\mathfrak{K}} \mathcal{L}(\phi(x), \nabla\phi(x), x)\, d^{1+n}x.$$

def CM18.IsVariation {n : ℕ} (K : Set (Spacetime n)) (ψ : ScalarField n) : Prop

A variation (Definition 1.0.3) on a set $K$ is a smooth scalar field $\psi$ whose support is contained in $K$; equivalently $\psi \in C_c^\infty(K)$.

def CM18.perturbedField {n : ℕ} (φ ψ : ScalarField n) (ε : ℝ) : ScalarField n

The perturbed field (Definition 1.0.4) $\phi_\varepsilon := \phi + \varepsilon\psi$.

def CM18.IsStationaryPoint {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) : Prop

$\phi$ is a stationary point of the action (Definition 1.0.5) iff for every compact set $\mathfrak{K}$ and every variation $\psi \in C_c^\infty(\mathfrak{K})$, $$\left.\frac{d}{d\varepsilon}\right|_{\varepsilon=0} \mathcal{A}[\phi_\varepsilon; \mathfrak{K}] = 0.$$

noncomputable def CM18.dL_dφ {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (x : Spacetime n) : ℝ

The partial derivative $\partial\mathcal{L}/\partial\phi$ evaluated at $(\phi(x), \nabla\phi(x), x)$.

noncomputable def CM18.dL_dgrad {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (x : Spacetime n) (α : Fin (n + 1)) : ℝ

The partial derivative $\partial\mathcal{L}/\partial(\nabla_\alpha\phi)$ evaluated at $(\phi(x), \nabla\phi(x), x)$, holding the other gradient components, $\phi$, and $x$ fixed.

noncomputable def CM18.eulerLagrangeOperator {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (x : Spacetime n) : ℝ

The Euler-Lagrange operator $$E[\phi](x) = \frac{\partial\mathcal{L}}{\partial\phi} - \sum_\alpha \nabla_\alpha\left( \frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)}\right).$$ The Euler-Lagrange PDE (Theorem 1.1) is $E[\phi] = 0$.

theorem CM18.ibp_fundamental_lemma {n : ℕ} (f : Spacetime n → ℝ) (hcont : Continuous f) (hf : ∀ (K : Set (Spacetime n)), IsCompact K → ∀ (ψ : ScalarField n), IsVariation K ψ → ∫ (x : Spacetime n) in K, f x * ψ x = 0) (x : Spacetime n) : f x = 0

Fundamental lemma of the calculus of variations: if $f$ is continuous and $\int_K f\psi = 0$ for every compact $K$ and every variation $\psi \in C_c^\infty(K)$, then $f \equiv 0$.

theorem CM18.pointwise_chain_rule {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (x : Spacetime n) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) (hψ : ContDiff ℝ (↑⊤) ψ) : HasDerivAt (fun (ε : ℝ) => L (φ x + ε * ψ x) (spacetimeGradient (perturbedField φ ψ ε) x) x) (dL_dφ L φ x * ψ x + ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α) 0

Pointwise chain rule at $\varepsilon = 0$ for the integrand of the action: the derivative in $\varepsilon$ of $\mathcal{L}(\phi_\varepsilon(x), \nabla\phi_\varepsilon(x), x)$ at $\varepsilon=0$ equals $\frac{\partial\mathcal{L}}{\partial\phi}\psi + \sum_\alpha \frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)} \nabla_\alpha\psi$.

theorem CM18.general_chain_rule_all_eps {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (x : Spacetime n) (ε₀ : ℝ) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : DifferentiableAt ℝ φ x) (hψ : DifferentiableAt ℝ ψ x) : HasDerivAt (fun (ε : ℝ) => L (φ x + ε * ψ x) (spacetimeGradient (perturbedField φ ψ ε) x) x) ((fderiv ℝ (fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (φ x + ε₀ * ψ x, fun (μ : Fin (n + 1)) => spacetimeGradient φ x μ + ε₀ * spacetimeGradient ψ x μ, x)) (ψ x, spacetimeGradient ψ x, 0)) ε₀

General pointwise chain rule at an arbitrary base point $\varepsilon_0$: gives a closed-form expression for $\frac{d}{d\varepsilon} \mathcal{L}(\phi_\varepsilon(x), \nabla\phi_\varepsilon(x), x)$ at any $\varepsilon = \varepsilon_0$ in terms of the full Fréchet derivative of $\mathcal{L}$. Used to dominate the difference quotient when differentiating under the integral sign.

theorem CM18.leibniz_chain_rule {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (K : Set (Spacetime n)) (hK : IsCompact K) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) (hψ : ContDiff ℝ (↑⊤) ψ) : deriv (fun (ε : ℝ) => action L (perturbedField φ ψ ε) K) 0 = ∫ (x : Spacetime n) in K, dL_dφ L φ x * ψ x + ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α

Differentiation under the integral sign (Leibniz rule) applied to the action: for smooth data, $$\left.\frac{d}{d\varepsilon}\right|_{\varepsilon=0} \mathcal{A}[\phi_\varepsilon; K] = \int_K \left(\frac{\partial\mathcal{L}}{\partial\phi}\,\psi + \sum_\alpha \frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)}\,\nabla_\alpha\psi\right) d^{1+n}x.$$

theorem CM18.ibp_single_coordinate {n : ℕ} (f : Spacetime n → ℝ) (ψ : ScalarField n) (K : Set (Spacetime n)) (α : Fin (n + 1)) (hK : IsCompact K) (hψ : IsVariation K ψ) (hf : ContDiff ℝ 1 f) : ∫ (x : Spacetime n) in K, f x * spacetimeGradient ψ x α = ∫ (x : Spacetime n) in K, -(fderiv ℝ f x) (Pi.single α 1) * ψ x

Integration by parts in one coordinate direction $\alpha$: since $\psi$ vanishes near $\partial K$, $\int_K f\,\partial_\alpha\psi\, d^{1+n}x = -\int_K (\partial_\alpha f)\,\psi\, d^{1+n}x$.

theorem CM18.el_terms_integrable {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (K : Set (Spacetime n)) (hK : IsCompact K) (hψ : IsVariation K ψ) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) : MeasureTheory.IntegrableOn (fun (x : Spacetime n) => dL_dφ L φ x * ψ x) K MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Spacetime n) => ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α) K MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Spacetime n) => ∑ α : Fin (n + 1), -(fderiv ℝ (fun (y : Spacetime n) => dL_dgrad L φ y α) x) (Pi.single α 1) * ψ x) K MeasureTheory.volume ∧ (∀ (α : Fin (n + 1)), MeasureTheory.IntegrableOn (fun (x : Spacetime n) => dL_dgrad L φ x α * spacetimeGradient ψ x α) K MeasureTheory.volume) ∧ ∀ (α : Fin (n + 1)), MeasureTheory.IntegrableOn (fun (x : Spacetime n) => -(fderiv ℝ (fun (y : Spacetime n) => dL_dgrad L φ y α) x) (Pi.single α 1) * ψ x) K MeasureTheory.volume

Integrability of the Euler-Lagrange-type terms over the compact set $K$: the field-derivative term, the gradient-derivative sum, the integrated-by-parts sum, and each summand of those sums are integrable on $K$.

theorem CM18.dL_dgrad_contDiff {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (α : Fin (n + 1)) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) : ContDiff ℝ 1 fun (x : Spacetime n) => dL_dgrad L φ x α

If $\mathcal{L}$ is $C^2$ and $\phi$ is $C^2$, then $x \mapsto \partial\mathcal{L}/\partial(\nabla_\alpha\phi)$ evaluated at $(\phi(x), \nabla\phi(x), x)$ is $C^1$. This is the regularity required to integrate by parts.

theorem CM18.ibp_per_coordinate_sum {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (K : Set (Spacetime n)) (hK : IsCompact K) (hψ : IsVariation K ψ) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) : ∫ (x : Spacetime n) in K, ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α = ∫ (x : Spacetime n) in K, ∑ α : Fin (n + 1), -(fderiv ℝ (fun (y : Spacetime n) => dL_dgrad L φ y α) x) (Pi.single α 1) * ψ x ∧ MeasureTheory.IntegrableOn (fun (x : Spacetime n) => dL_dφ L φ x * ψ x) K MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Spacetime n) => ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α) K MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Spacetime n) => ∑ α : Fin (n + 1), -(fderiv ℝ (fun (y : Spacetime n) => dL_dgrad L φ y α) x) (Pi.single α 1) * ψ x) K MeasureTheory.volume

Coordinate-by-coordinate integration by parts applied to each term in the $\sum_\alpha \frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)} \nabla_\alpha\psi$ sum, giving $\sum_\alpha (-\nabla_\alpha \frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)})\psi$, together with the integrability conditions that justify swapping integral and sum.

theorem CM18.ibp_euler_lagrange {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (K : Set (Spacetime n)) (hK : IsCompact K) (hψ : IsVariation K ψ) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) : ∫ (x : Spacetime n) in K, dL_dφ L φ x * ψ x + ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α = ∫ (x : Spacetime n) in K, eulerLagrangeOperator L φ x * ψ x

Integration by parts reassembled: the full first-variation integrand equals the Euler-Lagrange operator times the variation, $$\int_K \left(\frac{\partial\mathcal{L}}{\partial\phi}\,\psi + \sum_\alpha \frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)}\,\nabla_\alpha\psi\right) = \int_K E[\phi](x)\,\psi(x)\, d^{1+n}x.$$

theorem CM18.first_variation_expansion {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (K : Set (Spacetime n)) (hK : IsCompact K) (ψ : ScalarField n) (hψ : IsVariation K ψ) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) : deriv (fun (ε : ℝ) => action L (perturbedField φ ψ ε) K) 0 = ∫ (x : Spacetime n) in K, eulerLagrangeOperator L φ x * ψ x

First-variation formula: combining the Leibniz chain rule with integration by parts, $$\left.\frac{d}{d\varepsilon}\right|_{\varepsilon=0} \mathcal{A}[\phi_\varepsilon; K] = \int_K E[\phi](x)\,\psi(x)\, d^{1+n}x.$$

theorem CM18.euler_lagrange_equation {n : ℕ} (L : Lagrangian n) (φ : ScalarField n) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × Spacetime n) => L p.1 p.2.1 p.2.2) (hφ : ContDiff ℝ 2 φ) : IsStationaryPoint L φ ↔ ∀ (x : Spacetime n), eulerLagrangeOperator L φ x = 0

Theorem 1.1 (Principle of Stationary Action / Euler-Lagrange equation): for a $C^2$ Lagrangian $\mathcal{L}$ and a $C^2$ field $\phi$, $\phi$ is a stationary point of the action if and only if the Euler-Lagrange PDE $$\nabla_\alpha\left(\frac{\partial\mathcal{L}}{\partial(\nabla_\alpha\phi)}\right) = \frac{\partial\mathcal{L}}{\partial\phi}$$ holds pointwise on spacetime.

theorem CM18.proposition_2_0_1_ode_flow {n : ℕ} (Y : Spacetime n → Spacetime n) (hY_smooth : ContDiff ℝ ⊤ Y) (C : ℝ) (hC : 0 < C) (hY_bdd : ∀ (x : Spacetime n) (μ ν : Fin (n + 1)), |(fderiv ℝ (fun (y : Spacetime n) => Y y ν) x) (Pi.single μ 1)| ≤ C) : ∃ ε₀ > 0, ∃ (F : ℝ → Spacetime n → Spacetime n), (∀ (x : Spacetime n), F 0 x = x) ∧ (∀ (x : Spacetime n) (ε : ℝ), |ε| ≤ ε₀ → deriv (fun (s : ℝ) => F s x) ε = Y (F ε x)) ∧ (∀ (x : Spacetime n), ContDiff ℝ ⊤ fun (ε : ℝ) => F ε x) ∧ (∀ (ε : ℝ), ContDiff ℝ ⊤ (F ε)) ∧ (∀ (ε : ℝ), |ε| ≤ ε₀ → Function.Bijective (F ε) ∧ ∀ (x : Spacetime n), F (-ε) (F ε x) = x) ∧ (∀ (ε₁ ε₂ : ℝ), |ε₁| + |ε₂| ≤ ε₀ → ∀ (x : Spacetime n), F ε₁ (F ε₂ x) = F (ε₁ + ε₂) x) ∧ (∀ (x : Spacetime n), ∃ (R : ℝ → Spacetime n → Spacetime n), (∀ (x' : Spacetime n), ContDiff ℝ ⊤ fun (ε : ℝ) => R ε x') ∧ (∀ (ε : ℝ), ContDiff ℝ ⊤ (R ε)) ∧ ∀ (ε : ℝ) (μ : Fin (n + 1)), F ε x μ = x μ + ε * Y x μ + ε ^ 2 * R ε x μ) ∧ (∀ (x : Spacetime n), ∃ (S : ℝ → Spacetime n → Fin (n + 1) → Fin (n + 1) → ℝ), (∀ (x' : Spacetime n), ContDiff ℝ ⊤ fun (ε : ℝ) => S ε x') ∧ ∀ (ε : ℝ) (μ ν : Fin (n + 1)), (fderiv ℝ (fun (y : Spacetime n) => F ε y μ) x) (Pi.single ν 1) = (if μ = ν then 1 else 0) + ε * (fderiv ℝ (fun (y : Spacetime n) => Y y μ) x) (Pi.single ν 1) + ε ^ 2 * S ε x μ ν) ∧ (∀ (x : Spacetime n), ∃ (S : ℝ → Spacetime n → Fin (n + 1) → Fin (n + 1) → ℝ), (∀ (x' : Spacetime n), ContDiff ℝ ⊤ fun (ε : ℝ) => S ε x') ∧ ∀ (ε : ℝ) (μ ν : Fin (n + 1)), (fderiv ℝ (fun (y : Spacetime n) => F (-ε) y μ) (F ε x)) (Pi.single ν 1) = (if μ = ν then 1 else 0) - ε * (fderiv ℝ (fun (y : Spacetime n) => Y y μ) x) (Pi.single ν 1) + ε ^ 2 * S ε x μ ν) ∧ ∀ (x : Spacetime n), ∃ (S : ℝ → Spacetime n → ℝ), (∀ (x' : Spacetime n), ContDiff ℝ ⊤ fun (ε : ℝ) => S ε x') ∧ ∀ (ε : ℝ), (Matrix.of fun (μ ν : Fin (n + 1)) => (fderiv ℝ (fun (y : Spacetime n) => F (-ε) y μ) (F ε x)) (Pi.single ν 1)).det = 1 - ε * ∑ α : Fin (n + 1), (fderiv ℝ (fun (y : Spacetime n) => Y y α) x) (Pi.single α 1) + ε ^ 2 * S ε x

Proposition 2.0.1 (ODE flow generated by a smooth, bounded-gradient vector field): given a smooth vector field $Y$ on $\mathbb{R}^{1+n}$ whose first partial derivatives are uniformly bounded by $C$, the local flow $F_\varepsilon$ of $Y$ exists on a uniform $\varepsilon$-interval and enjoys identity at $\varepsilon=0$, the flow equation, joint smoothness, a one-parameter group law, local bijectivity with explicit inverse $F_{-\varepsilon}$, a Taylor expansion of $F_\varepsilon x$ to second order in $\varepsilon$, Taylor expansions of $D F_{\pm\varepsilon}$ to second order, and the Jacobian determinant expansion $\det DF_{-\varepsilon}|_{F_\varepsilon x} = 1 - \varepsilon\,\nabla_\alpha Y^\alpha(x) + O(\varepsilon^2)$.