Documentation

FirstOrderMethodsOptimization_Beck_2017.Chap10.Theorem_10_72

theorem non_euclidean_proximal_gradient_objective_values_antitone {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.ConstantOrBacktrackingB5StepsizeRule x L) :
Antitone fun (k : ) => composite_model_objective f g (x k)

Theorem 10.72 (1): clause (a). Under the displayed g-regularity, smoothness, domain, and Bregman-potential hypotheses, if the non-Euclidean proximal-gradient trajectory uses either the constant stepsize rule L_k = L_f or backtracking procedure B5, then the objective sequence F(x^k) is nonincreasing.

theorem finite_linear_term_is_convex_function {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] (ell : E →L[] ) (c : ) :
is_convex_function fun (u : E) => (c * ell u)

Helper for Theorem 10.72: a finite linear term is convex as an extended-real-valued function.

@[reducible, inline]
noncomputable abbrev non_euclidean_scaled_linearized_objective {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] (f g : EEReal) (x : E) (L : PosReal) (n : ) :
EEReal

Helper for Theorem 10.72: the source linearized objective u ↦ (⟨∇f(x^n), u⟩ + g(u)) / L_n appearing in (10.u400), before the Bregman term is added back.

Instances For
    theorem non_euclidean_scaled_linearized_objective_effective_domain_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :

    Helper for Theorem 10.72: adding the finite linearization term u ↦ ⟪∇f(x^n), u⟫ / L_n does not change the effective domain of the scaled penalty, so the source linearized objective has the same effective domain as g.

    theorem non_euclidean_scaled_linearized_objective_proper_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :

    Helper for Theorem 10.72: the source linearized objective is proper and convex, so it can be used as the ψ_n input of Theorem 9.12 on the exact textbook route.

    theorem non_euclidean_convex_support_toReal_at_basepoint {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f : EEReal} (hf_convex : is_convex_function f) (hf_ne_bot : ∀ (z : E), f z ) {xBase y : E} (hxBase : xBase effective_domain f) (hxDiff : DifferentiableAt (fun (z : E) => (f z).toReal) xBase) (hy : y effective_domain f) :
    (f y).toReal (f xBase).toReal + inner (gradient (fun (z : E) => (f z).toReal) xBase) (y - xBase)

    Helper for Theorem 10.72: convexity of the smooth term gives the supporting-hyperplane inequality for the finite-valued restriction x ↦ (f x).toReal at a differentiability point.

    theorem non_euclidean_successor_le_textbook_model {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.ConstantOrBacktrackingB5StepsizeRule x L) (n : ) (u : E) :
    composite_model_objective f g (x (n + 1)) non_euclidean_textbook_model f g ω (x n) (L n) u

    Helper for Theorem 10.72: the accepted upper-model inequality together with the minimizing property of the realized step bounds the successor objective by the textbook model at any comparator u. This is the source (10.94) and (10.u399) package.

    theorem non_euclidean_textbook_model_le_objective_add_bregman {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) {n : } {u : E} (hu : u effective_domain g), non_euclidean_textbook_model f g ω (x n) (L n) u composite_model_objective f g u + ((L n) * B[ω] u (x n))

    Helper for Theorem 10.72: convexity of f replaces the local linear model at a comparator by the true objective value, leaving only the Bregman penalty. This is the source passage from m(u, x^n) to f(u).

    theorem non_euclidean_objective_gap_nonneg {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ (n : ), FOpt composite_model_objective f g (x n)

    Helper for Theorem 10.72: the optimal value is a lower bound for every objective value along the non-Euclidean proximal-gradient trajectory.

    theorem non_euclidean_optimizer_mem_effective_domain_g {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {xStar : E} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ (hxStar : xStar XStar), xStar effective_domain g

    Helper for Theorem 10.72: every optimizer has finite nonsmooth value, so it belongs to effective_domain g.

    theorem non_euclidean_successor_minimizes_scaled_bregman_objective {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {x : E} {L : PosReal} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (n : ) :
    IsMinOn (secondProxObjective (non_euclidean_scaled_linearized_objective f g x L n) ω (x n)) Set.univ (x (n + 1))

    Helper for Theorem 10.72: the realized next iterate minimizes exactly the Chapter 9 objective ψ_n(·) + B_ω(·, x^n) used in the source proof of clause (b).

    theorem non_euclidean_three_point_add_form {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {x : E} {L : PosReal} (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (n : ) (u : E) :
    inner (gradient (fun (z : E) => (ω z).toReal) (x n) - gradient (fun (z : E) => (ω z).toReal) (x (n + 1))) (u - x (n + 1)) + B[ω] u (x n) = B[ω] u (x (n + 1)) + B[ω] (x (n + 1)) (x n)

    Helper for Theorem 10.72: the source three-point identity for the Chapter 10 iterates can be rewritten directly in add form, so the Chapter 9 optimality inequality can be normalized without passing through an EReal subtraction chain.

    theorem psi_n_second_prox_three_point_bridge {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (n : ) {u : E} (hu : u effective_domain g), non_euclidean_scaled_linearized_objective f g x L n (x (n + 1)) + (B[ω] u (x (n + 1)) + B[ω] (x (n + 1)) (x n)) non_euclidean_scaled_linearized_objective f g x L n u + (B[ω] u (x n))

    Helper for Theorem 10.72: apply the source second-prox segment argument to the linearized objective (m(·, x^n) + g) / L_n. The trajectory already provides successor membership in dom(∂ω), so no generic exact-sum-rule qualification is needed, and the result has the plus form of equation (10.96) in scaled_bregman_objective language.

    theorem non_euclidean_scaled_objective_successor_add_bregman_le_comparator {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (n : ) {u : E} (hu : u effective_domain g), scaled_bregman_objective f g ω (x n) (L n) (x (n + 1)) + (B[ω] u (x (n + 1))) scaled_bregman_objective f g ω (x n) (L n) u

    Helper for Theorem 10.72: expose the source second-prox segment comparison for (m(·, x^n) + g) / L_n in the chapter's scaled_bregman_objective notation.

    theorem non_euclidean_B5_accepts_of_stepsize_ge_Lf {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ [IsProperExtendedRealFunction g] [Fact (LowerSemicontinuous g)] [Fact (is_convex_function g)] [ : IsBregmanPotentialOn ω (effective_domain g) 1] (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (n : ) (Lbar : PosReal) (hLbar : Lf Lbar), non_euclidean_proximal_gradient_backtracking_B5_accepts f g ω Lbar (x n)

    Helper for Theorem 10.72: any trial curvature Lbar ≥ L_f is accepted by the B5 upper-model test at the current non-Euclidean proximal-gradient iterate.

    theorem non_euclidean_B5_local_stepsize_bounds {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ [IsProperExtendedRealFunction g] [Fact (LowerSemicontinuous g)] [Fact (is_convex_function g)] [ : IsBregmanPotentialOn ω (effective_domain g) 1] (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) {s : PosReal} {η : ProximalGradientBacktrackingGrowthFactor} (hB5 : UsesNonEuclideanProximalGradientBacktrackingB5Rule f g ω x L s η) (n : ), have LPrev := proximal_gradient_backtracking_B2_previous_stepsize s L n; LPrev (L n) (L n) max (η * Lf) LPrev

    Helper for Theorem 10.72: under B5, the chosen curvature sits between the previous trial curvature and max {η L_f, L_prev}.

    theorem non_euclidean_alpha_mul_lf_eq_max_stepsize {Lf : NNReal} {α : } {s : PosReal} {η : ProximalGradientBacktrackingGrowthFactor} (hLf : 0 < Lf) ( : α = max (↑η) (s / Lf)) :
    max (η * Lf) s = α * Lf

    Helper for Theorem 10.72: if α = max {η, s / L_f} with L_f > 0, then α L_f = max {η L_f, s}.

    theorem non_euclidean_sublinear_rate_alpha_pos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) :
    0 < α

    Helper for Theorem 10.72: the non-Euclidean sublinear-rate owner forces the rate constant α to be positive.

    theorem non_euclidean_stepsize_control {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } ( : IsBregmanPotentialOn ω (effective_domain g) 1) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) (n : ) :
    (L n) α * Lf

    Helper for Theorem 10.72: every admissible constant/B5 stepsize satisfies the uniform bound L_n ≤ α L_f.

    theorem non_euclidean_objective_eq_real_of_mem_effective_domain {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ {z : E} (hz : z effective_domain g), composite_model_objective f g z = ((f z).toReal + (g z).toReal)

    Helper for Theorem 10.72: on effective_domain g, the composite objective is a finite real sum of the finite f- and g-values.

    theorem non_euclidean_objective_eq_coe_toReal_of_mem_effective_domain {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ {z : E} (hz : z effective_domain g), composite_model_objective f g z = (composite_model_objective f g z).toReal

    Helper for Theorem 10.72: on effective_domain g, the objective value itself is the cast of its toReal value.

    theorem non_euclidean_iterate_mem_effective_domain {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {x : E} {L : PosReal} (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) {n : } (hn : 1 n) :

    Helper for Theorem 10.72: every positive non-Euclidean proximal-gradient iterate lies in effective_domain g.

    theorem non_euclidean_positive_iterate_gap_coe {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) {n : } (hn : 1 n), ((composite_model_objective f g (x n)).toReal - FOpt) = composite_model_objective f g (x n) - FOpt

    Helper for Theorem 10.72: every positive-index objective gap is finite, so its real value casts back to the displayed EReal gap F(x^n) - F_opt.

    theorem non_euclidean_positive_iterate_gap_nonneg {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} :
    IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf∀ (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) {n : } (hn : 1 n), 0 (composite_model_objective f g (x n)).toReal - FOpt

    Helper for Theorem 10.72: every positive-index objective gap is nonnegative as a real number.

    theorem non_euclidean_textbook_successor_add_scaled_bregman_le_optimizer {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } {xStar : E} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) (hxStar : xStar XStar) (n : ) :
    composite_model_objective f g (x (n + 1)) + ((L n) * B[ω] xStar (x (n + 1))) composite_model_objective f g xStar + ((L n) * B[ω] xStar (x n))

    Helper for Theorem 10.72: rewrite the stabilized Chapter 9 comparator directly into the textbook finite-EReal one-step inequality F(x^(n+1)) + L_n B_ω(x*, x^(n+1)) ≤ F(x*) + L_n B_ω(x*, x^n).

    theorem non_euclidean_one_step_gap_le_scaled_bregman_drop {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } {xStar : E} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) (hxStar : xStar XStar) (n : ) :
    (composite_model_objective f g (x (n + 1))).toReal - FOpt (L n) * (B[ω] xStar (x n) - B[ω] xStar (x (n + 1)))

    Helper for Theorem 10.72: route correction for clause (b). After the Chapter 9 comparator has been stabilized, convert it to the textbook one-step gap drop F(x^(n+1)) - F_opt ≤ L_n (B_ω(x*, x^n) - B_ω(x*, x^(n+1))).

    theorem non_euclidean_one_step_gap_div_le_bregman_drop {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } {xStar : E} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) (hxStar : xStar XStar) (n : ) :
    ((composite_model_objective f g (x (n + 1))).toReal - FOpt) / (α * Lf) B[ω] xStar (x n) - B[ω] xStar (x (n + 1))

    Helper for Theorem 10.72: dividing the one-step drop by the source denominator α L_f produces the textbook normalized gap inequality (10.100).

    theorem non_euclidean_real_prefix_telescope {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } {xStar : E} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) (hxStar : xStar XStar) (K : ) :
    iFinset.range (K + 1), ((composite_model_objective f g (x (i + 1))).toReal - FOpt) / (α * Lf) + B[ω] xStar (x (K + 1)) B[ω] xStar (x 0)

    Helper for Theorem 10.72: summing the normalized one-step inequalities telescopes the Bregman terms exactly as in (10.102).

    theorem non_euclidean_proximal_gradient_objective_gap_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] {f g ω : EEReal} {XStar : Set E} {FOpt : } {Lf : NNReal} [hproblem : IsConvexCompositeSmoothMinimizationProblem f g XStar FOpt Lf] {x : E} {L : PosReal} {α : } {xStar : E} ( : IsBregmanPotentialOn ω (effective_domain g) 1) (hω_diff : zsubdifferential_domain ω, DifferentiableAt (fun (w : E) => (ω w).toReal) z) (htraj : is_non_euclidean_proximal_gradient_trajectory f g ω x L) (hrule : hproblem.NonEuclideanSublinearRateStepsizeRule x L α) (hxStar : xStar XStar) (k : ) (hk : 1 k) :
    composite_model_objective f g (x k) - FOpt (α * Lf * B[ω] xStar (x 0) / k)

    Theorem 10.72 (2): clause (b). Under the same assumptions as clause (1), every positive iterate satisfies the non-Euclidean sublinear objective-gap estimate F(x^k) - F_opt ≤ α L_f B[ω] x* x^0 / k for every optimizer x* ∈ X^*.