module module

`IndisputableMonolith.Cost.Ndim.XCoordinates`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.Ndim.Core module_import

declarations in this module (15)

def xDirection L23
def xDiagonalCorrection L27
def xHessianEntry L31
def xHessianMatrix L36
theorem xHessianEntry_offDiag L39
theorem xHessianEntry_diag L45
theorem xHessianEntry_zero_cost L55
abbrev vec2 L65
def xHessianMatrix2OfR L69
def xHessianMatrix2 L79
theorem xHessianMatrix2_eq_general L82
theorem det_xHessianMatrix2OfR_formula L91
theorem det_xHessianMatrix2_formula L100
theorem det_xHessianMatrix2_zero_cost L112
theorem det_xHessianMatrix2_ne_zero_of_generic L121