Documentation

FirstOrderMethodsOptimization_Beck_2017.Chap14.Lemma_14_4.InactiveBlockSupport

theorem twoBlockCurrentX2ObjectiveIsMinOn {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) (x1 : E1) (x2 : E2) (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (n : ) :
IsMinOn (two_block_alternating_minimization_x2_objective (Function.toEReal f) g1 g2 (x1 n)) Set.univ (x2 n)

Helper for Lemma 14.4 InactiveBlockSupport helper: the current second block is always an exact minimizer of the current x₂-subproblem.

theorem twoBlockIteratesMemEffectiveDomainAndInitialSublevel {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) (x1 : E1) (x2 : E2) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (n : ) :

Helper for Lemma 14.4 InactiveBlockSupport helper: every outer iterate of the two-block trajectory remains in effective_domain F, and the full objective never exceeds its initial value.

Helper for Lemma 14.4 InactiveBlockSupport helper: the intermediate half-step x^{k+1/2} = (x₁^{k+1}, x₂^k) is finite and lies below the initial objective level.

theorem convexRealSupportUnivFDeriv {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {φ : E} {x y : E} (hφ_convex : ConvexOn Set.univ φ) (hφ_diff : DifferentiableAt φ x) :
φ y φ x + (fderiv φ x) (y - x)

Helper for Lemma 14.4 InactiveBlockSupport helper: a convex differentiable real-valued function on Set.univ satisfies the first-order support inequality in fderiv form.

theorem partialInfimumSupportAtFixedPointOfAttainedPairSupport {E V : Type u} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup V] [NormedSpace V] (H : E × VEReal) (x0 : E) (v0 : V) (y : E) (g : Module.Dual E) (hattained : sInf (Set.range fun (v : V) => H (x0, v)) = H (x0, v0)) (hsupport : ∀ (v : V), H (y, v) H (x0, v0) + (g (y - x0))) :
sInf (Set.range fun (v : V) => H (y, v)) sInf (Set.range fun (v : V) => H (x0, v)) + (g (y - x0))

Helper for Lemma 14.4 InactiveBlockSupport helper: once a supporting affine lower bound is known for every point in a fixed target fiber, the same bound descends to the corresponding partial infimum.

theorem convexContactSupportAtTouchedConvexMajorant {E : Type u} [NormedAddCommGroup E] [InnerProductSpace E] [ProperSpace E] {eta : EEReal} {chi : E} {x0 y : E} (heta_convex : is_convex_function eta) (hchi_convex : ConvexOn Set.univ chi) (heta_le_chi : ∀ (x : E), eta x (chi x)) (hcontact : eta x0 = (chi x0)) (hchi_diff : DifferentiableAt chi x0) :
eta y eta x0 + (inner (gradient chi x0) (y - x0))

Helper for Lemma 14.4 InactiveBlockSupport helper: if a convex extended-real-valued function is touched from above at x0 by a convex differentiable real-valued majorant, then the gradient of that majorant supports the convex function at every comparison point.

theorem twoBlockFirstPenaltyEqCoeToRealOfMemEffectiveDomain {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] {y : E1 × E2} (hy : y effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :
(g1 y.1).toReal = g1 y.1

Helper for Lemma 14.4 InactiveBlockSupport helper: finiteness of the full objective at a pair forces finiteness of the first penalty term at the same point.

theorem twoBlockSecondPenaltyEqCoeToRealOfMemEffectiveDomain {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] {y : E1 × E2} (hy : y effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :
(g2 y.2).toReal = g2 y.2

Helper for Lemma 14.4 InactiveBlockSupport helper: finiteness of the full objective at a pair forces finiteness of the second penalty term at the same point.

theorem twoBlockFirstPenaltyMemEffectiveDomainOfObjectiveMem {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] {y : E1 × E2} (hy : y effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :
y.1 effective_domain g1

Helper for Lemma 14.4 InactiveBlockSupport helper: finiteness of the full objective at a pair puts the first penalty term in its effective domain.

theorem twoBlockSecondPenaltyMemEffectiveDomainOfObjectiveMem {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] {y : E1 × E2} (hy : y effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :
y.2 effective_domain g2

Helper for Lemma 14.4 InactiveBlockSupport helper: finiteness of the full objective at a pair puts the second penalty term in its effective domain.

theorem twoBlockX1FrozenSliceSupportAtCurrentSecondBlock {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) {L1 : PosReal} (hf_x1_convex : ConvexOn Set.univ fun (y1 : E1) => f (y1, x2 k)) (hf_x1_smooth : is_l_smooth_on (fun (y1 : E1) => f (y1, x2 k)) Set.univ (PosReal.toNNReal L1)) (y1 : E1) :
f (y1, x2 k) f (x1 k, x2 k) + (fderiv (fun (y1 : E1) => f (y1, x2 k)) (x1 k)) (y1 - x1 k)

Helper for Lemma 14.4 InactiveBlockSupport helper: convexity of the frozen smooth slice gives its first-order support inequality at the current first block.

theorem twoBlockX1PartialInfimumEqCurrentObjective {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) :

Helper for Lemma 14.4 InactiveBlockSupport helper: exact minimization of the current second block identifies the first partial infimum φ₁(x₁^k) with the current objective value.

theorem twoBlockX1PartialInfimumEqOptimalObjective {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :

Helper for Lemma 14.4 InactiveBlockSupport helper: global optimality of xStar identifies the fiber infimum φ₁(xStar.1) with the full objective value F xStar.

theorem twoBlockX1InactiveMarginalEqCurrentValue {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :
twoBlockX1InactiveMarginal f g2 (x1 k) = (f (x1 k, x2 k)) + g2 (x2 k)

Helper for Lemma 14.4 InactiveBlockSupport helper: once the current iterate is finite, the inactive marginal η₁(y₁) = inf_z₂ (f(y₁, z₂) + g₂(z₂)) is attained at the current second block.

theorem twoBlockX1InactiveMarginalLeOptimalWitness {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (xStar : E1 × E2) :
twoBlockX1InactiveMarginal f g2 xStar.1 (f xStar) + g2 xStar.2

Helper for Lemma 14.4 InactiveBlockSupport helper: the optimizer's second block is one witness for the inactive marginal at xStar.1.

theorem twoBlockX1InactiveMarginalAddActivePenaltyEqCurrentObjective {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :

Helper for Lemma 14.4 InactiveBlockSupport helper: reattaching the active penalty to the current inactive marginal recovers the full current objective value.

theorem twoBlockX1InactiveMarginalAddActivePenaltyLeObjectiveAtStar {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (xStar : E1 × E2) :

Helper for Lemma 14.4 InactiveBlockSupport helper: reattaching the active penalty to the optimizer witness bounds the inactive marginal by the full objective at xStar.

theorem twoBlockX1InactiveMarginalSupportAtStar {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) {L1 : PosReal} [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] [Fact (is_convex_function g2)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x1_smooth : is_l_smooth_on (fun (y1 : E1) => f (y1, x2 k)) Set.univ (PosReal.toNNReal L1)) (xStar : E1 × E2) :
twoBlockX1InactiveMarginal f g2 xStar.1 twoBlockX1InactiveMarginal f g2 (x1 k) + (inner (gradient (fun (y1 : E1) => f (y1, x2 k)) (x1 k)) (xStar.1 - x1 k))

Helper for Lemma 14.4 InactiveBlockSupport helper: the current second-block fiber is a convex touching majorant of the first inactive marginal, so η₁ inherits the frozen-slice first-order support inequality at xStar.1.

theorem twoBlockX1ProxCandidateAffineUpperBoundAtStar {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) (L1 : PosReal) [IsProperExtendedRealFunction g1] [Fact (LowerSemicontinuous g1)] [Fact (is_convex_function g1)] [IsProperExtendedRealFunction g2] [Fact (is_convex_function g2)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x1_smooth : is_l_smooth_on (fun (y1 : E1) => f (y1, x2 k)) Set.univ (PosReal.toNNReal L1)) (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :
have xPlus := prox_gradient_operator (fun (y1 : E1) => f (y1, x2 k)) g1 L1 (x1 k); have Gk := prox_gradient_mapping (fun (y1 : E1) => f (y1, x2 k)) g1 L1 (x1 k); have quad := L1 / 2 * xPlus - x1 k ^ 2; two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (xPlus, x2 k) two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar + (inner Gk (xPlus - xStar.1)) + quad

Helper for Lemma 14.4 InactiveBlockSupport helper: the prox-gradient candidate on the current x₁-slice should already satisfy the full optimizer gap bound. This is the remaining x₁-side structural blocker after the exact-step comparison has been isolated.

theorem twoBlockX1ProxCandidateGapLeGradientMapping {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) (L1 : PosReal) [IsProperExtendedRealFunction g1] [Fact (LowerSemicontinuous g1)] [Fact (is_convex_function g1)] [IsProperExtendedRealFunction g2] [Fact (is_convex_function g2)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x1_smooth : is_l_smooth_on (fun (y1 : E1) => f (y1, x2 k)) Set.univ (PosReal.toNNReal L1)) (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :
have xPlus := prox_gradient_operator (fun (y1 : E1) => f (y1, x2 k)) g1 L1 (x1 k); two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (xPlus, x2 k) - two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar (prox_gradient_mapping (fun (y1 : E1) => f (y1, x2 k)) g1 L1 (x1 k) * (x1 k, x2 k) - xStar)

Lemma 14.4 InactiveBlockSupport helper: the prox-gradient candidate on the current x₁-slice satisfies the optimizer gap bound before comparing the exact alternating-minimization half-step against that candidate.

theorem two_block_half_step_objective_gap_le_x1_gradient_mapping {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E1] [ProperSpace E1] [NormedSpace E2] (x1 : E1) (x2 : E2) (k : ) (L1 : PosReal) [IsProperExtendedRealFunction g1] [Fact (LowerSemicontinuous g1)] [Fact (is_convex_function g1)] [IsProperExtendedRealFunction g2] [Fact (is_convex_function g2)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x1_smooth : is_l_smooth_on (fun (y1 : E1) => f (y1, x2 k)) Set.univ (PosReal.toNNReal L1)) (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (two_block_alternating_minimization_half_step x1 x2 k) - two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar (prox_gradient_mapping (fun (y1 : E1) => f (y1, x2 k)) g1 L1 (x1 k) * (x1 k, x2 k) - xStar)

Helper for Lemma 14.4 InactiveBlockSupport helper (1): if x1 and x2 are generated by the two-block alternating minimization method and the initial pair (x1 0, x2 0) lies in effective_domain F, then the half-step objective gap satisfies F(x^{k+1/2}) - F(x^*) ≤ ‖G^1_{L₁}(x^k)‖ * ‖x^k - x^*‖, with x^{k+1/2} = (x1 (k + 1), x2 k). The intended Chapter 14 proof route is the established current-fiber partial-infimum support bridge, followed by support on the fixed xStar.1 fiber.

theorem twoBlockX2FrozenSliceSupportAtHalfStepFirstBlock {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) {L2 : PosReal} (hf_x2_convex : ConvexOn Set.univ fun (y2 : E2) => f (x1 (k + 1), y2)) (hf_x2_smooth : is_l_smooth_on (fun (y2 : E2) => f (x1 (k + 1), y2)) Set.univ (PosReal.toNNReal L2)) (y2 : E2) :
f (x1 (k + 1), y2) f (x1 (k + 1), x2 k) + (fderiv (fun (y2 : E2) => f (x1 (k + 1), y2)) (x2 k)) (y2 - x2 k)

Helper for Lemma 14.4 InactiveBlockSupport helper: convexity of the frozen smooth slice gives its first-order support inequality at the current second block.

theorem twoBlockX2PartialInfimumEqCurrentObjective {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) :

Helper for Lemma 14.4 InactiveBlockSupport helper: exact minimization of the half-step first block identifies the second partial infimum φ₂(x₂^k) with the half-step objective value.

theorem twoBlockX2PartialInfimumEqOptimalObjective {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :

Helper for Lemma 14.4 InactiveBlockSupport helper: global optimality of xStar identifies the fiber infimum φ₂(xStar.2) with the full objective value F xStar.

theorem twoBlockX2InactiveMarginalEqCurrentValue {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :
twoBlockX2InactiveMarginal f g1 (x2 k) = (f (x1 (k + 1), x2 k)) + g1 (x1 (k + 1))

Helper for Lemma 14.4 InactiveBlockSupport helper: once the half-step is finite, the inactive marginal η₂(y₂) = inf_z₁ (f(z₁, y₂) + g₁(z₁)) is attained at the updated first block.

theorem twoBlockX2InactiveMarginalLeOptimalWitness {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (xStar : E1 × E2) :
twoBlockX2InactiveMarginal f g1 xStar.2 (f xStar) + g1 xStar.1

Helper for Lemma 14.4 InactiveBlockSupport helper: the optimizer's first block is one witness for the inactive marginal at xStar.2.

theorem twoBlockX2InactiveMarginalAddInactivePenaltyEqHalfStepObjective {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) :

Helper for Lemma 14.4 InactiveBlockSupport helper: reattaching the inactive penalty to the current second marginal recovers the half-step objective value.

theorem twoBlockX2InactiveMarginalAddInactivePenaltyLeObjectiveAtStar {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (xStar : E1 × E2) :

Helper for Lemma 14.4 InactiveBlockSupport helper: reattaching the inactive penalty to the optimizer witness bounds the second inactive marginal by the full objective at xStar.

theorem twoBlockX2InactiveMarginalSupportAtStar {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) {L2 : PosReal} [IsProperExtendedRealFunction g1] [IsProperExtendedRealFunction g2] [Fact (is_convex_function g1)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x2_smooth : is_l_smooth_on (fun (y2 : E2) => f (x1 (k + 1), y2)) Set.univ (PosReal.toNNReal L2)) (xStar : E1 × E2) :
twoBlockX2InactiveMarginal f g1 xStar.2 twoBlockX2InactiveMarginal f g1 (x2 k) + (inner (gradient (fun (y2 : E2) => f (x1 (k + 1), y2)) (x2 k)) (xStar.2 - x2 k))

Helper for Lemma 14.4 InactiveBlockSupport helper: the half-step first-block fiber is a convex touching majorant of the second inactive marginal, so η₂ inherits the frozen-slice first-order support inequality at xStar.2.

theorem twoBlockX2ProxCandidateAffineUpperBoundAtStar {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) (L2 : PosReal) [IsProperExtendedRealFunction g2] [Fact (LowerSemicontinuous g2)] [Fact (is_convex_function g2)] [IsProperExtendedRealFunction g1] [Fact (is_convex_function g1)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x2_smooth : is_l_smooth_on (fun (y2 : E2) => f (x1 (k + 1), y2)) Set.univ (PosReal.toNNReal L2)) (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :
have xPlus := prox_gradient_operator (fun (y2 : E2) => f (x1 (k + 1), y2)) g2 L2 (x2 k); have Gk := prox_gradient_mapping (fun (y2 : E2) => f (x1 (k + 1), y2)) g2 L2 (x2 k); have quad := L2 / 2 * xPlus - x2 k ^ 2; two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (k + 1), xPlus) two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar + (inner Gk (xPlus - xStar.2)) + quad

Helper for Lemma 14.4 InactiveBlockSupport helper: the prox-gradient candidate on the current x₂-slice should already satisfy the full optimizer gap bound. This is the remaining x₂-side structural blocker after the exact-step comparison has been isolated.

theorem twoBlockX2ProxCandidateGapLeGradientMapping {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) (L2 : PosReal) [IsProperExtendedRealFunction g2] [Fact (LowerSemicontinuous g2)] [Fact (is_convex_function g2)] [IsProperExtendedRealFunction g1] [Fact (is_convex_function g1)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x2_smooth : is_l_smooth_on (fun (y2 : E2) => f (x1 (k + 1), y2)) Set.univ (PosReal.toNNReal L2)) (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :
have xPlus := prox_gradient_operator (fun (y2 : E2) => f (x1 (k + 1), y2)) g2 L2 (x2 k); two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (k + 1), xPlus) - two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar (prox_gradient_mapping (fun (y2 : E2) => f (x1 (k + 1), y2)) g2 L2 (x2 k) * two_block_alternating_minimization_half_step x1 x2 k - xStar)
theorem two_block_next_iterate_objective_gap_le_x2_gradient_mapping {E1 E2 : Type u} [NormedAddCommGroup E1] [NormedAddCommGroup E2] (f : E1 × E2) (g1 : E1EReal) (g2 : E2EReal) [InnerProductSpace E2] [ProperSpace E2] [NormedSpace E1] (x1 : E1) (x2 : E2) (k : ) (L2 : PosReal) [IsProperExtendedRealFunction g2] [Fact (LowerSemicontinuous g2)] [Fact (is_convex_function g2)] [IsProperExtendedRealFunction g1] [Fact (is_convex_function g1)] (htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2) (hx0 : (x1 0, x2 0) effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) (hf_convex : ConvexOn Set.univ f) (hf_x2_smooth : is_l_smooth_on (fun (y2 : E2) => f (x1 (k + 1), y2)) Set.univ (PosReal.toNNReal L2)) (xStar : E1 × E2) (hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar) :
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (k + 1), x2 (k + 1)) - two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar (prox_gradient_mapping (fun (y2 : E2) => f (x1 (k + 1), y2)) g2 L2 (x2 k) * two_block_alternating_minimization_half_step x1 x2 k - xStar)

Helper for Lemma 14.4 InactiveBlockSupport helper (2): if x1 and x2 are generated by the two-block alternating minimization method and the initial pair (x1 0, x2 0) lies in effective_domain F, then the full-step objective gap satisfies F(x^{k+1}) - F(x^*) ≤ ‖G^2_{L₂}(x^{k+1/2})‖ * ‖x^{k+1/2} - x^*‖, with x^{k+1} = (x1 (k + 1), x2 (k + 1)) and x^{k+1/2} = (x1 (k + 1), x2 k). Its canonical bridge is the symmetric partial-infimum support descent on the current half-step fiber.