EulerLagrange

📁 Source: PhysLean/ClassicalMechanics/EulerLagrange.lean

Statistics

Metric	Count
Definitions eulerLagrangeOp	1
Theorems eulerLagrangeOp_eq, eulerLagrangeOp_zero, euler_lagrange_varGradient	3
Total	4

ClassicalMechanics

Definitions

Name	Category	Theorems
eulerLagrangeOp 📖	CompOp	4 math math: euler_lagrange_varGradient, eulerLagrangeOp_zero, eulerLagrangeOp_eq, HarmonicOscillator.gradLagrangian_eq_eulerLagrangeOp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eulerLagrangeOp_eq 📖	mathematical	—	eulerLagrangeOp Time.deriv	—	—
eulerLagrangeOp_zero 📖	mathematical	—	eulerLagrangeOp	—	eulerLagrangeOp_eq
euler_lagrange_varGradient 📖	mathematical	Time Time.instNormedAddCommGroup Time.instNormedSpaceReal	varGradient Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace instInnerProductSpace' Time.instSeminormedAddCommGroup Time.instAddCommGroup Time.instModuleReal Time.instOfNat eulerLagrangeOp	—	Time.instFiniteDimensionalReal Time.instBorelSpace eulerLagrangeOp_eq HasVarGradientAt.varGradient HasVarAdjDerivAt.comp HasVarAdjDerivAt.fmap DifferentiableAt.hasAdjFDerivAt HasVarAdjDerivAt.prod HasVarAdjDerivAt.id HasVarAdjDerivAt.fderiv gradient_eq_adjFDeriv adjFDeriv_uncurry

---

← Back to Index