IsLocalMaxOn.norm_add_self
theorem IsLocalMaxOn.norm_add_self :
∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : TopologicalSpace X] {f : X → E} {s : Set X} {c : X},
IsLocalMaxOn (norm ∘ f) s c → IsLocalMaxOn (fun x => ‖f x + f c‖) s c
This theorem states that if a function `f` from a type `X` to a type `E` has a local maximum of its norm on a set `s` at a point `c`, then the function which maps an element `x` to the norm of the sum of `f(x)` and `f(c)` also has a local maximum at `c` on `s`. Here, `E` is assumed to be a seminormed additive commutative group and a normed space over real numbers, and `X` is assumed to be a topological space. In mathematical terms, if we have $\|f(x)\| \leq \|f(c)\|$ for all `x` in a neighborhood of `c`, then we also have $\|f(x) + f(c)\| \leq \|f(c) + f(c)\|$ for all `x` in the same neighborhood.
More concisely: If `f` is a continuous function from a topological space `X` to a normed space `E` over real numbers, and `c` is a local maximum of the norm of `f` on a set `s` in `X`, then `c` is also a local maximum of the norm of `f(x) + f(c)` on `s`.
|
IsMaxFilter.norm_add_self
theorem IsMaxFilter.norm_add_self :
∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E}
{l : Filter α} {c : α}, IsMaxFilter (norm ∘ f) l c → IsMaxFilter (fun x => ‖f x + f c‖) l c
The theorem `IsMaxFilter.norm_add_self` states that for any function `f` from an arbitrary type `α` to a seminormed add commutative group `E` over the real numbers, if the composition of the `norm` function and `f` has a maximum value at a point `c` along a filter `l`, then the function that maps `x` to the norm of the sum of `f(x)` and `f(c)` also has a maximum along the same filter `l` at the same point `c`.
More concisely: If `f: α → E` is a function from type `α` to a seminormed add commutative group `E` over the real numbers, and `c ∈ α` is a point such that `∥f(c)∥ ≥ ∥f(x)∥∀x ∈ l`, then `x ↦ ∥f(x) + f(c)∥` has a maximum at `c` along filter `l`.
|
IsLocalMaxOn.norm_add_sameRay
theorem IsLocalMaxOn.norm_add_sameRay :
∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : TopologicalSpace X] {f : X → E} {s : Set X} {c : X} {y : E},
IsLocalMaxOn (norm ∘ f) s c → SameRay ℝ (f c) y → IsLocalMaxOn (fun x => ‖f x + y‖) s c
This theorem states that given a function `f : α → E`, if the composition of `norm` and `f` has a local maximum within a set `s` at a point `c`, and if a vector `y` is on the same ray as `f c` (which means that either `y` or `f c` is zero or some positive multiples of them are equal), then the function that maps `x` to the norm of the sum of `f x` and `y` also has a local maximum within the set `s` at the same point `c`. Here `E` is a seminormed add commutative group and a normed space over ℝ, and `X` is a topological space.
More concisely: If `f : X → E` has a local maximum of `norm (f x)` at `c ∈ s`, and `y ∈ E` is on the same ray as `f c`, then the function `x ↦ norm (f x + y)` also has a local maximum at `c` within `s`.
|
IsLocalMax.norm_add_self
theorem IsLocalMax.norm_add_self :
∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : TopologicalSpace X] {f : X → E} {c : X},
IsLocalMax (norm ∘ f) c → IsLocalMax (fun x => ‖f x + f c‖) c
The theorem `IsLocalMax.norm_add_self` states that for a function `f` from a topological space `X` to a semi-normed commutative group `E` which also has a normed real space structure, if the composition of `f` and the norm function has a local maximum at a point `c`, then the function `f` when applied to `x` and `c`, and then their results added and normed, also has a local maximum at `c`. In simpler terms, if the norm of `f` reaches a peak value at a certain point, then the norm of the sum of `f` applied to any point and `f` applied to this peak point also reaches a local maximum at this peak point.
More concisely: If `f: X → E` is a function from a topological space `X` to a semi-normed commutative group `E` with a normed real space structure, and `c ∈ X` is a point where the composition `∥f(c)∥` has a local maximum, then `∥f(x) + f(c)∥` has a local maximum at `c` for all `x ∈ X`.
|
IsLocalMax.norm_add_sameRay
theorem IsLocalMax.norm_add_sameRay :
∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : TopologicalSpace X] {f : X → E} {c : X} {y : E},
IsLocalMax (norm ∘ f) c → SameRay ℝ (f c) y → IsLocalMax (fun x => ‖f x + y‖) c
The theorem `IsLocalMax.norm_add_sameRay` states that for a function `f` mapping from some type `X` to a seminormed add commutative group `E` over the real numbers, if the composition of the norm function and `f` has a local maximum at a point `c` and `y` is a vector that is on the same ray as `f(c)`, then the function assigning to each `x` the norm of `f(x) + y` also has a local maximum at `c`. Here, two vectors are on the same ray if either one of them is zero or there exist positive multiples of them that are equal. In other words, this theorem is about how adding a vector that is on the same ray as the output of a function at a local maximum of the norm of the function's output does not change the location of the local maximum.
More concisely: If `f` is a function from type `X` to a seminormed add commutative group `E` over the real numbers, and the norm of `f(c)` has a local maximum at `c`, then the function assigning to each `x` the norm of `f(x) + y` also has a local maximum at `c`, where `y` is any vector on the same ray as `f(c)`.
|
IsMaxOn.norm_add_sameRay
theorem IsMaxOn.norm_add_sameRay :
∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E} {s : Set α}
{c : α} {y : E}, IsMaxOn (norm ∘ f) s c → SameRay ℝ (f c) y → IsMaxOn (fun x => ‖f x + y‖) s c
This theorem states that, given a function `f` from some type `α` to a seminormed add commutative group `E` (equipped with a structure of `NormedSpace` over `ℝ`), if the composition of `f` with the norm function has a maximum at a point `c` on a set `s`, and if a vector `y` lies on the same ray as the image of `c` under `f`, then the function that maps each `x` to the norm of the sum of `f(x)` and `y` also has a maximum at `c` on the set `s`.
In more mathematical terms, if `||f||` reaches its maximum value on `s` at `c` and `y` is a vector in the same direction as `f(c)`, then the function `x ↦ ||f(x) + y||` also reaches its maximum value on `s` at `c`.
More concisely: If `f: α → E` is a function from `α` to a normed space `E` over `ℝ`, `s ⊆ α`, `c ∈ s` is a point where `||f(c)|| = max {||f(x)|| : x ∈ s}`, and `y` is a vector in the same direction as `f(c)`, then `||f(x) + y||` achieves its maximum value at `c` within `s`.
|
IsMaxOn.norm_add_self
theorem IsMaxOn.norm_add_self :
∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E} {s : Set α}
{c : α}, IsMaxOn (norm ∘ f) s c → IsMaxOn (fun x => ‖f x + f c‖) s c
The theorem `IsMaxOn.norm_add_self` states that for any function `f` mapping elements from a type `α` to a type `E`, where `E` forms a semi-normed additive commutative group and also a normed space over the real numbers, if the composition of the `norm` function and `f` has a maximum on a set `s` at a point `c`, then the function defined by the norm of the sum of `f(x)` and `f(c)` also has a maximum on `s` at `c`. In simpler terms, if `f` achieves its maximum norm at some point `c`, then the norm of `f(x) + f(c)` also achieves its maximum at the same point `c` for all `x` in set `s`.
More concisely: If `f : α → E` maps a set `α` to a semi-normed additive commutative group `E` over the real numbers, and the norm of `f` attains its maximum at `c` in the set `s`, then the norm of `f(x) + f(c)` also achieves its maximum at `c` for all `x` in `s`.
|
IsMaxFilter.norm_add_sameRay
theorem IsMaxFilter.norm_add_sameRay :
∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E}
{l : Filter α} {c : α} {y : E},
IsMaxFilter (norm ∘ f) l c → SameRay ℝ (f c) y → IsMaxFilter (fun x => ‖f x + y‖) l c
This theorem states that if a function `f : α → E` has a property such that the norm of the function `f`, denoted as `norm ∘ f`, reaches a maximum at a specific point `c` in a filter `l`, and if a vector `y` is on the same ray as the value of the function at `c`, denoted as `f c`, then the function that computes the norm of the sum of `f x` and `y`, denoted as `fun x => ‖f x + y‖`, also has a maximum at the same point `c` in the filter `l`.
In other words, if the function `f` achieves its maximum norm at some point with respect to a filter, then adding a vector that is on the same ray as the function value at that point does not change the location of the maximum norm with respect to the filter.
More concisely: If a function `f : α → E` reaches the maximum norm at a point `c` in a filter `l`, then the function `x => ||f x + y||` also reaches the maximum norm at `c` for any vector `y` on the ray through `fc`.
|