Theorems · Theorem · complex analysis

Complex.norm_le_of_forall_mem_frontier_norm_le

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f : E → F} {U : Set E},
  Bornology.IsBounded U →
    DiffContOnCl ℂ f U → ∀ {C : ℝ}, (∀ z ∈ frontier U, ‖f z‖ ≤ C) → ∀ {z : E}, z ∈ closure U → ‖f z‖ ≤ C

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.

Defined in

Mathlib.Analysis.Complex.AbsMax

Cited by

2 results in Mathlib

Foundations

Depth 290 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNontrivial