theorem block_coordinate_descent_lemma_of_slice_smooth {ι : Type u} {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] (f : ((i : ι) → Ei i) → EReal) (block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i) (L : NNReal) (i : ι) [CompleteSpace (Ei i)] {x : (j : ι) → Ei j} (h_slice_convex : Convex ℝ {d : Ei i | x + Pi.single i d ∈ interior (effective_domain f)}) (h_slice_smooth : is_l_smooth_on (block_coordinate_slice f x i) {d : Ei i | x + Pi.single i d ∈ interior (effective_domain f)} L) (h_block_gradient_spec : HasGradientAt (block_coordinate_slice f x i) (block_gradient i x) 0) {d : Ei i} (hx : x ∈ interior (effective_domain f)) (hxd : x + Pi.single i d ∈ interior (effective_domain f)) : (f (x + Pi.single i d)).toReal ≤ (f x).toReal + inner ℝ (block_gradient i x) d + ↑L / 2 * ‖d‖ ^ 2

Bridge lemma for Lemma 11.2: fix a block index i and a base point x, and suppose the admissible one-block slice domain {d | x + 𝒰[i] d ∈ interior (effective_domain f)} is convex. If the i-th slice d ↦ f (x + 𝒰[i] d) is L-smooth on that admissible slice domain and has gradient block_gradient i x at d = 0, then the block update satisfies the quadratic upper model f (x + 𝒰[i] d) ≤ f x + ⟪block_gradient i x, d⟫ + (L / 2) ‖d‖² whenever both endpoints lie in interior (effective_domain f).

theorem IsBlockProximalGradientProblem.block_coordinate_slice_hasGradientAt {ι : Type u} {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [Fintype ι] {f : ((i : ι) → Ei i) → EReal} {g : (i : ι) → Ei i → EReal} {block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i} {XStar : Set ((i : ι) → Ei i)} {FOpt : ℝ} {Li : ι → ↑PosReal} (hproblem : IsBlockProximalGradientProblem f g block_gradient XStar FOpt Li) (i : ι) [CompleteSpace (Ei i)] {x : (j : ι) → Ei j} {d : Ei i} (hxd : x + Pi.single i d ∈ interior (effective_domain f)) : HasGradientAt (block_coordinate_slice f x i) (block_gradient i (x + Pi.single i d)) d

Re-centering the one-block slice at d identifies its gradient with the Chapter 11 block gradient at the updated point x + 𝒰[i] d.

theorem IsBlockProximalGradientProblem.block_coordinate_slice_is_l_smooth_on {ι : Type u} {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [Fintype ι] {f : ((i : ι) → Ei i) → EReal} {g : (i : ι) → Ei i → EReal} {block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i} {XStar : Set ((i : ι) → Ei i)} {FOpt : ℝ} {Li : ι → ↑PosReal} (hproblem : IsBlockProximalGradientProblem f g block_gradient XStar FOpt Li) (i : ι) [CompleteSpace (Ei i)] {x : (j : ι) → Ei j} : is_l_smooth_on (block_coordinate_slice f x i) {d : Ei i | x + Pi.single i d ∈ interior (effective_domain f)} (PosReal.toNNReal (Li i))

The Chapter 11 block-Lipschitz owner implies that the frozen one-block slice is L_i-smooth on its natural admissible domain.

theorem BlockProximalGradientAssumptions.block_coordinate_slice_domain_convex {ι : Type u} {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [Fintype ι] {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} (hproblem : BlockProximalGradientAssumptions f g block_gradient XStar FOpt Lf Li) (i : ι) {x : (j : ι) → Ei j} : Convex ℝ {d : Ei i | x + Pi.single i d ∈ interior (effective_domain f)}

The admissible one-block slice domain is convex under the Chapter 11 standing assumptions.

theorem BlockProximalGradientAssumptions.block_coordinate_descent_lemma {ι : Type u} {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [Fintype ι] {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} (hproblem : BlockProximalGradientAssumptions f g block_gradient XStar FOpt Lf Li) (i : ι) [CompleteSpace (Ei i)] {x : (j : ι) → Ei j} {d : Ei i} (hx : x ∈ interior (effective_domain f)) (hxd : x + Pi.single i d ∈ interior (effective_domain f)) : (f (x + Pi.single i d)).toReal ≤ (f x).toReal + inner ℝ (block_gradient i x) d + ↑(Li i) / 2 * ‖d‖ ^ 2

Lemma 11.2: under Definition 11.4, the textbook one-block update satisfies the quadratic upper model with the corresponding block Lipschitz constant L_i.