Commit 2023-06-09 14:49 eb1efd93

View on Github →

feat: port Analysis.Complex.AbsMax (#4901)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/AbsMax.lean

added theorem Complex.eqOn_closedBall_of_isMaxOn_norm

added theorem Complex.eqOn_closure_of_eqOn_frontier

added theorem Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm

added theorem Complex.eqOn_of_eqOn_frontier

added theorem Complex.eqOn_of_isPreconnected_of_isMaxOn_norm

added theorem Complex.eq_of_isMaxOn_of_ball_subset

added theorem Complex.eventually_eq_of_isLocalMax_norm

added theorem Complex.eventually_eq_or_eq_zero_of_isLocalMin_norm

added theorem Complex.exists_mem_frontier_isMaxOn_norm

added theorem Complex.isOpen_setOf_mem_nhds_and_isMaxOn_norm

added theorem Complex.norm_eqOn_closedBall_of_isMaxOn

added theorem Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn

added theorem Complex.norm_eqOn_of_isPreconnected_of_isMaxOn

added theorem Complex.norm_eq_norm_of_isMaxOn_of_ball_subset

added theorem Complex.norm_eventually_eq_of_isLocalMax

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₃