English
Let U be a bounded subset of a normed complex space, and f: E → F be complex-differentiable on U. If there exists a bound C such that ‖f(z)‖ ≤ C for every z on the boundary of U (frontier U), then the same bound holds on the closure of U, i.e., for every z in closure(U) we have ‖f(z)‖ ≤ C.
Русский
Пусть U — ограниченная подмножество норми ⁿой комплексной пространства, и f: E → F комплексно дифференцируема на U. Если существует предел C такой, что ‖f(z)‖ ≤ C для каждого z на границе U, то не менее она сохраняется и на замыкании U: для каждого z в closure(U) выполняется ‖f(z)‖ ≤ C.
LaTeX
$$$$\forall f: E \to F, \forall U \subset E, \bigl( \operatorname{IsBounded}(U) \land \operatorname{DiffContOnCl}(\mathbb{C}, f, U) \land \exists C \in \mathbb{R}, \forall z \in \partial U, \|f(z)\| \le C \bigr) \Rightarrow \forall z \in \overline{U}, \|f(z)\| \le C.$$$$
Lean4
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a bounded set `U` and
`‖f z‖ ≤ C` for any `z ∈ frontier U`, then the same is true for any `z ∈ closure U`. -/
theorem norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : Set E} (hU : IsBounded U) (hd : DiffContOnCl ℂ f U)
{C : ℝ} (hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C) {z : E} (hz : z ∈ closure U) : ‖f z‖ ≤ C :=
by
rw [closure_eq_self_union_frontier, union_comm, mem_union] at hz
rcases hz with hz | hz; · exact hC z hz
rcases exists_ne z with ⟨w, hne⟩
set e := (lineMap z w : ℂ → E)
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
have hL : AntilipschitzWith (nndist z w)⁻¹ e := antilipschitzWith_lineMap hne.symm
replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U) := hd.comp hde.diffContOnCl (mapsTo_preimage _ _)
have h₀ : (0 : ℂ) ∈ e ⁻¹' U := by simpa only [e, mem_preimage, lineMap_apply_zero]
rcases exists_mem_frontier_isMaxOn_norm (hL.isBounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩
calc
‖f z‖ = ‖f (e 0)‖ := by simp only [e, lineMap_apply_zero]
_ ≤ ‖f (e ζ)‖ := (hζ (subset_closure h₀))
_ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)
