import Mathlib.Analysis.Complex.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity

/-! Jury (1962): sufficiency of the second-order unit-disk test.
All complex roots of z² + a z + b are handled, including repeated roots.
This is not a formalization of the higher-order Jury table or necessity. -/
namespace PaperToLean.Jury
noncomputable section

theorem real_root_upper (a b x : ℝ) (hb : b < 1) (hp : 0 < 1 + a + b)
    (hx : x ^ 2 + a * x + b = 0) : x < 1 := by
  by_contra h
  have hx1 : 1 ≤ x := le_of_not_gt h
  have hy : 1 < -a - x := by
    by_contra hy
    have hfactor : 0 ≤ 1 + a + x := by linarith
    have hprod := mul_nonneg (sub_nonneg.mpr hx1) hfactor
    nlinarith
  have hprod := mul_nonneg (sub_nonneg.mpr hx1) (show 0 ≤ -a - x by linarith)
  nlinarith

theorem real_root_inside (a b x : ℝ) (hb : b < 1)
    (hp : 0 < 1 + a + b) (hm : 0 < 1 - a + b)
    (hx : x ^ 2 + a * x + b = 0) : -1 < x ∧ x < 1 := by
  have hu := real_root_upper a b x hb hp hx
  have hl := real_root_upper (-a) b (-x) hb (by linarith) (by nlinarith)
  exact ⟨by linarith, hu⟩

theorem root_parts (a b : ℝ) (z : ℂ) (hz : z ^ 2 + (a : ℂ) * z + b = 0) :
    z.re ^ 2 - z.im ^ 2 + a * z.re + b = 0 ∧ z.im * (2 * z.re + a) = 0 := by
  have hr := congrArg Complex.re hz
  have hi := congrArg Complex.im hz
  simp [pow_two] at hr hi
  constructor <;> nlinarith

theorem nonreal_modulus (a b : ℝ) (z : ℂ)
    (hz : z ^ 2 + (a : ℂ) * z + b = 0) (hi : z.im ≠ 0) : Complex.normSq z = b := by
  obtain ⟨hr, him⟩ := root_parts a b z hz
  have ha := (mul_eq_zero.mp him).resolve_left hi
  rw [Complex.normSq_apply]
  nlinarith [congrArg (fun t : ℝ => t * z.re) ha]

/-- The usual three strict inequalities put every root in the open disk. -/
theorem quadratic_sufficient (a b : ℝ) (hb : |b| < 1)
    (hp : 0 < 1 + a + b) (hm : 0 < 1 - a + b) (z : ℂ)
    (hz : z ^ 2 + (a : ℂ) * z + b = 0) : ‖z‖ < 1 := by
  have hb1 : b < 1 := (abs_lt.mp hb).2
  have hnorm : Complex.normSq z < 1 := by
    by_cases hi : z.im = 0
    · have hr := (root_parts a b z hz).1
      rw [hi] at hr
      have h := real_root_inside a b z.re hb1 hp hm (by nlinarith)
      rw [Complex.normSq_apply, hi]
      nlinarith [mul_pos (show 0 < 1 - z.re by linarith) (show 0 < 1 + z.re by linarith)]
    · rw [nonreal_modulus a b z hz hi]
      exact hb1
  rw [Complex.normSq_eq_norm_sq] at hnorm
  nlinarith [norm_nonneg z]

#print axioms real_root_upper
#print axioms real_root_inside
#print axioms root_parts
#print axioms nonreal_modulus
#print axioms quadratic_sufficient
end
end PaperToLean.Jury