Observable upper-model, gradient, cocoercivity, interpolation, and descent inequalities.

noncomputable def V7.BregmanRemainder {d : ℕ} (oracle : PairOracle d) (x y : Point d) : ℝ

The objective's linearization error at x, based at y.

Equations

• V7.BregmanRemainder oracle x y = oracle.value x - oracle.value y - V7.pairing (oracle.gradient y) (x - y)

noncomputable def V7.UpperModelGuard {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (x y : Point d) : Prop

The quadratic upper model with estimate M bounds the objective at y.

Equations

• V7.UpperModelGuard p M oracle x y = (oracle.value y ≤ oracle.value x + V7.pairing (oracle.gradient x) (y - x) + M / 2 * V7.lpNorm p (y - x) ^ 2)

noncomputable def V7.GradientGuard {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (x y : Point d) : Prop

The two observed gradients satisfy the proposed Lipschitz bound in the dual norm.

Equations

• V7.GradientGuard p M oracle x y = (V7.lpNorm (V7.conjugateExponent p) (oracle.gradient y - oracle.gradient x) ≤ M * V7.lpNorm p (y - x))

noncomputable def V7.CocoercivityGuard {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (x y : Point d) : Prop

Exact current orientation: D_f(x,y) uses the gradient at y.

Equations

• V7.CocoercivityGuard p M oracle x y = (V7.BregmanRemainder oracle x y ≥ V7.lpNorm (V7.conjugateExponent p) (oracle.gradient x - oracle.gradient y) ^ 2 / (2 * M))

noncomputable def V7.EuclideanInterpolationGuard {d : ℕ} (M : ℝ) (oracle : PairOracle d) (xi xj : Point d) : Prop

The observed Euclidean Bregman gap dominates the squared gradient difference.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.TerminalDescentGuard {d : ℕ} (M : ℝ) (oracle : PairOracle d) (u v : Point d) : Prop

The terminal gradient step achieves the decrease predicted by the smoothness estimate.

Equations

• V7.TerminalDescentGuard M oracle u v = (oracle.value v ≤ oracle.value u - V7.lpNorm 2 (oracle.gradient u) ^ 2 / (2 * M))

inductive V7.ObservableGuardKind : Type

The observable inequalities that a local trial may check.

• upperModel : ObservableGuardKind
• gradient : ObservableGuardKind
• cocoercivity : ObservableGuardKind
• interpolation : ObservableGuardKind
• terminalDescent : ObservableGuardKind

@[instance_reducible]

instance V7.instDecidableEqObservableGuardKind : DecidableEq ObservableGuardKind

Equations

• V7.instDecidableEqObservableGuardKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure V7.ObservableGuardFailure (d : ℕ) : Type

The kind and pair of points witnessing a failed observable guard.

• kind : ObservableGuardKind

  The inequality that failed.

• x : Point d

  The first point of the failed guard.

• y : Point d

  The second point of the failed guard.

noncomputable def V7.GuardFails {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (w : ObservableGuardFailure d) : Prop

The selected observable inequality fails for the supplied oracle and estimates.

Equations

• One or more equations did not get rendered due to their size.