English
For the monomial X^n, spectralValue is 0.
Русский
У монома X^n спектральное значение равно 0.
LaTeX
$$$$\operatorname{spectralValue}(X^{n}) = 0.$$$$
Lean4
/-- The norm of any root of `p` is bounded by the spectral value of `p`. See
[S. Bosch, U. Güntzer, R. Remmert, *Non-Archimedean Analysis* (Proposition 3.1.2/1(1))]
[bosch-guntzer-remmert]. -/
theorem norm_root_le_spectralValue {f : AlgebraNorm K L} (hf_pm : IsPowMul f) (hf_na : IsNonarchimedean f) {p : K[X]}
(hp : p.Monic) {x : L} (hx : aeval x p = 0) : f x ≤ spectralValue p :=
by
by_cases hx0 : f x = 0
· rw [hx0]; exact spectralValue_nonneg p
· by_contra h_ge
have hn_lt : ∀ (n : ℕ) (_ : n < p.natDegree), ‖p.coeff n‖ < f x ^ (p.natDegree - n) :=
by
intro n hn
have hexp : (‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖ := by
rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _), rpow_natCast, ←
cast_sub (le_of_lt hn), one_div, pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
have h_base : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) < f x :=
by
rw [spectralValue, iSup, not_le,
Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
(Set.range_nonempty (spectralValueTerms p))] at h_ge
have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈ Set.range (spectralValueTerms p) := by use n;
simp only [spectralValueTerms, if_pos hn]
exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg
rw [← hexp, ← rpow_natCast, ← rpow_natCast]
exact rpow_lt_rpow (rpow_nonneg (norm_nonneg _) _) h_base (cast_pos.mpr (tsub_pos_of_lt hn))
have h_deg : 0 < p.natDegree := natDegree_pos_of_monic_of_aeval_eq_zero hp hx
have h_lt : f ((Finset.range p.natDegree).sum fun i : ℕ ↦ p.coeff i • x ^ i) < f (x ^ p.natDegree) :=
by
have hn' : ∀ (n : ℕ) (_ : n < p.natDegree), f (p.coeff n • x ^ n) < f (x ^ p.natDegree) :=
by
intro n hn
by_cases hn0 : n = 0
· rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg), ← Nat.sub_zero p.natDegree, ← hn0]
exact (mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)
· have : p.natDegree = p.natDegree - n + n := by rw [Nat.sub_add_cancel (le_of_lt hn)]
rw [map_smul_eq_mul, hf_pm _ (succ_le_iff.mp (pos_iff_ne_zero.mpr hn0)), hf_pm _ (succ_le_iff.mpr h_deg),
this, pow_add]
gcongr
exact hn_lt n hn
set g := fun i : ℕ ↦ p.coeff i • x ^ i
obtain ⟨m, hm_in, hm⟩ :
∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree), f ((Finset.range p.natDegree).sum g) ≤ f (g m) :=
by
obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add hf_na g (Finset.range p.natDegree)
rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
exact ⟨m, hm, h⟩
exact lt_of_le_of_lt hm (hn' m (hm_in h_deg))
have h0 : f 0 ≠ 0 :=
by
have h_eq : f 0 = f (x ^ p.natDegree) :=
by
rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree, one_smul, ←
max_eq_left_of_lt h_lt]
exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)
exact h_eq ▸ ne_of_gt (lt_of_le_of_lt (apply_nonneg _ _) h_lt)
exact h0 (map_zero _)
