Documentation Verification Report

HamiltonsEquations

📁 Source: PhysLean/ClassicalMechanics/HamiltonsEquations.lean

Statistics

Metric	Count
Definitions `hamiltonEqOp`	1
Theorems `hamiltonEqOp_eq`, `hamiltonEqOp_eq_zero_iff_hamiltons_equations`, `hamiltons_equations_varGradient`	3
Total	4

ClassicalMechanics

Definitions

Name	Category	Theorems
`hamiltonEqOp` 📖	CompOp	3 math math: `hamiltonEqOp_eq`, `hamiltonEqOp_eq_zero_iff_hamiltons_equations`, `hamiltons_equations_varGradient`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hamiltonEqOp_eq` 📖	mathematical	—	`hamiltonEqOp` `Time.deriv`	—	—
`hamiltonEqOp_eq_zero_iff_hamiltons_equations` 📖	mathematical	—	`hamiltonEqOp` `Time` `Time.deriv`	—	`hamiltonEqOp_eq`
`hamiltons_equations_varGradient` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`varGradient` `Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Time.instInnerProductSpaceReal` `Time.instFiniteDimensionalReal` `Time.instMeasurableSpace` `Time.instBorelSpace` `instInnerProductSpace'Prod` `instInnerProductSpace'` `instInnerOfInnerProductSpace'` `Time.deriv` `hamiltonEqOp`	—	`HasVarGradientAt.varGradient` `Time.instFiniteDimensionalReal` `Time.instBorelSpace` `HasVarAdjDerivAt.add` `HasVarAdjDerivAt.comp` `HasVarAdjDerivAt.fmap` `ContDiff.inner'` `DifferentiableAt.hasAdjFDerivAt` `DifferentiableAt.inner'` `HasVarAdjDerivAt.prod` `HasVarAdjDerivAt.fst` `HasVarAdjDerivAt.id` `HasVarAdjDerivAt.fderiv'` `HasVarAdjDerivAt.neg` `adjFDeriv_prod_snd` `adjFDeriv_uncurry` `adjFDeriv_inner` `gradient_eq_adjFDeriv`

---

← Back to Index