pith. machine review for the scientific record. sign in
theorem proved term proof

xHessianEntry_zero_cost

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

formal statement (Lean)

  55theorem xHessianEntry_zero_cost {n : ℕ} (α x : Vec n) {i j : Fin n}
  56    (hR : aggregate α x = 1) :
  57    xHessianEntry α x i j = xDirection α x i * xDirection α x j := by

proof body

Term-mode proof.

  58  unfold xHessianEntry xDirection xDiagonalCorrection
  59  rw [hR]
  60  by_cases hij : i = j
  61  · simp [hij]
  62  · simp [hij]
  63
  64/-- Two-component vectors written in coordinate order. -/

depends on (5)

Lean names referenced from this declaration's body.