(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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {l : Filter α} {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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {l : Filter α} {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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace X] {f : X → E} {s : Set X} {c : X} {y : E} (h : IsLocalMaxOn (norm ∘ f) s c) (hy : SameRay ℝ (f c) y) : IsLocalMaxOn (fun (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 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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace X] {f : X → E} {s : Set X} {c : X} (h : IsLocalMaxOn (norm ∘ f) s c) : IsLocalMaxOn (fun (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 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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace X] {f : X → E} {c : X} {y : E} (h : IsLocalMax (norm ∘ f) c) (hy : SameRay ℝ (f c) y) : IsLocalMax (fun (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 fun x => ‖f x + y‖ has a local maximum at c.

theorem IsLocalMax.norm_add_self {X : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace X] {f : X → E} {c : X} (h : IsLocalMax (norm ∘ f) c) : IsLocalMax (fun (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 fun x => ‖f x + f c‖ has a local maximum at c.