English
The nonnegative norm of x equals the supremum over all places w of the local norm at w, paired with its nonnegativity proof.
Русский
Неотрицательная норма x равна супремуму по всем местам w локальной нормы в x, с доказательством неотрицательности.
LaTeX
$$$ \|x\|_+ = \sup_{w} \langle \operatorname{normAtPlace}(w, x), \operatorname{normAtPlace\_nonneg}(w, x) \rangle $$$
Lean4
theorem nnnorm_eq_sup_normAtPlace (x : mixedSpace K) :
‖x‖₊ = univ.sup fun w ↦ ⟨normAtPlace w x, normAtPlace_nonneg w x⟩ :=
by
have :
(univ : Finset (InfinitePlace K)) =
(univ.image (fun w : { w : InfinitePlace K // IsReal w } ↦ w.1)) ∪
(univ.image (fun w : { w : InfinitePlace K // IsComplex w } ↦ w.1)) :=
by ext; simp [isReal_or_isComplex]
rw [this, sup_union, univ.sup_image, univ.sup_image, Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]
congr
· ext w
simp [normAtPlace_apply_of_isReal w.prop]
· ext w
simp [normAtPlace_apply_of_isComplex w.prop]
