English
Under the existing hypotheses, there exists a point on the frontier where the maximum of the norm on closure is attained.
Русский
При существующих предположениях существует точка на границе, где достигается максимум нормы на closure.
LaTeX
$$$$\\exists z \\in \\mathrm{frontier}(U),\\ IsMaxOn (\\|f\\|) (\\overline{U}) z.$$$$
Lean4
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a nonempty bounded
set `U` and is continuous on its closure, then there exists a point `z ∈ frontier U` such that
`(‖f ·‖)` takes it maximum value on `closure U` at `z`. -/
theorem exists_mem_frontier_isMaxOn_norm [FiniteDimensional ℂ E] {f : E → F} {U : Set E} (hb : IsBounded U)
(hne : U.Nonempty) (hd : DiffContOnCl ℂ f U) : ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z :=
by
have hc : IsCompact (closure U) := hb.isCompact_closure
obtain ⟨w, hwU, hle⟩ : ∃ w ∈ closure U, IsMaxOn (norm ∘ f) (closure U) w :=
hc.exists_isMaxOn hne.closure hd.continuousOn.norm
rw [closure_eq_interior_union_frontier, mem_union] at hwU
rcases hwU with hwU | hwU; rotate_left; · exact ⟨w, hwU, hle⟩
have : interior U ≠ univ := ne_top_of_le_ne_top hc.ne_univ interior_subset_closure
rcases exists_mem_frontier_infDist_compl_eq_dist hwU this with ⟨z, hzU, hzw⟩
refine ⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq ?_⟩
refine (norm_eq_norm_of_isMaxOn_of_ball_subset hd (hle.on_subset subset_closure) ?_).symm
rw [dist_comm, ← hzw]
exact ball_infDist_compl_subset.trans interior_subset
