# Documentation

Mathlib.Analysis.NormedSpace.Extr

# (Local) maximums in a normed space #

In this file we prove the following lemma, see IsMaxFilter.norm_add_sameRay. 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 fun x => ‖f x + y‖ has a maximum along l at c.

Then we specialize it to the case y = f c and to different special cases of IsMaxFilter: IsMaxOn, IsLocalMaxOn, and IsLocalMax.

## Tags #

local maximum, normed space

theorem IsMaxFilter.norm_add_sameRay {α : Type u_1} {E : Type u_3} [] {f : αE} {l : } {c : α} {y : E} (h : IsMaxFilter (norm f) l c) (hy : SameRay (f c) y) :
IsMaxFilter (fun x => f x + y) l c

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 fun x => ‖f x + y‖ has a maximum along l at c.

theorem IsMaxFilter.norm_add_self {α : Type u_1} {E : Type u_3} [] {f : αE} {l : } {c : α} (h : IsMaxFilter (norm f) l c) :
IsMaxFilter (fun x => f x + f c) l c

If f : α → E is a function such that norm ∘ f has a maximum along a filter l at a point c, then the function fun x => ‖f x + f c‖ has a maximum along l at c.

theorem IsMaxOn.norm_add_sameRay {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {c : α} {y : E} (h : IsMaxOn (norm f) s c) (hy : SameRay (f c) y) :
IsMaxOn (fun x => f x + y) s c

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 fun x => ‖f x + y‖ has a maximum on s at c.

theorem IsMaxOn.norm_add_self {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {c : α} (h : IsMaxOn (norm f) s c) :
IsMaxOn (fun x => f x + f c) s c

If f : α → E is a function such that norm ∘ f has a maximum on a set s at a point c, then the function fun x => ‖f x + f c‖ has a maximum on s at c.

theorem IsLocalMaxOn.norm_add_sameRay {X : Type u_2} {E : Type u_3} [] [] {f : XE} {s : Set X} {c : X} {y : E} (h : IsLocalMaxOn (norm f) s c) (hy : SameRay (f c) y) :
IsLocalMaxOn (fun x => f x + y) s c

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 fun x => ‖f x + y‖ has a local maximum on s at c.

theorem IsLocalMaxOn.norm_add_self {X : Type u_2} {E : Type u_3} [] [] {f : XE} {s : Set X} {c : X} (h : IsLocalMaxOn (norm f) s c) :
IsLocalMaxOn (fun x => f x + f c) s c

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 fun x => ‖f x + f c‖ has a local maximum on s at c.

theorem IsLocalMax.norm_add_sameRay {X : Type u_2} {E : Type u_3} [] [] {f : XE} {c : X} {y : E} (h : IsLocalMax (norm f) c) (hy : SameRay (f c) y) :
IsLocalMax (fun x => f x + y) c

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 fun x => ‖f x + y‖ has a local maximum at c.

theorem IsLocalMax.norm_add_self {X : Type u_2} {E : Type u_3} [] [] {f : XE} {c : X} (h : IsLocalMax (norm f) c) :
IsLocalMax (fun x => f x + f c) c

If f : α → E is a function such that norm ∘ f has a local maximum at a point c, then the function fun x => ‖f x + f c‖ has a local maximum at c.