Commit 2022-07-17 04:14 41e467ac

feat(analysis/complex/abs_max): add a version of the maximum modulus principle (#15364)

• Add versions of the maximum modulus principle that assume strict convexity of the codomain and prove f x = f y instead of ∥f x∥ = ∥f y∥

• Add a version of the maximum modulus principle for arbitrary open connected sets.

• Add supporting lemmas.

  • More lemmas about strictly convex spaces and norm (eq_of_norm_eq_of_norm_add_eq, same_ray.eq_of_norm_eq, same_ray.norm_eq_iff);

  • Lemmas about is_max_* and λ x, ∥f x + y∥.

  • Generalize convex.is_preconnected from ℝ to a real vector space.

• Improve documentation.