English
If f: X → E has a local maximum of ‖f‖ on a set s at c and y lies on the same ray as f(c), then x ↦ ‖f(x) + y‖ has a local maximum on s at c.
Русский
Если у f: X → E локальный максимум по норме на множестве s в точке c, и y лежит на том же луче, что и f(c), то x ↦ ‖f(x) + y‖ имеет локальный максимум на s в c.
LaTeX
$$$\\text{IsLocalMaxOn}(\\|f\\| \\circ f, s, c) \\land \\text{SameRay}(f(c), y) \\Rightarrow \\text{IsLocalMaxOn}(\\lambda x. \\|f(x) + y\\|, s, c)$$$
Lean4
/-- 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 norm_add_sameRay (h : IsLocalMaxOn (norm ∘ f) s c) (hy : SameRay ℝ (f c) y) :
IsLocalMaxOn (fun x => ‖f x + y‖) s c :=
IsMaxFilter.norm_add_sameRay h hy
