1. PhyslibAlpha
  2. ClassicalFieldTheory
  3. Local
  4. FirstVariation
  5. Criterion
Imports
/- Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Juan Jose Fernandez Morales -/ module public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Density public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.IntegrationByParts public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Regularity

First variation criteria

i. Overview

This module assembles the analytic ingredients of the local first-variation proof into the packaged first-variation formula and the internal Euler-Lagrange criteria used by the public facade.

ii. Key results

    ClassicalFieldTheory.Local. isCritical_iff_eulerLagrange_zero_of_hasFiniteAction_and_continuousInCoordinates

iii. Table of contents

    A. First-variation assembly

    B. Final Euler-Lagrange criterion

iv. References

    J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5, Theorem 5.2.

@[expose] public section

A. First-variation assembly

Explicit global finiteness hypothesis for all admissible variations.

def AllVariationsHaveFiniteAction (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop := ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), HasFiniteActionVariation L f η

The first-variation formula for the local action, packaged as a reusable hypothesis.

def HasFirstVariationFormula (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop := ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), HasFiniteActionVariation L f η → HasDerivAt (actionVariation L f η) (firstVariationValue L f η) 0
d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhEuler:eulerLagrangeOp L f = 0η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηhderiv:HasDerivAt (actionVariation L f η) 0 0hzero:firstVariationValue L f η = 0⊢ HasDerivAt (actionVariation L f η) 0 0 All goals completed! 🐙lemma eulerLagrange_zero_of_isCritical (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hfirst : HasFirstVariationFormula L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) (hcrit : IsCritical L f) : eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L f⊢ eulerLagrangeOp L f = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L f⊢ Continuous (eulerLagrangeOp L f)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L f⊢ ∀ (g : Space d → EuclideanSpace ℝ (Fin m)), IsTestFunction g → ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L f⊢ Continuous (eulerLagrangeOp L f) All goals completed! 🐙 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L f⊢ ∀ (g : Space d → EuclideanSpace ℝ (Fin m)), IsTestFunction g → ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L fg:Space d → EuclideanSpace ℝ (Fin m)hg:IsTestFunction g⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L fg:Space d → EuclideanSpace ℝ (Fin m)hg:IsTestFunction gη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m)) := { toFun := g, isTestFunction := hg }⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L fg:Space d → EuclideanSpace ℝ (Fin m)hg:IsTestFunction gη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m)) := { toFun := g, isTestFunction := hg }hηfin:HasFiniteActionVariation L f η⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L fg:Space d → EuclideanSpace ℝ (Fin m)hg:IsTestFunction gη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m)) := { toFun := g, isTestFunction := hg }hηfin:HasFiniteActionVariation L f ηhfirstη:HasDerivAt (actionVariation L f η) (firstVariationValue L f η) 0⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L fg:Space d → EuclideanSpace ℝ (Fin m)hg:IsTestFunction gη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m)) := { toFun := g, isTestFunction := hg }hηfin:HasFiniteActionVariation L f ηhfirstη:HasDerivAt (actionVariation L f η) (firstVariationValue L f η) 0hcritη:HasDerivAt (actionVariation L f η) 0 0⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcrit:IsCritical L fg:Space d → EuclideanSpace ℝ (Fin m)hg:IsTestFunction gη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m)) := { toFun := g, isTestFunction := hg }hηfin:HasFiniteActionVariation L f ηhfirstη:HasDerivAt (actionVariation L f η) (firstVariationValue L f η) 0hcritη:HasDerivAt (actionVariation L f η) 0 0hzero:firstVariationValue L f η = 0⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, g x⟫_ℝ = 0 All goals completed! 🐙theorem isCritical_iff_eulerLagrange_zero (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hfirst : HasFirstVariationFormula L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f → eulerLagrangeOp L f = 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ eulerLagrangeOp L f = 0 → IsCritical L f d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f → eulerLagrangeOp L f = 0 All goals completed! 🐙 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hfirst:HasFirstVariationFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ eulerLagrangeOp L f = 0 → IsCritical L f All goals completed! 🐙d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hint:HasActionVariationDerivativeUnderIntegral L fhpoint:HasPointwiseLinearizedDensityFormula L fhibp:HasIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηhderiv:HasDerivAt (actionVariation L f η) (firstVariationValue L f η) 0hlinearized:∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0 = ∫ (x : Space d), firstVariationDensity L f η xhvalue:∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0 = firstVariationValue L f η⊢ HasDerivAt (actionVariation L f η) (firstVariationValue L f η) 0 All goals completed! 🐙private lemma hasFirstVariationFormula_of_contDiff_underIntegral_and_parts (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hint : HasActionVariationDerivativeUnderIntegral L f) (hibp : HasIntegratedByPartsFormula L f) : HasFirstVariationFormula L f := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhint:HasActionVariationDerivativeUnderIntegral L fhibp:HasIntegratedByPartsFormula L f⊢ HasFirstVariationFormula L f All goals completed! 🐙private lemma hasFirstVariationFormula_of_underIntegral_linearized_and_termwise (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hint : HasActionVariationDerivativeUnderIntegral L f) (hpoint : HasPointwiseLinearizedDensityFormula L f) (hterm : HasTermwiseIntegratedByPartsFormula L f) : HasFirstVariationFormula L f := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hint:HasActionVariationDerivativeUnderIntegral L fhpoint:HasPointwiseLinearizedDensityFormula L fhterm:HasTermwiseIntegratedByPartsFormula L f⊢ HasFirstVariationFormula L f All goals completed! 🐙private lemma hasFirstVariationFormula_of_contDiff_underIntegral_and_termwise (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hint : HasActionVariationDerivativeUnderIntegral L f) (hterm : HasTermwiseIntegratedByPartsFormula L f) : HasFirstVariationFormula L f := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhint:HasActionVariationDerivativeUnderIntegral L fhterm:HasTermwiseIntegratedByPartsFormula L f⊢ HasFirstVariationFormula L f All goals completed! 🐙

B. Intermediate Euler-Lagrange criteria

The local Euler-Lagrange criterion obtained from the packaged analytic ingredients of the first-variation formula. This is the current formalized form of Theorem 5.2.

private theorem isCritical_iff_eulerLagrange_zero_of_underIntegral_linearized_and_parts (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hint : HasActionVariationDerivativeUnderIntegral L f) (hpoint : HasPointwiseLinearizedDensityFormula L f) (hibp : HasIntegratedByPartsFormula L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hint:HasActionVariationDerivativeUnderIntegral L fhpoint:HasPointwiseLinearizedDensityFormula L fhibp:HasIntegratedByPartsFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙

Variant of the local Euler-Lagrange criterion where the integration-by-parts input is reduced to a termwise hypothesis.

private theorem isCritical_iff_eulerLagrange_zero_of_underIntegral_linearized_and_termwise (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hint : HasActionVariationDerivativeUnderIntegral L f) (hpoint : HasPointwiseLinearizedDensityFormula L f) (hterm : HasTermwiseIntegratedByPartsFormula L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hint:HasActionVariationDerivativeUnderIntegral L fhpoint:HasPointwiseLinearizedDensityFormula L fhterm:HasTermwiseIntegratedByPartsFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙
private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_underIntegral_and_termwise (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hint : HasActionVariationDerivativeUnderIntegral L f) (hterm : HasTermwiseIntegratedByPartsFormula L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhint:HasActionVariationDerivativeUnderIntegral L fhterm:HasTermwiseIntegratedByPartsFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_continuous_coordDeriv_and_termwise (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hcontVar : ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), ∀ I : DerivativeIndex d k, ∀ a : Fin m, Continuous (fun p : ℝ × Space d => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2))) (hterm : HasTermwiseIntegratedByPartsFormula L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)hterm:HasTermwiseIntegratedByPartsFormula L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_regular (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hcontVar : ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), Lagrangian.ContinuousCoordDerivAlongFamily L (fun s : ℝ => variedField f η s)) (hcoeff : Lagrangian.ContDiffCoordDerivAlongField L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), L.ContinuousCoordDerivAlongFamily fun s => variedField f η shcoeff:L.ContDiffCoordDerivAlongField fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_regularityAt (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hreg : HasEulerLagrangeRegularityAt L f) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhreg:HasEulerLagrangeRegularityAt L fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)hcoeff:L.ContDiffCoordDerivAlongField fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), L.ContinuousCoordDerivAlongFamily fun s => variedField f η s⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_smoothRegularity (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hreg : HasSmoothEulerLagrangeRegularity L) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhreg:HasSmoothEulerLagrangeRegularity Lhfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_coordinateRegularity (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hcoord : Lagrangian.ContDiffCoordDerivInCoordinates L) (hfin : AllVariationsHaveFiniteAction L f) (hcont : Continuous (eulerLagrangeOp L f)) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcoord:L.ContDiffCoordDerivInCoordinateshfin:AllVariationsHaveFiniteAction L fhcont:Continuous (eulerLagrangeOp L f)⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_regularityAt' (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hreg : HasEulerLagrangeRegularityAt L f) (hfin : AllVariationsHaveFiniteAction L f) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhreg:HasEulerLagrangeRegularityAt L fhfin:AllVariationsHaveFiniteAction L f⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhfin:AllVariationsHaveFiniteAction L fhcoeff:L.ContDiffCoordDerivAlongField fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), L.ContinuousCoordDerivAlongFamily fun s => variedField f η s⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_smoothRegularity' (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hreg : HasSmoothEulerLagrangeRegularity L) (hfin : AllVariationsHaveFiniteAction L f) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhreg:HasSmoothEulerLagrangeRegularity Lhfin:AllVariationsHaveFiniteAction L f⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙private theorem isCritical_iff_eulerLagrange_zero_of_contDiff_and_coordinateRegularity' (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hcoord : Lagrangian.ContDiffCoordDerivInCoordinates L) (hfin : AllVariationsHaveFiniteAction L f) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcoord:L.ContDiffCoordDerivInCoordinateshfin:AllVariationsHaveFiniteAction L f⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcoord:L.ContDiffCoordDerivInCoordinateshbase:HasFiniteAction L fhlocal:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), HasCompactlySupportedActionVariationDifference L f ηhfin:AllVariationsHaveFiniteAction L f⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙theorem isCritical_iff_eulerLagrange_zero_of_hasFiniteAction_and_continuousInCoordinates (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) (hcoord : Lagrangian.ContDiffCoordDerivInCoordinates L) (hcontL : Lagrangian.ContinuousInCoordinates L) (hbase : HasFiniteAction L f) : IsCritical L f ↔ eulerLagrangeOp L f = 0 := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcoord:L.ContDiffCoordDerivInCoordinateshcontL:L.ContinuousInCoordinateshbase:HasFiniteAction L f⊢ IsCritical L f ↔ eulerLagrangeOp L f = 0 All goals completed! 🐙