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

det_xHessianMatrix2_formula

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)

 100theorem det_xHessianMatrix2_formula (a b x y : ℝ)
 101    (hx : x ≠ 0) (hy : y ≠ 0) :
 102    let R := aggregate (vec2 a b) (vec2 x y)

proof body

Tactic-mode proof.

 103    Matrix.det (xHessianMatrix2 a b x y)
 104      = -(a * b * (R - 1) * (R + 1) * (R ^ 2 * a + R ^ 2 * b - R ^ 2 + a + b + 1))
 105          / (4 * R ^ 2 * x ^ 2 * y ^ 2) := by
 106  dsimp [xHessianMatrix2]
 107  simpa using det_xHessianMatrix2OfR_formula a b x y (aggregate (vec2 a b) (vec2 x y))
 108    hx hy (aggregate_pos (vec2 a b) (vec2 x y)).ne'
 109
 110/-- The neutral locus `aggregate = 1` is a degeneracy locus in the `2 × 2`
 111model. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.