HasVarGradient

📁 Source: PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean

Statistics

Metric	Count
Definitions HasVarGradientAt, varGradient, «termδ(_:=_),∫_,_»,∫_,_»), «termδ_,∫_,_»	4
Theorems add, neg, sum, unique, varGradient	5
Total	9

HasVarGradientAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	HasVarGradientAt	HasVarGradientAt	—	HasVarAdjDerivAt.add
neg 📖	mathematical	HasVarGradientAt	HasVarGradientAt	—	HasVarAdjDerivAt.neg
sum 📖	mathematical	HasVarGradientAt	HasVarGradientAt	—	HasVarAdjDerivAt.const add
unique 📖	—	HasVarGradientAt	—	—	HasVarAdjDerivAt.unique
varGradient 📖	mathematical	HasVarGradientAt	varGradient	—	unique

(root)

Definitions

Name	Category	Theorems
HasVarGradientAt 📖	CompData	7 math math: HasVarGradientAt.neg, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt, Electromagnetism.ElectromagneticPotential.kineticTerm_hasVarGradientAt, HasVarGradientAt.add, HasVarGradientAt.sum, Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_gradLagrangian
varGradient 📖	CompOp	4 math math: ClassicalMechanics.euler_lagrange_varGradient, HasVarGradientAt.varGradient, ClassicalMechanics.hamiltons_equations_varGradient, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae
«termδ(_:=_),∫_,_» 📖,∫_,_» "API Documentation")	CompOp	—
«termδ_,∫_,_» 📖	CompOp	—

---

← Back to Index