From 41e467ac020bf6b45a0109522caf9b3d330e2e20 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 17 Jul 2022 04:14:30 +0000
Subject: [PATCH] feat(analysis/complex/abs_max): add a version of the maximum
 modulus principle (#15364)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* 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.
---
 docs/overview.yaml                           |  10 +
 docs/undergrad.yaml                          |   6 +-
 src/analysis/complex/abs_max.lean            | 228 +++++++++++++++++--
 src/analysis/convex/strict_convex_space.lean |   5 +
 src/analysis/convex/topology.lean            |  13 +-
 src/analysis/normed_space/extr.lean          |  85 +++++++
 src/analysis/normed_space/ray.lean           |   9 +
 7 files changed, 327 insertions(+), 29 deletions(-)
 create mode 100644 src/analysis/normed_space/extr.lean

diff --git a/docs/overview.yaml b/docs/overview.yaml
index 553a47b1724b5..7ace0212f69c0 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -333,6 +333,16 @@ Analysis:
     regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
     change of variables formula: 'measure_theory.integral_image_eq_integral_abs_det_fderiv_smul'
 
+  Complex analysis:
+    Cauchy integral formula: 'diff_cont_on_cl.circle_integral_sub_inv_smul'
+    Liouville theorem: 'differentiable.apply_eq_apply_of_bounded'
+    maximum modulus principle: 'complex.eventually_eq_of_is_local_max_norm'
+    analyticity of holomorphic functions: 'differentiable_on.analytic_at'
+    Schwarz lemma: 'complex.abs_le_abs_of_maps_to_ball_self'
+    removable singularity: 'complex.differentiable_on_update_lim_insert_of_is_o'
+    Phragmen-Lindelöf principle: 'phragmen_lindelof.horizontal_strip'
+    fundamental theorem of algebra: 'complex.is_alg_closed'
+
 Probability Theory:
   Definitions in probability theory:
     probability measure: 'measure_theory.is_probability_measure'
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
index 7bc41ef6bd4b4..6f6f7c711309a 100644
--- a/docs/undergrad.yaml
+++ b/docs/undergrad.yaml
@@ -371,7 +371,7 @@ Single Variable Complex Analysis:
     extension of trigonometric functions to the complex plane: 'complex.sin'
     power series expansion of elementary functions: ''
   Functions on one complex variable:
-    holomorphic functions: ''
+    holomorphic functions: 'differentiable_on'
     Cauchy-Riemann conditions: ''
     contour integrals of continuous functions in $\C$: ''
     antiderivatives of a holomorphic function: ''
@@ -379,10 +379,10 @@ Single Variable Complex Analysis:
     theorem of holomorphic functions under integral domains: ''
     winding number of a closed curve in $\C$ with respect to a point: ''
     Cauchy formulas: ''
-    analyticity of a holomorphic function: ''
+    analyticity of a holomorphic function: 'differentiable_on.analytic_at'
     principle of isolated zeros: ''
     principle of analytic continuation: ''
-    maximum principle: ''
+    maximum principle: 'complex.eventually_eq_of_is_local_max_norm'
     isolated singularities: ''
     Laurent series: ''
     meromorphic functions: ''
diff --git a/src/analysis/complex/abs_max.lean b/src/analysis/complex/abs_max.lean
index 0a5c350c688d6..9f82194df62d3 100644
--- a/src/analysis/complex/abs_max.lean
+++ b/src/analysis/complex/abs_max.lean
@@ -6,28 +6,75 @@ Authors: Yury G. Kudryashov
 import analysis.complex.cauchy_integral
 import analysis.convex.integral
 import analysis.normed_space.completion
+import analysis.normed_space.extr
 import topology.algebra.order.extr_closure
 
 /-!
 # Maximum modulus principle
 
-In this file we prove several versions of the maximum modulus principle.
+In this file we prove several versions of the maximum modulus principle. There are several
+statements that can be called "the maximum modulus principle" for maps between normed complex
+spaces. They differ by assumptions on the domain (any space, a nontrivial space, a finite
+dimensional space), assumptions on the codomain (any space, a strictly convex space), and by
+conclusion (either equality of norms or of the values of the function).
 
-There are several statements that can be called "the maximum modulus principle" for maps between
-normed complex spaces.
+## Main results
 
-In the most general case, see `complex.norm_eventually_eq_of_is_local_max`, we can only say that for
-a differentiable function `f : E → F`, if the norm has a local maximum at `z`, then *the norm* is
-constant in a neighborhood of `z`.
+### Theorems for any codomain
 
-If the domain is a nontrivial finite dimensional space, then this implies the following version of
-the maximum modulus principle, see `complex.exists_mem_frontier_is_max_on_norm`. If `f : E → F` is
-complex differentiable on a nonempty compact set `K`, then there exists a point `z ∈ frontier K`
-such that `λ z, ∥f z∥` takes it maximum value on `K` at `z`.
+Consider a function `f : E → F` that is complex differentiable on a set `s`, is continuous on its
+closure, and `∥f x∥` has a maximum on `s` at `c`. We prove the following theorems.
 
-Finally, if the codomain is a strictly convex space, then the function cannot have a local maximum
-of the norm unless the function (not only its norm) is a constant. This version is not formalized
-yet.
+- `complex.norm_eq_on_closed_ball_of_is_max_on`: if `s = metric.ball c r`, then `∥f x∥ = ∥f c∥` for
+  any `x` from the corresponding closed ball;
+
+- `complex.norm_eq_norm_of_is_max_on_of_ball_subset`: if `metric.ball c (dist w c) ⊆ s`, then
+  `∥f w∥ = ∥f c∥`;
+
+- `complex.norm_eq_on_of_is_preconnected_of_is_max_on`: if `U` is an open (pre)connected set, `f` is
+  complex differentiable on `U`, and `∥f x∥` has a maximum on `U` at `c ∈ U`, then `∥f x∥ = ∥f c∥`
+  for all `x ∈ U`;
+
+- `complex.norm_eq_on_closure_of_is_preconnected_of_is_max_on`: if `s` is open and (pre)connected
+  and `c ∈ s`, then `∥f x∥ = ∥f c∥` for all `x ∈ closure s`;
+
+- `complex.norm_eventually_eq_of_is_local_max`: if `f` is complex differentiable in a neighborhood
+  of `c` and `∥f x∥` has a local maximum at `c`, then `∥f x∥` is locally a constant in a
+  neighborhood of `c`.
+
+### Theorems for a strictly convex codomain
+
+If the codomain `F` is a strictly convex space, then in the lemmas from the previous section we can
+prove `f w = f c` instead of `∥f w∥ = ∥f c∥`, see
+`complex.eq_on_of_is_preconnected_of_is_max_on_norm`,
+`complex.eq_on_closure_of_is_preconnected_of_is_max_on_norm`,
+`complex.eq_of_is_max_on_of_ball_subset`, `complex.eq_on_closed_ball_of_is_max_on_norm`, and
+`complex.eventually_eq_of_is_local_max_norm`.
+
+### Values on the frontier
+
+Finally, we prove some corollaries that relate the (norm of the) values of a function on a set to
+its values on the frontier of the set. All these lemmas assume that `E` is a nontrivial space.  In
+this section `f g : E → F` are functions that are complex differentiable on a bounded set `s` and
+are continuous on its closure. We prove the following theorems.
+
+- `complex.exists_mem_frontier_is_max_on_norm`: If `E` is a finite dimensional space and `s` is a
+  nonempty bounded set, then there exists a point `z ∈ frontier s` such that `λ z, ∥f z∥` takes it
+  maximum value on `closure s` at `z`.
+
+- `complex.norm_le_of_forall_mem_frontier_norm_le`: if `∥f z∥ ≤ C` for all `z ∈ frontier s`, then
+  `∥f z∥ ≤ C` for all `z ∈ s`; note that this theorem does not require `E` to be a finite
+  dimensional space.
+
+- `complex.eq_on_closure_of_eq_on_frontier`: if `f x = g x` on the frontier of `s`, then `f x = g x`
+  on `closure s`;
+
+- `complex.eq_on_of_eq_on_frontier`: if `f x = g x` on the frontier of `s`, then `f x = g x`
+  on `s`.
+
+## Tags
+
+maximum modulus principle, complex analysis
 -/
 
 open topological_space metric set filter asymptotics function measure_theory affine_map
@@ -48,8 +95,8 @@ We split the proof into a series of lemmas. First we prove the principle for a f
 with an additional assumption that `F` is a complete space, then drop unneeded assumptions one by
 one.
 
-The only "public API" lemmas in this section are TODO and
-`complex.norm_eq_norm_of_is_max_on_of_closed_ball_subset`.
+The lemmas with names `*_auxₙ` are considered to be private and should not be used outside of this
+file.
 -/
 
 lemma norm_max_aux₁ [complete_space F] {f : ℂ → F} {z w : ℂ}
@@ -119,6 +166,13 @@ begin
   exact norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuous_on.norm)
 end
 
+/-!
+### Maximum modulus principle for any codomain
+
+If we do not assume that the codomain is a strictly convex space, then we can only claim that the
+**norm** `∥f x∥` is locally constant.
+-/
+
 /-!
 Finally, we generalize the theorem from a disk in `ℂ` to a closed ball in any normed space.
 -/
@@ -145,12 +199,8 @@ begin
     (hz.comp_maps_to hball (line_map_apply_zero z w))
 end
 
-/-!
-### Different forms of the maximum modulus principle
--/
-
 /-- **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`
+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∥`. -/
 lemma norm_eq_norm_of_is_max_on_of_ball_subset {f : E → F} {s : set E} {z w : E}
   (hd : diff_cont_on_cl ℂ f s) (hz : is_max_on (norm ∘ f) s z) (hsub : ball z (dist w z) ⊆ s) :
@@ -181,11 +231,139 @@ begin
     (λ x hx y hy, le_trans (hz.2 hy) hx.ge)
 end
 
+/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
+complex normed space. Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
+that `∥f x∥` takes its maximum value on `U` at `c ∈ U`. Then `∥f x∥ = ∥f c∥` for all `x ∈ U`. -/
+lemma norm_eq_on_of_is_preconnected_of_is_max_on {f : E → F} {U : set E} {c : E}
+  (hc : is_preconnected U) (ho : is_open U) (hd : differentiable_on ℂ f U) (hcU : c ∈ U)
+  (hm : is_max_on (norm ∘ f) U c) :
+  eq_on (norm ∘ f) (const E ∥f c∥) U :=
+begin
+  set V := U ∩ {z | is_max_on (norm ∘ f) U z},
+  have hV : ∀ x ∈ V, ∥f x∥ = ∥f c∥, from λ x hx, le_antisymm (hm hx.1) (hx.2 hcU),
+  suffices : U ⊆ V, from λ x hx, hV x (this hx),
+  have hVo : is_open V,
+  { simpa only [ho.mem_nhds_iff, set_of_and, set_of_mem_eq]
+      using is_open_set_of_mem_nhds_and_is_max_on_norm hd },
+  have hVne : (U ∩ V).nonempty := ⟨c, hcU, hcU, hm⟩,
+  set W := U ∩ {z | ∥f z∥ ≠ ∥f c∥},
+  have hWo : is_open W, from hd.continuous_on.norm.preimage_open_of_open ho is_open_ne,
+  have hdVW : disjoint V W, from λ x ⟨hxV, hxW⟩, hxW.2 (hV x hxV),
+  have hUVW : U ⊆ V ∪ W,
+    from λ x hx, (eq_or_ne (∥f x∥) (∥f c∥)).imp (λ h, ⟨hx, λ y hy, (hm hy).out.trans_eq h.symm⟩)
+      (and.intro hx),
+  exact hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne,
+end
+
+/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
+complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U` and is
+continuous on its closure. Suppose that `∥f x∥` takes its maximum value on `U` at `c ∈ U`. Then
+`∥f x∥ = ∥f c∥` for all `x ∈ closure U`. -/
+lemma norm_eq_on_closure_of_is_preconnected_of_is_max_on {f : E → F} {U : set E} {c : E}
+  (hc : is_preconnected U) (ho : is_open U) (hd : diff_cont_on_cl ℂ f U) (hcU : c ∈ U)
+  (hm : is_max_on (norm ∘ f) U c) :
+  eq_on (norm ∘ f) (const E ∥f c∥) (closure U) :=
+(norm_eq_on_of_is_preconnected_of_is_max_on hc ho hd.differentiable_on hcU hm).of_subset_closure
+  hd.continuous_on.norm continuous_on_const subset_closure subset.rfl
+
+section strict_convex
+
+/-!
+### The case of a strictly convex codomain
+
+If the codomain `F` is a strictly convex space, then we can claim equalities like `f w = f z`
+instead of `∥f w∥ = ∥f z∥`.
+
+Instead of repeating the proof starting with lemmas about integrals, we apply a corresponding lemma
+above twice: for `f` and for `λ x, f x + f c`.  Then we have `∥f w∥ = ∥f z∥` and
+`∥f w + f z∥ = ∥f z + f z∥`, thus `∥f w + f z∥ = ∥f w∥ + ∥f z∥`. This is only possible if
+`f w = f z`, see `eq_of_norm_eq_of_norm_add_eq`.
+-/
+
+variables [strict_convex_space ℝ F]
+
+/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
+complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
+that `∥f x∥` takes its maximum value on `U` at `c ∈ U`. Then `f x = f c` for all `x ∈ U`.
+
+TODO: change assumption from `is_max_on` to `is_local_max`. -/
+lemma eq_on_of_is_preconnected_of_is_max_on_norm {f : E → F} {U : set E} {c : E}
+  (hc : is_preconnected U) (ho : is_open U) (hd : differentiable_on ℂ f U) (hcU : c ∈ U)
+  (hm : is_max_on (norm ∘ f) U c) :
+  eq_on f (const E (f c)) U :=
+λ x hx,
+have H₁ : ∥f x∥ = ∥f c∥, from norm_eq_on_of_is_preconnected_of_is_max_on hc ho hd hcU hm hx,
+have H₂ : ∥f x + f c∥ = ∥f c + f c∥,
+  from norm_eq_on_of_is_preconnected_of_is_max_on hc ho (hd.add_const _) hcU hm.norm_add_self hx,
+eq_of_norm_eq_of_norm_add_eq H₁ $ by simp only [H₂, same_ray.rfl.norm_add, H₁]
+
+/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
+complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U` and is
+continuous on its closure. Suppose that `∥f x∥` takes its maximum value on `U` at `c ∈ U`. Then
+`f x = f c` for all `x ∈ closure U`. -/
+lemma eq_on_closure_of_is_preconnected_of_is_max_on_norm {f : E → F} {U : set E} {c : E}
+  (hc : is_preconnected U) (ho : is_open U) (hd : diff_cont_on_cl ℂ f U) (hcU : c ∈ U)
+  (hm : is_max_on (norm ∘ f) U c) :
+  eq_on f (const E (f c)) (closure U) :=
+(eq_on_of_is_preconnected_of_is_max_on_norm hc ho hd.differentiable_on hcU hm).of_subset_closure
+  hd.continuous_on continuous_on_const subset_closure subset.rfl
+
+/-- **Maximum modulus principle**. Let `f : E → F` be a function between complex normed spaces.
+Suppose that the codomain `F` is a strictly convex space, `f` is complex differentiable on a set
+`s`, `f` is continuous on the closure of `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`. -/
+lemma eq_of_is_max_on_of_ball_subset {f : E → F} {s : set E} {z w : E} (hd : diff_cont_on_cl ℂ f s)
+  (hz : is_max_on (norm ∘ f) s z) (hsub : ball z (dist w z) ⊆ s) :
+  f w = f z :=
+have H₁ : ∥f w∥ = ∥f z∥, from norm_eq_norm_of_is_max_on_of_ball_subset hd hz hsub,
+have H₂ : ∥f w + f z∥ = ∥f z + f z∥,
+  from norm_eq_norm_of_is_max_on_of_ball_subset (hd.add_const _) hz.norm_add_self hsub,
+eq_of_norm_eq_of_norm_add_eq H₁ $ by simp only [H₂, same_ray.rfl.norm_add, H₁]
+
+/-- **Maximum modulus principle** on a closed ball. Suppose that a function `f : E → F` from a
+normed complex space to a strictly convex normed complex space has the following properties:
+
+- it is continuous on a closed ball `metric.closed_ball z r`,
+- it is complex differentiable on the corresponding open ball;
+- the norm `∥f w∥` takes its maximum value on the open ball at its center.
+
+Then `f` is a constant on the closed ball.  -/
+lemma eq_on_closed_ball_of_is_max_on_norm {f : E → F} {z : E} {r : ℝ}
+  (hd : diff_cont_on_cl ℂ f (ball z r)) (hz : is_max_on (norm ∘ f) (ball z r) z) :
+  eq_on f (const E (f z)) (closed_ball z r) :=
+λ x hx, eq_of_is_max_on_of_ball_subset hd hz $ ball_subset_ball hx
+
+/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable in a neighborhood of `c`
+and the norm `∥f z∥` has a local maximum at `c`, then `f` is locally constant in a neighborhood
+of `c`. -/
+lemma eventually_eq_of_is_local_max_norm {f : E → F} {c : E}
+  (hd : ∀ᶠ z in 𝓝 c, differentiable_at ℂ f z) (hc : is_local_max (norm ∘ f) c) :
+  ∀ᶠ y in 𝓝 c, f y = f c :=
+begin
+  rcases nhds_basis_closed_ball.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩,
+  exact nhds_basis_closed_ball.eventually_iff.2 ⟨r, hr₀, eq_on_closed_ball_of_is_max_on_norm
+    (differentiable_on.diff_cont_on_cl $
+      λ x hx, (hr $ closure_ball_subset_closed_ball hx).1.differentiable_within_at)
+    (λ x hx, (hr $ ball_subset_closed_ball hx).2)⟩
+end
+
+end strict_convex
+
+/-!
+### Maximum on a set vs maximum on its frontier
+
+In this section we prove corollaries of the maximum modulus principle that relate the values of a
+function on a set to its values on the frontier of this set.
+-/
+
+variable [nontrivial E]
+
 /-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a nonempty bounded
 set `U` and is continuous on its closure, then there exists a point `z ∈ frontier U` such that
 `λ z, ∥f z∥` takes it maximum value on `closure U` at `z`. -/
-lemma exists_mem_frontier_is_max_on_norm [nontrivial E] [finite_dimensional ℂ E]
-  {f : E → F} {U : set E} (hb : bounded U) (hne : U.nonempty) (hd : diff_cont_on_cl ℂ f U) :
+lemma exists_mem_frontier_is_max_on_norm [finite_dimensional ℂ E] {f : E → F} {U : set E}
+  (hb : bounded U) (hne : U.nonempty) (hd : diff_cont_on_cl ℂ f U) :
   ∃ z ∈ frontier U, is_max_on (norm ∘ f) (closure U) z :=
 begin
   have hc : is_compact (closure U), from hb.is_compact_closure,
@@ -203,7 +381,7 @@ end
 
 /-- **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`. -/
-lemma norm_le_of_forall_mem_frontier_norm_le [nontrivial E] {f : E → F} {U : set E} (hU : bounded U)
+lemma norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : set E} (hU : bounded U)
   (hd : diff_cont_on_cl ℂ f U) {C : ℝ} (hC : ∀ z ∈ frontier U, ∥f z∥ ≤ C)
   {z : E} (hz : z ∈ closure U) :
   ∥f z∥ ≤ C :=
@@ -228,7 +406,7 @@ end
 
 /-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
 `U`, then they are equal on `closure U`. -/
-lemma eq_on_closure_of_eq_on_frontier [nontrivial E] {f g : E → F} {U : set E} (hU : bounded U)
+lemma eq_on_closure_of_eq_on_frontier {f g : E → F} {U : set E} (hU : bounded U)
   (hf : diff_cont_on_cl ℂ f U) (hg : diff_cont_on_cl ℂ g U) (hfg : eq_on f g (frontier U)) :
   eq_on f g (closure U) :=
 begin
@@ -239,7 +417,7 @@ end
 
 /-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
 `U`, then they are equal on `U`. -/
-lemma eq_on_of_eq_on_frontier [nontrivial E] {f g : E → F} {U : set E} (hU : bounded U)
+lemma eq_on_of_eq_on_frontier {f g : E → F} {U : set E} (hU : bounded U)
   (hf : diff_cont_on_cl ℂ f U) (hg : diff_cont_on_cl ℂ g U) (hfg : eq_on f g (frontier U)) :
   eq_on f g U :=
 (eq_on_closure_of_eq_on_frontier hU hf hg hfg).mono subset_closure
diff --git a/src/analysis/convex/strict_convex_space.lean b/src/analysis/convex/strict_convex_space.lean
index 9a0370eefe98f..293808bc66e2e 100644
--- a/src/analysis/convex/strict_convex_space.lean
+++ b/src/analysis/convex/strict_convex_space.lean
@@ -219,6 +219,11 @@ inequality for `x` and `y` becomes an equality. -/
 lemma same_ray_iff_norm_add : same_ray ℝ x y ↔ ∥x + y∥ = ∥x∥ + ∥y∥ :=
 ⟨same_ray.norm_add, λ h, not_not.1 $ λ h', (norm_add_lt_of_not_same_ray h').ne h⟩
 
+/-- If `x` and `y` are two vectors in a strictly convex space have the same norm and the norm of
+their sum is equal to the sum of their norms, then they are equal. -/
+lemma eq_of_norm_eq_of_norm_add_eq (h₁ : ∥x∥ = ∥y∥) (h₂ : ∥x + y∥ = ∥x∥ + ∥y∥) : x = y :=
+(same_ray_iff_norm_add.mpr h₂).eq_of_norm_eq h₁
+
 /-- In a strictly convex space, two vectors `x`, `y` are not in the same ray if and only if the
 triangle inequality for `x` and `y` is strict. -/
 lemma not_same_ray_iff_norm_add_lt : ¬ same_ray ℝ x y ↔ ∥x + y∥ < ∥x∥ + ∥y∥ :=
diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean
index 28f625b7a4016..5381e8564c8c4 100644
--- a/src/analysis/convex/topology.lean
+++ b/src/analysis/convex/topology.lean
@@ -39,7 +39,7 @@ open_locale pointwise convex
 lemma real.convex_iff_is_preconnected {s : set ℝ} : convex ℝ s ↔ is_preconnected s :=
 convex_iff_ord_connected.trans is_preconnected_iff_ord_connected.symm
 
-alias real.convex_iff_is_preconnected ↔ convex.is_preconnected is_preconnected.convex
+alias real.convex_iff_is_preconnected ↔ _ is_preconnected.convex
 
 /-! ### Standard simplex -/
 
@@ -265,6 +265,7 @@ lemma convex.subset_interior_image_homothety_of_one_lt {s : set E} (hs : convex
   s ⊆ interior (homothety x t '' s) :=
 subset_closure.trans $ hs.closure_subset_interior_image_homothety_of_one_lt hx t ht
 
+/-- A nonempty convex set is path connected. -/
 protected lemma convex.is_path_connected {s : set E} (hconv : convex ℝ s) (hne : s.nonempty) :
   is_path_connected s :=
 begin
@@ -276,6 +277,16 @@ begin
     (line_map_apply_one _ _) H
 end
 
+/-- A nonempty convex set is connected. -/
+protected lemma convex.is_connected {s : set E} (h : convex ℝ s) (hne : s.nonempty) :
+  is_connected s :=
+(h.is_path_connected hne).is_connected
+
+/-- A convex set is preconnected. -/
+protected lemma convex.is_preconnected {s : set E} (h : convex ℝ s) : is_preconnected s :=
+s.eq_empty_or_nonempty.elim (λ h, h.symm ▸ is_preconnected_empty)
+  (λ hne, (h.is_connected hne).is_preconnected)
+
 /--
 Every topological vector space over ℝ is path connected.
 
diff --git a/src/analysis/normed_space/extr.lean b/src/analysis/normed_space/extr.lean
new file mode 100644
index 0000000000000..ea541566064e6
--- /dev/null
+++ b/src/analysis/normed_space/extr.lean
@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.normed_space.ray
+import topology.local_extr
+
+/-!
+# (Local) maximums in a normed space
+
+In this file we prove the following lemma, see `is_max_filter.norm_add_same_ray`. If `f : α → E` is
+a function such that `norm ∘ f` has a maximum along a filter `l` at a point `c` and `y` is a vector
+on the same ray as `f c`, then the function `λ x, ∥f x + y∥` has a maximul along `l` at `c`.
+
+Then we specialize it to the case `y = f c` and to different special cases of `is_max_filter`:
+`is_max_on`, `is_local_max_on`, and `is_local_max`.
+
+## Tags
+
+local maximum, normed space
+-/
+
+variables {α X E : Type*} [semi_normed_group E] [normed_space ℝ E] [topological_space X]
+
+section
+
+variables {f : α → E} {l : filter α} {s : set α} {c : α} {y : E}
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum along a filter `l` at a point
+`c` and `y` is a vector on the same ray as `f c`, then the function `λ x, ∥f x + y∥` has a maximul
+along `l` at `c`. -/
+lemma is_max_filter.norm_add_same_ray (h : is_max_filter (norm ∘ f) l c) (hy : same_ray ℝ (f c) y) :
+  is_max_filter (λ x, ∥f x + y∥) l c :=
+h.mono $ λ x hx,
+calc ∥f x + y∥ ≤ ∥f x∥ + ∥y∥ : norm_add_le _ _
+           ... ≤ ∥f c∥ + ∥y∥ : add_le_add_right hx _
+           ... = ∥f c + y∥   : hy.norm_add.symm
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum along a filter `l` at a point
+`c`, then the function `λ x, ∥f x + f c∥` has a maximul along `l` at `c`. -/
+lemma is_max_filter.norm_add_self (h : is_max_filter (norm ∘ f) l c) :
+  is_max_filter (λ x, ∥f x + f c∥) l c :=
+h.norm_add_same_ray same_ray.rfl
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum on a set `s` at a point `c` and
+`y` is a vector on the same ray as `f c`, then the function `λ x, ∥f x + y∥` has a maximul on `s` at
+`c`. -/
+lemma is_max_on.norm_add_same_ray (h : is_max_on (norm ∘ f) s c) (hy : same_ray ℝ (f c) y) :
+  is_max_on (λ x, ∥f x + y∥) s c :=
+h.norm_add_same_ray hy
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum on a set `s` at a point `c`,
+then the function `λ x, ∥f x + f c∥` has a maximul on `s` at `c`. -/
+lemma is_max_on.norm_add_self (h : is_max_on (norm ∘ f) s c) : is_max_on (λ x, ∥f x + f c∥) s c :=
+h.norm_add_self
+
+end
+
+variables {f : X → E} {s : set X} {c : X} {y : E}
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum on a set `s` at a point
+`c` and `y` is a vector on the same ray as `f c`, then the function `λ x, ∥f x + y∥` has a local
+maximul on `s` at `c`. -/
+lemma is_local_max_on.norm_add_same_ray (h : is_local_max_on (norm ∘ f) s c)
+  (hy : same_ray ℝ (f c) y) : is_local_max_on (λ x, ∥f x + y∥) s c :=
+h.norm_add_same_ray hy
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum on a set `s` at a point
+`c`, then the function `λ x, ∥f x + f c∥` has a local maximul on `s` at `c`. -/
+lemma is_local_max_on.norm_add_self (h : is_local_max_on (norm ∘ f) s c) :
+  is_local_max_on (λ x, ∥f x + f c∥) s c :=
+h.norm_add_self
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum at a point `c` and `y` is
+a vector on the same ray as `f c`, then the function `λ x, ∥f x + y∥` has a local maximul at `c`. -/
+lemma is_local_max.norm_add_same_ray (h : is_local_max (norm ∘ f) c)
+  (hy : same_ray ℝ (f c) y) : is_local_max (λ x, ∥f x + y∥) c :=
+h.norm_add_same_ray hy
+
+/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum at a point `c`, then the
+function `λ x, ∥f x + f c∥` has a local maximul at `c`. -/
+lemma is_local_max.norm_add_self (h : is_local_max (norm ∘ f) c) :
+  is_local_max (λ x, ∥f x + f c∥) c :=
+h.norm_add_self
diff --git a/src/analysis/normed_space/ray.lean b/src/analysis/normed_space/ray.lean
index a813093626bbe..992d0ead9f667 100644
--- a/src/analysis/normed_space/ray.lean
+++ b/src/analysis/normed_space/ray.lean
@@ -90,6 +90,7 @@ begin
   simp only [same_ray_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or]
 end
 
+/-- Two vectors of the same norm are on the same ray if and only if they are equal. -/
 lemma same_ray_iff_of_norm_eq (h : ∥x∥ = ∥y∥) : same_ray ℝ x y ↔ x = y :=
 begin
   obtain rfl | hy := eq_or_ne y 0,
@@ -100,3 +101,11 @@ end
 
 lemma not_same_ray_iff_of_norm_eq (h : ∥x∥ = ∥y∥) : ¬ same_ray ℝ x y ↔ x ≠ y :=
 (same_ray_iff_of_norm_eq h).not
+
+/-- If two points on the same ray have the same norm, then they are equal. -/
+lemma same_ray.eq_of_norm_eq (h : same_ray ℝ x y) (hn : ∥x∥ = ∥y∥) : x = y :=
+(same_ray_iff_of_norm_eq hn).mp h
+
+/-- The norms of two vectors on the same ray are equal if and only if they are equal. -/
+lemma same_ray.norm_eq_iff (h : same_ray ℝ x y) : ∥x∥ = ∥y∥ ↔ x = y :=
+⟨h.eq_of_norm_eq, λ h, h ▸ rfl⟩