Euler–Lagrange equation

euler_lagrange_equation

Submitter: Kim Morrison.

Notes: §44 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The Euler–Lagrange equation: a sufficiently regular stationary path x of the action I(y) = ∫_a^b L(t, y(t), y'(t)) dt satisfies ∂L/∂x = (d/dt)(∂L/∂x') pointwise on the open interval (a, b). Stationarity is expressed as the first variation of the action vanishing against every smooth compactly supported perturbation inside (a, b). It is the central necessary condition of the calculus of variations. mathlib has related ingredients such as the fundamental lemma of the calculus of variations, but no bundled action-functional extremum notion and no Euler–Lagrange theorem.

Source: L. Euler (1744) and J.-L. Lagrange (1755). Listed as §44 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Let h be a smooth variation with compact support in (a, b). Differentiating I(x + ε h) under the integral at ε = 0 gives the first variation ∫_a^b (∂L/∂x · h + ∂L/∂x' · h') dt, which vanishes for all such h since x is a variational extremum. Integrate the second term by parts; the boundary terms vanish because h is compactly supported in (a, b), leaving ∫_a^b (∂L/∂x − d/dt(∂L/∂x')) h dt = 0 for all h. By the fundamental lemma of the calculus of variations the continuous factor ∂L/∂x − d/dt(∂L/∂x') is identically zero on (a, b), which is the Euler–Lagrange equation. C² regularity of L and x makes ∂L/∂x' differentiable in t so the integration by parts and the d/dt term are justified.

theorem declaration uses `sorry`euler_lagrange_equation {a b : ℝ} (L : ℝ → ℝ → ℝ → ℝ) (x : ℝ → ℝ) (_hab : a < b)
    (_hL : ContDiff ℝ 2 (fun p : ℝ × ℝ × ℝ => L p.1 p.2.1 p.2.2))
    (_hx : ContDiff ℝ 2 x)
    (_hxe : LeanEval.Analysis.IsVariationalExtremum a b L x) :
    ∀ t ∈ Set.Ioo a b,
      lagrangianPartialX L x t = deriv (lagrangianPartialV L x) t := bya:ℝb:ℝL:ℝ → ℝ → ℝ → ℝx:ℝ → ℝ_hab:a < b_hL:ContDiff ℝ 2 fun p => L p.1 p.2.1 p.2.2_hx:ContDiff ℝ 2 x_hxe:IsVariationalExtremum a b L x⊢ ∀ t ∈ Ioo a b, lagrangianPartialX L x t = deriv (lagrangianPartialV L x) t
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 2, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 2, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026