@[reducible, inline]

abbrev CM17Lagrangian.Spacetime (n : ℕ) : Type

Spacetime $\mathbb{R}^{1+n}$ as the function type $\{0, 1, \ldots, n\} \to \mathbb{R}$. The index $0$ is the time coordinate; indices $1, \ldots, n$ are spatial.

@[reducible, inline]

abbrev CM17Lagrangian.ScalarField (n : ℕ) : Type

A scalar field on $\mathbb{R}^{1+n}$, i.e. a real-valued function $\phi : \mathbb{R}^{1+n} \to \mathbb{R}$.

def CM17Lagrangian.Lagrangian (n : ℕ) : Type

A Lagrangian density $L(\phi, \partial \phi, x)$: a real-valued function of the field value, the spacetime gradient (an $(n+1)$-tuple of partial derivatives), and the spacetime point.

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

The spacetime gradient $(\partial_{\mu} \phi)_{\mu = 0, \ldots, n}$ of a scalar field $\phi$ at the point $x$, i.e. the $(n+1)$-tuple of partial derivatives.

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

The action functional $\mathcal{S}_K[\phi] = \int_K L(\phi(x), \partial \phi(x), x)\, dx$ of a scalar field $\phi$ on a region $K \subset \mathbb{R}^{1+n}$.

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

A variation $\psi$ supported in $K$: a smooth ($C^{\infty}$) scalar field whose support is contained in the region $K$. This is the class of admissible test perturbations of $\phi$.

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

The one-parameter perturbation $\phi_{\varepsilon}(x) = \phi(x) + \varepsilon \psi(x)$ used to define the first variation of the action.

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

A scalar field $\phi$ is a stationary point of the action: for every compact region $K$ and every variation $\psi$ supported in $K$, the first variation of the action vanishes, $\left. \frac{d}{d\varepsilon} \right|_{\varepsilon = 0} \mathcal{S}_K[\phi + \varepsilon \psi] = 0$.

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

Partial derivative of the Lagrangian with respect to the field value $\phi$: $\partial L / \partial \phi$ evaluated at $(\phi(x), \partial \phi(x), x)$.

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

Partial derivative of the Lagrangian with respect to the $\alpha$-th component of the gradient: $\partial L / \partial(\partial_{\alpha} \phi)$ evaluated at $(\phi(x), \partial \phi(x), x)$.

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

The Euler-Lagrange operator applied to $\phi$ at $x$: $\mathrm{EL}\phi = \dfrac{\partial L}{\partial \phi}

• \sum_{\alpha} \partial_{\alpha} !\left( \dfrac{\partial L}{\partial(\partial_{\alpha} \phi)} \right)$. A scalar field is stationary iff this operator vanishes identically.

theorem CM17Lagrangian.ibp_fundamental_lemma {n : ℕ} (f : Spacetime n → ℝ) (hf_cont : 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 \, dx = 0$ for every compact $K$ and every smooth variation $\psi$ supported in $K$, then $f \equiv 0$.

theorem CM17Lagrangian.leibniz_smooth {n : ℕ} (F : ℝ → Spacetime n → ℝ) (F' : Spacetime n → ℝ) (K : Set (Spacetime n)) (ε₀ : ℝ) (hK : IsCompact K) (hpw : ∀ x ∈ K, HasDerivAt (fun (x_1 : ℝ) => F x_1 x) (F' x) ε₀) (hF_cont : ∀ (ε : ℝ), ContinuousOn (F ε) K) (hF'_cont : ContinuousOn F' K) : HasDerivAt (fun (ε : ℝ) => ∫ (x : Spacetime n) in K, F ε x) (∫ (x : Spacetime n) in K, F' x) ε₀

Smooth differentiation under the integral sign on a compact domain: if at $\varepsilon_0$ the parameter derivative $\partial_{\varepsilon} F(\varepsilon, x)$ exists pointwise with limit $F'(x)$ and both $F(\varepsilon, \cdot)$ and $F'$ are continuous on $K$, then the parameterized integral $\varepsilon \mapsto \int_K F(\varepsilon, x) \, dx$ has derivative $\int_K F'(x) \, dx$ at $\varepsilon_0$.

theorem CM17Lagrangian.lagrangian_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

Chain rule for the Lagrangian along a perturbation: at $\varepsilon = 0$, the derivative of $\varepsilon \mapsto L(\phi + \varepsilon \psi, \partial(\phi + \varepsilon \psi), x)$ equals $\partial_{\phi} L \cdot \psi + \sum_{\alpha} \partial_{(\partial_{\alpha} \phi)} L \cdot \partial_{\alpha} \psi$.

theorem CM17Lagrangian.lagrangian_integrand_continuous {n : ℕ} (L : Lagrangian n) (φ ψ : ScalarField n) (K : Set (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 ℝ (↑⊤) ψ) : (∀ (ε : ℝ), ContinuousOn (fun (x : Spacetime n) => L (φ x + ε * ψ x) (spacetimeGradient (perturbedField φ ψ ε) x) x) K) ∧ ContinuousOn (fun (x : Spacetime n) => dL_dφ L φ x * ψ x + ∑ α : Fin (n + 1), dL_dgrad L φ x α * spacetimeGradient ψ x α) K

Continuity hypotheses needed to apply differentiation under the integral: both the parameter-dependent Lagrangian integrand $L(\phi_{\varepsilon}, \partial \phi_{\varepsilon}, x)$ and the limit integrand $\partial_{\phi} L \cdot \psi + \sum_{\alpha} \partial_{(\partial_{\alpha} \phi)} L \cdot \partial_{\alpha} \psi$ are continuous on $K$.

theorem CM17Lagrangian.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 a single coordinate direction: for $\psi$ compactly supported in $K$ and $f$ of class $C^1$, $\int_K f \, \partial_{\alpha} \psi \, dx = -\int_K (\partial_{\alpha} f) \, \psi \, dx$. The boundary term vanishes because $\psi$ is supported in $K$.

theorem CM17Lagrangian.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 all terms appearing in the Euler-Lagrange expansion: each piece of $\partial_{\phi} L \cdot \psi$, $\sum_{\alpha} \partial_{(\partial_{\alpha} \phi)} L \cdot \partial_{\alpha} \psi$, the integration-by-parts substitute $\sum_{\alpha} (-\partial_{\alpha} \partial_{(\partial_{\alpha} \phi)} L) \cdot \psi$, and their per-coordinate components are integrable on $K$.

theorem CM17Lagrangian.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 α

Smoothness of the gradient-derivative of the Lagrangian: if $L$ is $C^2$ in its arguments and $\phi$ is $C^2$, then $x \mapsto \partial_{(\partial_{\alpha} \phi)} L (\phi(x), \partial \phi(x), x)$ is $C^1$.

theorem CM17Lagrangian.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

Per-coordinate integration by parts applied to the gradient term: the integral $\int_K \sum_{\alpha} \partial_{(\partial_{\alpha} \phi)} L \cdot \partial_{\alpha} \psi \, dx$ equals $\int_K \sum_{\alpha} \bigl(-\partial_{\alpha} \partial_{(\partial_{\alpha} \phi)} L\bigr) \cdot \psi \, dx$, together with the integrability of all involved terms.

theorem CM17Lagrangian.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 α

Combining the pointwise chain rule with differentiation under the integral, the first variation of the action equals the integral of the linearized integrand: $\left. \frac{d}{d\varepsilon} \right|_{\varepsilon = 0} \mathcal{S}_K[\phi + \varepsilon \psi] = \int_K \left( \partial_{\phi} L \cdot \psi + \sum_{\alpha} \partial_{(\partial_{\alpha} \phi)} L \cdot \partial_{\alpha} \psi \right) dx$.

theorem CM17Lagrangian.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

Integrating by parts reorganizes the linearized integrand as the Euler-Lagrange operator times $\psi$: $\int_K \left( \partial_{\phi} L \cdot \psi + \sum_{\alpha} \partial_{(\partial_{\alpha} \phi)} L \cdot \partial_{\alpha} \psi \right) dx = \int_K \mathrm{EL}[\phi] \cdot \psi \, dx$.

theorem CM17Lagrangian.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 and the integration by parts, the first variation of the action equals the $L^2$-pairing of the Euler-Lagrange operator with the test variation, $\left. \frac{d}{d\varepsilon} \right|_{\varepsilon = 0} \mathcal{S}_K[\phi + \varepsilon \psi] = \int_K \mathrm{EL}[\phi](x) \cdot \psi(x) \, dx$.

theorem CM17Lagrangian.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 φ) (hEL_cont : Continuous (eulerLagrangeOperator L φ)) : IsStationaryPoint L φ ↔ ∀ (x : Spacetime n), eulerLagrangeOperator L φ x = 0

Euler-Lagrange equations: a sufficiently regular field $\phi$ is a stationary point of the action if and only if it satisfies the Euler-Lagrange equation $\mathrm{EL}\phi = \dfrac{\partial L}{\partial \phi}

• \sum_{\alpha} \partial_{\alpha} !\left( \dfrac{\partial L}{\partial(\partial_{\alpha} \phi)} \right) = 0$ for all $x$.