Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-27 22:00 7f52f94a

View on Github →

feat(analysis/complex): maximum modulus principle (#12050)

Estimated changes

Created src/analysis/complex/abs_max.lean

added theorem complex.eq_on_of_eq_on_frontier

added theorem complex.exists_mem_frontier_is_max_on_norm

added theorem complex.is_open_set_of_mem_nhds_and_is_max_on_norm

added theorem complex.norm_eq_norm_of_is_max_on_of_closed_ball_subset

added theorem complex.norm_eq_on_closed_ball_of_is_max_on

added theorem complex.norm_eventually_eq_of_is_local_max

added theorem complex.norm_le_of_forall_mem_frontier_norm_le

added theorem complex.norm_max_aux₁

added theorem complex.norm_max_aux₂

added theorem complex.norm_max_aux₃