module
module
IndisputableMonolith.Constants.CurvatureCostForm
show as:
view Lean formalization →
used by (1)
depends on (3)
declarations in this module (9)
-
theorem
canonicalDirichletEnergy_constant_zero -
abbrev
boundaryDefectCoefficient -
theorem
boundaryDefectCoefficient_eq_euler_char -
theorem
localJCostHessianCoefficient_eq_one -
def
boundaryCurvatureQuadraticCost -
theorem
boundaryCurvatureQuadraticCost_eq -
theorem
J_curv_eq_boundaryCurvatureQuadraticCost -
structure
CurvatureCostFormCert -
def
curvatureCostFormCert