def SublevelDistanceToEachOptimalPointBound {ι : Type u} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] (f : ((i : ι) → Ei i) → EReal) (g : (i : ι) → Ei i → EReal) (XStar : Set ((i : ι) → Ei i)) (α Rα : ↑PosReal) : Prop

A radius Rα bounds the positive α-sublevel of the Chapter 11 composite objective relative to every optimal point if every x with F x ≤ α stays within distance at most Rα of each xStar ∈ XStar.

theorem SublevelDistanceToEachOptimalPointBound.apply {ι : Type u} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] {f : ((i : ι) → Ei i) → EReal} {g : (i : ι) → Ei i → EReal} {XStar : Set ((i : ι) → Ei i)} {α Rα : ↑PosReal} (h : SublevelDistanceToEachOptimalPointBound f g XStar α Rα) {x xStar : (i : ι) → Ei i} (hx : composite_model_objective f (separableSum g) x ≤ ↑↑α) (hxStar : xStar ∈ XStar) : ‖x - xStar‖ ≤ ↑Rα

class CyclicBlockProximalGradientConvexAssumptions {ι : Type u} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] (f : ((i : ι) → Ei i) → EReal) (g : (i : ι) → Ei i → EReal) (block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i) (XStar : Set ((i : ι) → Ei i)) (FOpt : ℝ) (Lf : NNReal) (Li : ι → ↑PosReal) extends BlockProximalGradientAssumptions f g block_gradient XStar FOpt Lf Li : Prop

Theorem 11.6: in the convex case of the cyclic block proximal gradient method, the standing Chapter 11 block proximal-gradient assumptions are supplemented by (A) convexity of the smooth term f and (B) the requirement that every positive sublevel set of the composite objective F(x) = f(x) + ∑ i, g_i(x_i) stays within a uniformly bounded distance of every optimal point x* ∈ X^*: for each α > 0 there is Rα > 0 such that F(x) ≤ α implies ‖x - x*‖ ≤ Rα for all x* ∈ X^*. The weaker infDist reformulation is derived below as a bridge theorem, but it is not the primitive source-facing field.

• f_ne_bot (x : (i : ι) → Ei i) : f x ≠ ⊥
• block_g_proper (i : ι) : IsProperExtendedRealFunction (g i)
• block_g_closed (i : ι) : LowerSemicontinuous (g i)
• block_g_convex (i : ι) : is_convex_function (g i)
• f_closed : LowerSemicontinuous f
• g_effective_domain_subset_interior_f_effective_domain : effective_domain (separableSum g) ⊆ interior (effective_domain f)
• optimal_set_eq : XStar = unconstrained_problem_solutions (composite_model_objective f (separableSum g))
• optimal_set_nonempty : XStar.Nonempty
• optimal_value_isGLB : IsGLB (Set.range (composite_model_objective f (separableSum g))) ↑FOpt
• block_partial_gradient_spec (i : ι) {x : (i : ι) → Ei i} (hx : x ∈ interior (effective_domain f)) : HasFDerivAt (block_coordinate_slice f x i) ((InnerProductSpace.toDualMap ℝ (Ei i)) (block_gradient i x)) 0
• block_partial_gradient_lipschitz (i : ι) {x : (i : ι) → Ei i} {d : Ei i} (hx : x ∈ interior (effective_domain f)) (hxd : block_coordinate_update x i d ∈ interior (effective_domain f)) : ‖block_gradient i x - block_gradient i (block_coordinate_update x i d)‖ ≤ ↑(Li i) * ‖d‖
• f_effective_domain_convex : Convex ℝ (effective_domain f)
• f_toReal_smooth_on_interior_effective_domain : is_l_smooth_on (fun (x : (i : ι) → Ei i) => (f x).toReal) (interior (effective_domain f)) Lf
• f_convex : is_convex_function f
• bounded_sublevel_distance_to_each_optimal_point (α : ↑PosReal) : ∃ (Rα : ↑PosReal), SublevelDistanceToEachOptimalPointBound f g XStar α Rα

theorem CyclicBlockProximalGradientConvexAssumptions.bounded_sublevel_distance_to_optimal_set {ι : Type u} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] {Lf : NNReal} {Li : ι → ↑PosReal} {f : ((i : ι) → Ei i) → EReal} {g : (i : ι) → Ei i → EReal} {block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i} {XStar : Set ((i : ι) → Ei i)} {FOpt : ℝ} (h : CyclicBlockProximalGradientConvexAssumptions f g block_gradient XStar FOpt Lf Li) (α : ↑PosReal) : ∃ (Rα : ↑PosReal), ∀ ⦃x : (i : ι) → Ei i⦄, composite_model_objective f (separableSum g) x ≤ ↑↑α → Metric.infDist x XStar ≤ ↑Rα

The source-facing pairwise sublevel bound in Theorem 11.6 implies the weaker canonical distance-to-set estimate used in later convergence proofs.

theorem CyclicBlockProximalGradientConvexAssumptions.bounded_initial_sublevel_distance_to_optimal_set {ι : Type u} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] {Lf : NNReal} {Li : ι → ↑PosReal} {f : ((i : ι) → Ei i) → EReal} {g : (i : ι) → Ei i → EReal} {block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i} {XStar : Set ((i : ι) → Ei i)} {FOpt : ℝ} (h : CyclicBlockProximalGradientConvexAssumptions f g block_gradient XStar FOpt Lf Li) {x0 : (i : ι) → Ei i} {α : ↑PosReal} (hx0 : composite_model_objective f (separableSum g) x0 ≤ ↑↑α) : ∃ (Rα : ↑PosReal), ∀ ⦃x : (i : ι) → Ei i⦄, composite_model_objective f (separableSum g) x ≤ composite_model_objective f (separableSum g) x0 → Metric.infDist x XStar ≤ ↑Rα

If the initial objective value is bounded by a positive level α, then the same radius from Definition 11.6 controls the whole initial sublevel set {x | F x ≤ F x0} in the weaker distance-to-optimal-set form used later in the convergence analysis.