English
For a CM-field K and any x ∈ K, the norm bound ‖canonicalEmbedding K x‖ ≤ r holds iff every embedding φ satisfies ‖φ x‖ ≤ r.
Русский
Для поля CM и любого x ∈ K выполняется неравенство ‖canonicalEmbedding K x‖ ≤ r тогда и только тогда, когда для каждого вложения φ выполняется ‖φ x‖ ≤ r.
LaTeX
$$$\\|\\mathrm{canonicalEmbedding}(K)(x)\\| \\le r \\iff \\forall \\phi:K\\to\\mathbb{C},\\; \\|\\phi(x)\\| \\le r$$$
Lean4
theorem norm_le_iff [NumberField K] (x : K) (r : ℝ) : ‖canonicalEmbedding K x‖ ≤ r ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r :=
by
obtain hr | hr := lt_or_ge r 0
· obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))
refine iff_of_false ?_ ?_
· exact (hr.trans_le (norm_nonneg _)).not_ge
· exact fun h => hr.not_ge (le_trans (norm_nonneg _) (h φ))
· lift r to NNReal using hr
simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ, forall_true_left]
