mathlib3 documentation

analysis.normed_space.extr

(Local) maximums in a normed space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [seminormed_add_comm_group E] [normed_space E] {f : α E} {l : filter α} {c : α} {y : E} (h : is_max_filter (has_norm.norm f) l c) (hy : same_ray (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} [seminormed_add_comm_group E] [normed_space E] {f : α E} {l : filter α} {c : α} (h : is_max_filter (has_norm.norm f) 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} [seminormed_add_comm_group E] [normed_space E] {f : α E} {s : set α} {c : α} {y : E} (h : is_max_on (has_norm.norm f) s c) (hy : same_ray (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} [seminormed_add_comm_group E] [normed_space E] {f : α E} {s : set α} {c : α} (h : is_max_on (has_norm.norm f) 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} [seminormed_add_comm_group E] [normed_space E] [topological_space X] {f : X E} {s : set X} {c : X} {y : E} (h : is_local_max_on (has_norm.norm f) s c) (hy : same_ray (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} [seminormed_add_comm_group E] [normed_space E] [topological_space X] {f : X E} {s : set X} {c : X} (h : is_local_max_on (has_norm.norm f) s 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} [seminormed_add_comm_group E] [normed_space E] [topological_space X] {f : X E} {c : X} {y : E} (h : is_local_max (has_norm.norm f) c) (hy : same_ray (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} [seminormed_add_comm_group E] [normed_space E] [topological_space X] {f : X E} {c : X} (h : is_local_max (has_norm.norm f) 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.