English
If p ≠ 0 and a is a root of p, then ‖a‖ < cauchyBound(p).
Русский
Если p ≠ 0 и a является корнем p, то ‖a‖ < cauchyBound(p).
LaTeX
$$$$\|a\|_{+} < \mathrm{cauchyBound}(p)\qquad (p(a)=0,\ p\neq 0).$$$$
Lean4
/-- `cauchyBound` is a bound on the norm of polynomial roots.
-/
theorem norm_lt_cauchyBound {p : K[X]} (hp : p ≠ 0) {a : K} (h : p.IsRoot a) : ‖a‖₊ < cauchyBound p :=
by
rw [IsRoot.def, eval_eq_sum_range, range_add_one] at h
simp only [mem_range, lt_self_iff_false, not_false_eq_true, sum_insert, coeff_natDegree, add_eq_zero_iff_eq_neg] at h
apply_fun nnnorm at h
simp only [nnnorm_mul, nnnorm_pow, nnnorm_neg] at h
suffices ‖a‖₊ ^ p.natDegree ≤ (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
by
rcases eq_or_ne ‖a‖₊ 1 with ha | ha
· simp only [ha, one_pow, sum_const, card_range, nsmul_eq_mul, mul_one, gt_iff_lt] at this ⊢
apply lt_of_le_of_ne (by simp)
intro nh
simp [← nh, tsub_self] at this
rcases lt_or_gt_of_ne ha with ha | ha
· apply ha.trans_le
simp
· rw [geom_sum_of_one_lt ha] at this
calc
‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
_ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field_simp
_ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
gcongr
_ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 :=
by
congr 2
have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
field_simp
_ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 :=
by
gcongr
· apply lt_of_le_of_ne (by simp)
contrapose! this
simp only [← this, zero_mul]
apply pow_pos
exact zero_lt_one.trans ha
simp [zero_lt_one.trans ha]
_ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]
apply le_of_eq at h
have pld : ‖p.leadingCoeff‖₊ ≠ 0 := by simpa
calc
‖a‖₊ ^ p.natDegree
_ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ :=
by
rw [mul_div_cancel_left₀]
simpa
_ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
_ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ :=
by
gcongr
apply nnnorm_sum_le
_ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
_ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ :=
by
gcongr (∑ x ∈ _, ?_ * _) / _
rw [cauchyBound, add_tsub_cancel_right]
field_simp
apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
_ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x :=
by
simp only [← mul_sum]
field_simp
