det_xHessianMatrix2_zero_cost

formal source

 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
 131  let R := aggregate (vec2 a b) (vec2 x y)
 132  have hR : R ≠ 0 := (aggregate_pos (vec2 a b) (vec2 x y)).ne'
 133  have hRp1 : R + 1 ≠ 0 := by
 134    have hpos : 0 < R := by simp [R]
 135    linarith
 136  have hden : 4 * R ^ 2 * x ^ 2 * y ^ 2 ≠ 0 := by
 137    have hR2 : R ^ 2 ≠ 0 := pow_ne_zero 2 hR
 138    have hx2 : x ^ 2 ≠ 0 := pow_ne_zero 2 hx
 139    have hy2 : y ^ 2 ≠ 0 := pow_ne_zero 2 hy
 140    have h4R : 4 * R ^ 2 ≠ 0 := mul_ne_zero (by norm_num) hR2
 141    have h4Rx : 4 * R ^ 2 * x ^ 2 ≠ 0 := mul_ne_zero h4R hx2
 142    exact mul_ne_zero h4Rx hy2