Separating radii by norms of a nontrivially normed field, and solving norm equations

In a nontrivially normed field 𝕜 the norms need not be dense, so two radii 0 < r < s need not be separated by the norm of an element of 𝕜. They are separated after raising to a power: NormedField.exists_pow_lt_norm_lt_pow gives m : ℕ and c : 𝕜 with rᵐ < ‖c‖ < sᵐ. Compare NormedField.exists_lt_norm_lt, which separates the radii themselves in a densely normed field. Over an algebraically closed field m-th roots exist, so the radii themselves are separated: NormedField.exists_lt_norm_lt_of_isAlgClosed. Iterating, the norms of a sequence decrease strictly inside any interval (r, s): NormedField.exists_strictAnti_norm_mem_Ioo_of_isAlgClosed. If instead the norms accumulate at 1, then for r < 1 and any n some ϖ with ‖ϖ‖ < 1 has r < ‖ϖ‖ ^ n: NormedField.exists_lt_norm_pow_of_forall_exists_one_lt_norm_lt.

The same roots solve norm equations: over an algebraically closed normed field, for a multiset s containing 0 and any c, some d has ∏_{a ∈ s} max ‖d‖ ‖a‖ = ‖c‖ (NormedField.exists_prod_map_max_norm_eq_of_isAlgClosed). For a nonarchimedean norm the left side is the Gauss norm at radius ‖d‖ of the polynomial with roots s, so ‖d‖ is a radius at which that Gauss norm equals ‖c‖.

A normed field whose norm takes every positive real value is densely normed (DenselyNormedField.ofForallExistsNormEq).

Finally, TauCeti.norm_sub_div_le_of_dist_div_le turns a bound on the ratio F / w near c⁻¹ into a relative error bound for F - w / c.

theorem NormedField.exists_pow_lt_norm_lt_pow (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {r s : ℝ} (hr₀ : 0 < r) (hlt : r < s) : ∃ (m : ℕ) (c : 𝕜), r ^ m < ‖c‖ ∧ ‖c‖ < s ^ m

Two radii 0 < r < s are separated by a norm after raising to a power: there are m : ℕ and c : 𝕜 with rᵐ < ‖c‖ < sᵐ.

theorem NormedField.exists_lt_norm_lt_of_isAlgClosed (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] [IsAlgClosed 𝕜] {r s : ℝ} (hr₀ : 0 ≤ r) (hlt : r < s) : ∃ (c : 𝕜), r < ‖c‖ ∧ ‖c‖ < s

The norms of an algebraically closed nontrivially normed field are dense: two radii 0 ≤ r < s are separated by the norm of an element. This is the conclusion of NormedField.exists_lt_norm_lt without a DenselyNormedField instance.

theorem NormedField.exists_strictAnti_norm_mem_Ioo_of_isAlgClosed (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] [IsAlgClosed 𝕜] {r s : ℝ} (hr₀ : 0 ≤ r) (hlt : r < s) : ∃ (c : ℕ → 𝕜), (StrictAnti fun (n : ℕ) => ‖c n‖) ∧ ∀ (n : ℕ), ‖c n‖ ∈ Set.Ioo r s

The norms of an algebraically closed nontrivially normed field contain a strictly decreasing sequence in any interval (r, s) with 0 ≤ r < s.

theorem NormedField.exists_lt_norm_pow_of_forall_exists_one_lt_norm_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (hacc : ∀ (ε : ℝ), 1 < ε → ∃ (x : 𝕜), 1 < ‖x‖ ∧ ‖x‖ < ε) {r : ℝ} (hr : r < 1) (n : ℕ) : ∃ (ϖ : 𝕜), 0 < ‖ϖ‖ ∧ ‖ϖ‖ < 1 ∧ r < ‖ϖ‖ ^ n

If the norms of 𝕜 accumulate at 1, some element of norm less than one has n-th power of norm above any r < 1: for every n some ϖ with 0 < ‖ϖ‖ < 1 has r < ‖ϖ‖ ^ n.

theorem NormedField.exists_prod_map_max_norm_eq_of_isAlgClosed {𝕜 : Type u_2} [NormedField 𝕜] [IsAlgClosed 𝕜] {s : Multiset 𝕜} (hs : 0 ∈ s) (c : 𝕜) : ∃ (d : 𝕜), (Multiset.map (fun (a : 𝕜) => max ‖d‖ ‖a‖) s).prod = ‖c‖

Solving ∏_{a ∈ s} max ‖d‖ ‖a‖ = ‖c‖ over an algebraically closed field: if 0 ∈ s, then for every c some d satisfies this equation. For a nonarchimedean norm its left side is the Gauss norm at radius ‖d‖ of the polynomial ∏_{a ∈ s} (T - a), so ‖d‖ is a radius at which that Gauss norm equals ‖c‖.

@[instance_reducible]

def DenselyNormedField.ofForallExistsNormEq {𝕜 : Type u_1} [h' : NormedField 𝕜] (h : ∀ (r : ℝ), 0 < r → ∃ (x : 𝕜), ‖x‖ = r) : DenselyNormedField 𝕜

A normed field whose norm takes every positive real value is densely normed. The underlying normed field is the given one, so that over a NontriviallyNormedField this structure induces the original NontriviallyNormedField up to structure eta.

theorem TauCeti.norm_sub_div_le_of_dist_div_le {𝕜 : Type u_1} [NormedField 𝕜] {F w c : 𝕜} {η : ℝ} (hw : w ≠ 0) (h : dist (F / w) c⁻¹ ≤ η / ‖c‖) : ‖F - w / c‖ ≤ η * ‖w / c‖

A bound on the ratio F / w near c⁻¹ is a relative error bound for w / c: if dist (F / w) c⁻¹ ≤ η / ‖c‖ and w ≠ 0, then ‖F - w / c‖ ≤ η * ‖w / c‖.