def
IsStrictLocalMin
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_2}
[Preorder α]
(f : X → α)
(xStar : X)
:
A strict local minimizer is a point whose function value is strictly smaller than the value at every distinct nearby point.
Instances For
theorem
isStrictLocalMin_iff
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_2}
[Preorder α]
(f : X → α)
(xStar : X)
:
IsStrictLocalMin f xStar ↔ ∀ᶠ (x : X) in nhdsWithin xStar {xStar}ᶜ, f xStar < f x
Unfolding formula for IsStrictLocalMin.
theorem
IsStrictLocalMin.isLocalMin
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_2}
[Preorder α]
{f : X → α}
{xStar : X}
(h : IsStrictLocalMin f xStar)
:
IsLocalMin f xStar
A strict local minimizer is, in particular, a local minimizer.
theorem
isStrictLocalMin_iff_exists_forall_mem_ball
{X : Type u_1}
[PseudoMetricSpace X]
{α : Type u_2}
[Preorder α]
(f : X → α)
(xStar : X)
:
IsStrictLocalMin f xStar ↔ ∃ δ > 0, ∀ ⦃x : X⦄, x ∈ Metric.ball xStar δ → x ≠ xStar → f xStar < f x
Metric bridge for IsStrictLocalMin: in a pseudometric space, strict local minimality is
equivalent to the punctured-ball inequality from the source text.
theorem
isLocalMin_iff_exists_forall_norm_sub_lt
{X : Type u_1}
[SeminormedAddCommGroup X]
{α : Type u_2}
[Preorder α]
(f : X → α)
(xStar : X)
:
IsLocalMin f xStar ↔ ∃ δ > 0, ∀ (x : X), ‖x - xStar‖ < δ → f xStar ≤ f x
Normed-group bridge for Definition 1.4.1 (1): IsLocalMin is equivalent to the
source's norm-ball inequality.
theorem
isStrictLocalMin_iff_exists_forall_norm_sub_lt
{X : Type u_1}
[SeminormedAddCommGroup X]
{α : Type u_2}
[Preorder α]
(f : X → α)
(xStar : X)
:
IsStrictLocalMin f xStar ↔ ∃ δ > 0, ∀ (x : X), x ≠ xStar → ‖x - xStar‖ < δ → f xStar < f x
Normed-group bridge for Definition 1.4.1 (2): the canonical strict local-minimum owner is exactly the source's punctured norm-ball inequality.