Documentation

IntroductoryLecturesOnConvexOptimization_Nesterov_2004.Chap04.Definition_4_1_9

source
def GradientDominatedOn.UsesConstant {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : ℝ) (𝓕 : Set E) (f : E β†’ ℝ) (xStar : E) (Ο„f : ℝ) :
Prop

UsesConstant p 𝓕 f xStar Ο„f packages the unique differentiability of the feasible set, the canonical argmin membership of xStar, and the positive domination constant Ο„f used in the source-facing gradient-domination bound.

Instances For
    source
    class GradientDominatedOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : ℝ) (𝓕 : Set E) (f : E β†’ ℝ) :
    Prop

    Definition 4.1.9: a differentiable function f on a uniquely differentiable feasible set 𝓕 βŠ† ℝⁿ is gradient dominated of degree p ∈ [1, 2] when it has a global minimizer xStar on 𝓕 and a positive constant Ο„f such that f x - f xStar ≀ Ο„f * β€–gradientWithin f 𝓕 xβ€–^p for every x ∈ 𝓕. On open feasible sets, and in particular for 𝓕 = Set.univ, this agrees with the textbook ambient-gradient form.

    • differentiableOn : DifferentiableOn ℝ f 𝓕

      The function is differentiable on the feasible set.

    • degree_mem_Icc : p ∈ Set.Icc 1 2

      The degree of domination lies in the interval [1, 2].

    • exists_usesConstant : βˆƒ (xStar : E) (Ο„f : ℝ), UsesConstant p 𝓕 f xStar Ο„f

      The canonical minimizer set argmin[𝓕] f is nonempty, and one minimizer carries the unique-differentiability and positive-constant data needed for the source-facing gradient-domination inequality.

    Instances
      source
      theorem GradientDominatedOn.uniqueDiffOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} (hf : GradientDominatedOn p 𝓕 f) :
      UniqueDiffOn ℝ 𝓕
      source
      instance GradientDominatedOn.instFactAndDifferentiableOnRealUniqueDiffOnMemSetIccOfNat {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} [hf : GradientDominatedOn p 𝓕 f] :
      Fact (DifferentiableOn ℝ f 𝓕 ∧ UniqueDiffOn ℝ 𝓕 ∧ p ∈ Set.Icc 1 2)

      A GradientDominatedOn p 𝓕 f hypothesis canonically supplies the differentiability of f on 𝓕, the intrinsic within-gradient layer on 𝓕, and the admissible degree range p ∈ [1, 2].

      source
      theorem GradientDominatedOn.UsesConstant.uniqueDiffOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} {xStar : E} {Ο„f : ℝ} (hΟ„f : UsesConstant p 𝓕 f xStar Ο„f) :
      UniqueDiffOn ℝ 𝓕
      source
      theorem GradientDominatedOn.UsesConstant.mem_argmin {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} {xStar : E} {Ο„f : ℝ} (hΟ„f : UsesConstant p 𝓕 f xStar Ο„f) :
      xStar ∈ constrainedArgmin 𝓕 f
      source
      theorem GradientDominatedOn.UsesConstant.pos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} {xStar : E} {Ο„f : ℝ} (hΟ„f : UsesConstant p 𝓕 f xStar Ο„f) :
      0 < Ο„f
      source
      theorem GradientDominatedOn.UsesConstant.bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} {xStar : E} {Ο„f : ℝ} (hΟ„f : UsesConstant p 𝓕 f xStar Ο„f) {x : E} (hx : x ∈ 𝓕) :
      f x - f xStar ≀ Ο„f * β€–gradientWithin f 𝓕 xβ€–.rpow p
      source
      theorem GradientDominatedOn.UsesConstant.bound_eq_gradient_of_isOpen {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} {xStar x : E} {Ο„f : ℝ} (hΟ„f : UsesConstant p 𝓕 f xStar Ο„f) (hf : DifferentiableOn ℝ f 𝓕) (h𝓕_open : IsOpen 𝓕) (hx : x ∈ 𝓕) :
      f x - f xStar ≀ Ο„f * β€–gradient f xβ€–.rpow p

      On an open feasible set, the within-gradient bound from UsesConstant is exactly the textbook ambient-gradient bound.

      source
      theorem GradientDominatedOn.exists_usesConstant_of_mem_argmin {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} (hf : GradientDominatedOn p 𝓕 f) {xStar : E} (hxStar : xStar ∈ constrainedArgmin 𝓕 f) :
      βˆƒ (Ο„f : ℝ), UsesConstant p 𝓕 f xStar Ο„f

      Any point of the canonical minimizer set can be paired with some positive domination constant.

      source
      theorem GradientDominatedOn.argmin_nonempty {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {p : ℝ} {𝓕 : Set E} {f : E β†’ ℝ} (hf : GradientDominatedOn p 𝓕 f) :
      (constrainedArgmin 𝓕 f).Nonempty

      A gradient-dominated function has a nonempty canonical minimizer set on its feasible set.