# mathlibdocumentation

analysis.normed_space.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

theorem is_max_filter.norm_add_same_ray {α : Type u_1} {E : Type u_3} [ E] {f : α → E} {l : filter α} {c : α} {y : E} (h : l c) (hy : (f c) y) :
is_max_filter (λ (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 λ x, ∥f x + y∥ has a maximul along l at c.

theorem is_max_filter.norm_add_self {α : Type u_1} {E : Type u_3} [ E] {f : α → E} {l : filter α} {c : α} (h : l c) :
is_max_filter (λ (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 λ x, ∥f x + f c∥ has a maximul along l at c.

theorem is_max_on.norm_add_same_ray {α : Type u_1} {E : Type u_3} [ E] {f : α → E} {s : set α} {c : α} {y : E} (h : s c) (hy : (f c) y) :
is_max_on (λ (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 λ x, ∥f x + y∥ has a maximul on s at c.

theorem is_max_on.norm_add_self {α : Type u_1} {E : Type u_3} [ E] {f : α → E} {s : set α} {c : α} (h : s c) :
is_max_on (λ (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 λ x, ∥f x + f c∥ has a maximul on s at c.

theorem is_local_max_on.norm_add_same_ray {X : Type u_2} {E : Type u_3} [ E] {f : X → E} {s : set X} {c : X} {y : E} (h : c) (hy : (f c) y) :
is_local_max_on (λ (x : 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 λ x, ∥f x + y∥ has a local maximul on s at c.

theorem is_local_max_on.norm_add_self {X : Type u_2} {E : Type u_3} [ E] {f : X → E} {s : set X} {c : X} (h : c) :
is_local_max_on (λ (x : 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 λ x, ∥f x + f c∥ has a local maximul on s at c.

theorem is_local_max.norm_add_same_ray {X : Type u_2} {E : Type u_3} [ E] {f : X → E} {c : X} {y : E} (h : c) (hy : (f c) y) :
is_local_max (λ (x : 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 λ x, ∥f x + y∥ has a local maximul at c.

theorem is_local_max.norm_add_self {X : Type u_2} {E : Type u_3} [ E] {f : X → E} {c : X} (h : c) :
is_local_max (λ (x : 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 λ x, ∥f x + f c∥ has a local maximul at c.