det_xHessianMatrix2_formula

formal source

  97  field_simp [hx, hy, hR]
  98  ring
  99
 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)
 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. -/
 112theorem det_xHessianMatrix2_zero_cost (a b x y : ℝ)
 113    (hx : x ≠ 0) (hy : y ≠ 0)
 114    (hR : aggregate (vec2 a b) (vec2 x y) = 1) :
 115    Matrix.det (xHessianMatrix2 a b x y) = 0 := by
 116  rw [det_xHessianMatrix2_formula a b x y hx hy]
 117  simp [hR]
 118
 119/-- Away from the neutral locus and the secondary discriminant factor, the
 120`2 × 2` `x`-coordinate Hessian is nondegenerate. -/
 121theorem det_xHessianMatrix2_ne_zero_of_generic (a b x y : ℝ)
 122    (hx : x ≠ 0) (hy : y ≠ 0)
 123    (ha : a ≠ 0) (hb : b ≠ 0)
 124    (hR1 : aggregate (vec2 a b) (vec2 x y) ≠ 1)
 125    (hdisc :
 126      (aggregate (vec2 a b) (vec2 x y)) ^ 2 * a
 127        + (aggregate (vec2 a b) (vec2 x y)) ^ 2 * b
 128        - (aggregate (vec2 a b) (vec2 x y)) ^ 2
 129        + a + b + 1 ≠ 0) :
 130    Matrix.det (xHessianMatrix2 a b x y) ≠ 0 := by