Theorems · Theorem · complex analysis
Complex.norm_eq_norm_of_isMaxOn_of_ball_subset
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F} {s : Set E} {z w : E},
DiffContOnCl ℂ f s → IsMaxOn (norm ∘ f) s z → Metric.ball z (dist w z) ⊆ s → ‖f w‖ = ‖f z‖Maximum modulus principle: if f : E → F is complex differentiable on a set s, the norm
of f takes it maximum on s at z, and w is a point such that the closed ball with center z
and radius dist w z is included in s, then ‖f w‖ = ‖f z‖.
- Defined in
- Mathlib.Analysis.Complex.AbsMax
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Complexstatement and proof · cited by 5,565
- Norm.normstatement and proof · cited by 5,413
- le_rflproof · cited by 1,558
- Dist.diststatement and proof · cited by 1,539
- Metric.ballstatement and proof · cited by 735
- IsMaxOnstatement and proof · cited by 114
- DiffContOnClstatement and proof · cited by 92
- Metric.mem_closedBallproof · cited by 42
Cited by3
Results whose statement or proof uses this declaration.
- PhragmenLindelof.right_half_plane_of_tendsto_zero_on_realproof · cited by 2
- Complex.exists_mem_frontier_isMaxOn_normproof · cited by 1
- Complex.eq_of_isMaxOn_of_ball_subsetproof · cited by 1