English
Under the same hypotheses as I, but after passing to the completion of the codomain, the norm equality remains.
Русский
При тех же предпосылках, но после перехода к дополнению кодомического пространства, равенство норм сохраняется.
LaTeX
$$$$\\forall f: \\mathbb{C} \\to F,\\ z: \\mathbb{C},\\ w: \\mathbb{C},\\ hd, hz: \\text{as above},\\ ‖f(w)‖ = ‖f(z)‖.$$$$
Lean4
theorem norm_max_aux₂ {f : ℂ → F} {z w : ℂ} (hd : DiffContOnCl ℂ f (ball z (dist w z)))
(hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z) : ‖f w‖ = ‖f z‖ :=
by
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
have he : ∀ x, ‖e x‖ = ‖x‖ := UniformSpace.Completion.norm_coe
replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z := by
simpa only [IsMaxOn, Function.comp_def, he] using hz
simpa only [he, Function.comp_def] using norm_max_aux₁ (e.differentiable.comp_diffContOnCl hd) hz
