Documentation

IntroductoryLecturesOnConvexOptimization_Nesterov_2004.Chap01.Definition_1_6_4

source
def SatisfiesArmijoRule {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (stepSize : ℕ → ℝ) (x0 : E) (α β : ℝ) :
Prop

Definition 1.6.4: a step-size schedule hₖ satisfies the Armijo rule for the gradient-method trajectory started at x₀ when the objective is differentiable at every iterate, so the displayed ∇ f(xₖ) is genuine, 0 < α < β < 1, every step size is positive, and the consecutive iterates satisfy the two-sided Armijo decrease bounds.

Instances For
    source
    theorem SatisfiesArmijoRule.differentiableAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) (k : ℕ) :
    DifferentiableAt ℝ f (gradientMethod stepSize f x0 k)

    Along an Armijo trajectory, the objective is differentiable at every iterate.

    source
    theorem SatisfiesArmijoRule.hasGradientAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) (k : ℕ) :
    HasGradientAt f (gradient f (gradientMethod stepSize f x0 k)) (gradientMethod stepSize f x0 k)

    Along an Armijo trajectory, the displayed antigradient is the genuine gradient at every iterate.

    source
    theorem SatisfiesArmijoRule.alpha_pos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) :
    0 < α

    The Armijo rule forces the lower parameter to be positive.

    source
    theorem SatisfiesArmijoRule.alpha_lt_beta {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) :
    α < β

    The Armijo parameters satisfy α < β.

    source
    theorem SatisfiesArmijoRule.beta_lt_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) :
    β < 1

    The upper Armijo parameter lies below 1.

    source
    theorem SatisfiesArmijoRule.stepSize_pos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) (k : ℕ) :
    0 < stepSize k

    Every Armijo step size is positive.

    source
    theorem SatisfiesArmijoRule.bounds {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) (k : ℕ) :
    α * inner ℝ (gradient f (gradientMethod stepSize f x0 k)) (gradientMethod stepSize f x0 k - gradientMethod stepSize f x0 (k + 1)) ≤ f (gradientMethod stepSize f x0 k) - f (gradientMethod stepSize f x0 (k + 1)) ∧ f (gradientMethod stepSize f x0 k) - f (gradientMethod stepSize f x0 (k + 1)) ≤ β * inner ℝ (gradient f (gradientMethod stepSize f x0 k)) (gradientMethod stepSize f x0 k - gradientMethod stepSize f x0 (k + 1))

    The Armijo rule provides both comparison inequalities at each iterate.

    source
    theorem SatisfiesArmijoRule.lowerBound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) (k : ℕ) :
    α * inner ℝ (gradient f (gradientMethod stepSize f x0 k)) (gradientMethod stepSize f x0 k - gradientMethod stepSize f x0 (k + 1)) ≤ f (gradientMethod stepSize f x0 k) - f (gradientMethod stepSize f x0 (k + 1))

    The lower Armijo comparison inequality.

    source
    theorem SatisfiesArmijoRule.upperBound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {stepSize : ℕ → ℝ} {x0 : E} {α β : ℝ} (hArmijo : SatisfiesArmijoRule f stepSize x0 α β) (k : ℕ) :
    f (gradientMethod stepSize f x0 k) - f (gradientMethod stepSize f x0 (k + 1)) ≤ β * inner ℝ (gradient f (gradientMethod stepSize f x0 k)) (gradientMethod stepSize f x0 k - gradientMethod stepSize f x0 (k + 1))

    The upper Armijo comparison inequality.

    source
    theorem zero_zero_constOne_satisfiesArmijoRule {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] :
    SatisfiesArmijoRule (fun (x : E) => 0) (fun (x : ℕ) => 1) 0 (1 / 4) (1 / 2)

    The constant zero objective with initial point 0 and unit step sizes satisfies the Armijo rule for the canonical parameters α = 1 / 4 and β = 1 / 2.