theorem
proved
tactic proof
det_xHessianMatrix2_ne_zero_of_generic
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
143 rw [det_xHessianMatrix2_formula a b x y hx hy]
144 refine div_ne_zero ?_ hden
145 refine neg_ne_zero.mpr ?_
146 refine mul_ne_zero ?_ hdisc
147 refine mul_ne_zero ?_ hRp1
148 refine mul_ne_zero ?_ (sub_ne_zero.mpr hR1)
149 exact mul_ne_zero ha hb
150
151end Ndim
152end Cost
153end IndisputableMonolith