noncomputable def EllipsoidMethod.Ellipsoid {n : ℕ} (D : Matrix (Fin n) (Fin n) ℝ) (z : Fin n → ℝ) : Set (Fin n → ℝ)

noncomputable def EllipsoidMethod.updateMatrix {n : ℕ} (D : Matrix (Fin n) (Fin n) ℝ) (a : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

theorem EllipsoidMethod.quadForm_pos {n : ℕ} (D : Matrix (Fin n) (Fin n) ℝ) (hD : D.PosDef) (a : Fin n → ℝ) (ha : a ≠ 0) : 0 < a ⬝ᵥ D.mulVec a

theorem EllipsoidMethod.det_sub_smul_vecMulVec_of_isUnit {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : IsUnit A.det) (t : ℝ) (u v : Fin n → ℝ) : (A - t • Matrix.vecMulVec u v).det = A.det * (1 - t * v ⬝ᵥ A⁻¹.mulVec u)

theorem EllipsoidMethod.updateMatrix_det_ratio {n : ℕ} (hn : 1 < n) (D : Matrix (Fin n) (Fin n) ℝ) (hD : D.PosDef) (a : Fin n → ℝ) (ha : a ≠ 0) : (updateMatrix D a).det / D.det = (↑n ^ 2 / (↑n ^ 2 - 1)) ^ n * ((↑n - 1) / (↑n + 1))

theorem EllipsoidMethod.volume_ratio_numerical_bound {n : ℕ} (hn : 1 < n) : (↑n ^ 2 / (↑n ^ 2 - 1)) ^ n * ((↑n - 1) / (↑n + 1)) ≤ Real.exp (-1 / (↑n + 1))

theorem EllipsoidMethod.ellipsoid_volume_ratio_le_exp {n : ℕ} (hn : 1 < n) (D : Matrix (Fin n) (Fin n) ℝ) (hD : D.PosDef) (a : Fin n → ℝ) (ha : a ≠ 0) : ((updateMatrix D a).det / D.det) ^ (1 / 2) ≤ Real.exp (-1 / (2 * (↑n + 1)))