(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

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.