class
IsTwoBlockAlternatingMinimizationConvexRateProblem
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
(f : E1 × E2 → ℝ)
(g1 : E1 → EReal)
(g2 : E2 → EReal)
(XStar : outParam (Set (E1 × E2)))
(FOpt : outParam ℝ)
(L1 L2 : outParam ↑PosReal)
:
Source-facing two-block convex-rate owner: Assumption 14.12 together with the canonical
optimal-set and optimal-value data used by the Chapter 14 O(1 / k) rate theorem.
- g1_proper : IsProperExtendedRealFunction g1
- g1_closed : LowerSemicontinuous g1
- g1_convex : is_convex_function g1
- g2_proper : IsProperExtendedRealFunction g2
- g2_closed : LowerSemicontinuous g2
- g2_convex : is_convex_function g2
- f_convex : ConvexOn ℝ Set.univ f
- f_x1_smooth (z2 : E2) : is_l_smooth_on (fun (y1 : E1) => f (y1, z2)) Set.univ (PosReal.toNNReal L1)
- f_x2_smooth (z1 : E1) : is_l_smooth_on (fun (y2 : E2) => f (z1, y2)) Set.univ (PosReal.toNNReal L2)
- optimal_set_eq : XStar = unconstrained_problem_solutions (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)
- optimal_set_nonempty : XStar.Nonempty
- optimal_value_isGLB : IsGLB (Set.range (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)) ↑FOpt
- bounded_sublevel_distance_to_each_optimal_point (α : ↑PosReal) : ∃ (Rα : ↑PosReal), ∀ {y xStar : E1 × E2}, two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ ↑↑α → xStar ∈ XStar → ‖y - xStar‖ ≤ ↑Rα
Instances
theorem
TwoBlockConvexRate.toIsAlternatingMinimizationConvexRateProblem
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
(h : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2)
(hfull_smooth :
is_l_smooth_on (twoBlockAlternatingMinimizationSmoothTerm f) Set.univ
(twoBlockAlternatingMinimizationGlobalSmoothness L1 L2))
:
Assumption 14.12 exports the canonical Chapter 14 convex-rate owner on the Fin 2
block-vector view from Algorithm 14.8. This is a companion bridge, not a replacement for the
source-facing pair owner.
instance
TwoBlockConvexRate.instIsAlternatingMinimizationConvexRateProblemOfIsTwoBlockProblem
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
[h : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
[hfull_smooth :
Fact
(is_l_smooth_on (twoBlockAlternatingMinimizationSmoothTerm f) Set.univ
(twoBlockAlternatingMinimizationGlobalSmoothness L1 L2))]
:
Assumption 14.12 makes the canonical Fin 2 Chapter 14 convex-rate owner available through
typeclass search.
theorem
TwoBlockConvexRate.bounded_sublevel_distance_to_optimal_set
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
(h : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2)
(α : ↑PosReal)
:
∃ (Rα : ↑PosReal),
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ ↑↑α → Metric.infDist y XStar ≤ ↑Rα
The source-facing pairwise sublevel-radius clause in Assumption 14.12 implies the weaker distance-to-optimal-set estimate used elsewhere in the Chapter 14 rate analysis.
theorem
TwoBlockConvexRate.bounded_initial_sublevel_distance_to_each_optimal_point
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
(h : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2)
{x0 : E1 × E2}
{α : ↑PosReal}
(hx0 : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 x0 ≤ ↑↑α)
:
∃ (Rα : ↑PosReal),
∀ {y xStar : E1 × E2},
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 x0 →
xStar ∈ XStar → ‖y - xStar‖ ≤ ↑Rα
The source-facing pairwise sublevel-radius clause in Assumption 14.12 yields a radius that
controls the whole initial sublevel set {y | F y ≤ F x0}.
theorem
TwoBlockConvexRate.bounded_initial_sublevel_distance_to_optimal_set
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
(h : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2)
{x0 : E1 × E2}
{α : ↑PosReal}
(hx0 : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 x0 ≤ ↑↑α)
:
∃ (Rα : ↑PosReal),
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 x0 →
Metric.infDist y XStar ≤ ↑Rα
If the initial objective value is bounded by a positive level α, then the same Assumption
14.12 radius controls the whole initial sublevel set in the weaker distance-to-optimal-set form
used by later convergence arguments.
theorem
convex_real_support_univ_fderiv
{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 Theorem 14.8: a convex differentiable real-valued function on the whole Banach
space satisfies the first-order support inequality in fderiv form.
theorem
two_block_current_x2_objective_is_min_on
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 Theorem 14.8: the current second block is always an exact minimizer of the current
x₂-subproblem, with the k = 0 case coming from the initialization clause.
theorem
two_block_iterates_mem_effective_domain_and_initial_sublevel
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
(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 : ℕ)
:
(x1 n, x2 n) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) ∧ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n) ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0)
Helper for Theorem 14.8: every outer iterate stays in the effective domain of F, and the
objective never exceeds its initial value.
theorem
two_block_half_step_mem_effective_domain_and_initial_sublevel
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
(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 : ℕ)
:
two_block_alternating_minimization_half_step x1 x2 n ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) ∧ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2
(two_block_alternating_minimization_half_step x1 x2 n) ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0)
Helper for Theorem 14.8: each half-step also stays in the effective domain and in the initial sublevel set.
theorem
two_block_objective_gap_nonneg
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × E2}
{FOpt : ℝ}
[hg1_proper : IsProperExtendedRealFunction g1]
[hg2_proper : IsProperExtendedRealFunction g2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(n : ℕ)
:
0 ≤ (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)).toReal - FOpt
Helper for Theorem 14.8: every iterate objective gap is nonnegative because each iterate is
finite and xStar globally minimizes F.
theorem
two_block_objective_gap_le_of_quadratic_recurrence
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
(γ : ↑PosReal)
(hγ : 4 * ↑γ ≤ 8 * min ↑L1 ↑L2 * ↑R ^ 2)
(ha_nonneg :
∀ (n : ℕ), 0 ≤ (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)).toReal - FOpt)
(hstep :
∀ (n : ℕ),
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)).toReal - FOpt - ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt) ≥ 1 / ↑γ * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt) ^ 2)
(k : ℕ)
(hk : 2 ≤ k)
:
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 k, x2 k)).toReal - FOpt ≤ max
((1 / 2) ^ (↑(k - 1) / 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0)).toReal - FOpt))
(8 * min ↑L1 ↑L2 * ↑R ^ 2 / ↑(k - 1))
Helper for Theorem 14.8: the source proof reduces the theorem to a Chapter 14 quadratic recurrence and then to the Chapter 11 scalar recurrence estimate.
theorem
two_block_objective_ne_bot
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[hg1_proper : IsProperExtendedRealFunction g1]
[hg2_proper : IsProperExtendedRealFunction g2]
(y : E1 × E2)
:
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≠ ⊥
Helper for Theorem 14.8: properness of the penalty terms rules out the value -∞ for the
two-block objective at every point.
theorem
two_block_objective_eq_coe_toReal_of_mem_effective_domain
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[IsProperExtendedRealFunction g1]
[IsProperExtendedRealFunction g2]
{y : E1 × E2}
(hy : y ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
:
↑(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y).toReal = two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y
Helper for Theorem 14.8: on the effective domain, the objective is exactly the coercion of its real value.
theorem
two_block_optimal_point_mem_effective_domain
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
xStar ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2)
Helper for Theorem 14.8: the optimal pair attains the finite value FOpt, so it lies in the
effective domain of F.
theorem
two_block_next_iterate_objective_gap_le_half_step_gap
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{FOpt : ℝ}
[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 : ℕ)
:
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt ≤ (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2
(two_block_alternating_minimization_half_step x1 x2 n)).toReal - FOpt
Helper for Theorem 14.8: the exact second-block update makes the next objective gap no larger than the half-step objective gap.
theorem
two_block_x1_partial_infimum_eq_current_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(n : ℕ)
:
twoBlockX1PartialInfimum f g1 g2 (x1 n) = two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)
Helper for Theorem 14.8: exact minimization of the current second-block slice identifies the
first-block partial infimum at x₁^n with the current objective value.
theorem
two_block_x1_partial_infimum_eq_optimal_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
twoBlockX1PartialInfimum f g1 g2 xStar.1 = ↑FOpt
Helper for Theorem 14.8: the same first-block partial infimum equals the optimal value at
xStar.1.
theorem
two_block_x2_partial_infimum_eq_current_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(n : ℕ)
:
twoBlockX2PartialInfimum f g1 g2 (x2 n) = two_block_alternating_minimization_objective (Function.toEReal f) g1 g2
(two_block_alternating_minimization_half_step x1 x2 n)
Helper for Theorem 14.8: exact minimization of the current first-block slice identifies the
second-block partial infimum at x₂^n with the half-step objective value.
theorem
two_block_x2_partial_infimum_eq_optimal_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
twoBlockX2PartialInfimum f g1 g2 xStar.2 = ↑FOpt
Helper for Theorem 14.8: the second-block partial infimum equals the optimal value at
xStar.2.
theorem
two_block_first_penalty_eq_coe_toReal_of_mem_effective_domain
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[hg1_proper : IsProperExtendedRealFunction g1]
[hg2_proper : 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 Theorem 14.8: if the full objective is finite at y, then the first penalty term
is also finite there.
theorem
two_block_second_penalty_eq_coe_toReal_of_mem_effective_domain
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[hg1_proper : IsProperExtendedRealFunction g1]
[hg2_proper : 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 Theorem 14.8: if the full objective is finite at y, then the second penalty term
is also finite there.
theorem
two_block_first_penalty_mem_effective_domain_of_objective_mem
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[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 Theorem 14.8: finiteness of the full objective forces finiteness of the first penalty term at the same point.
theorem
two_block_second_penalty_mem_effective_domain_of_objective_mem
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[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 Theorem 14.8: finiteness of the full objective also forces finiteness of the second penalty term.
theorem
two_block_objective_is_convex_function
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[IsProperExtendedRealFunction g1]
[IsProperExtendedRealFunction g2]
(hf_convex : ConvexOn ℝ Set.univ f)
(hg1_convex : is_convex_function g1)
(hg2_convex : is_convex_function g2)
:
Helper for Theorem 14.8: the full two-block objective
F(y₁, y₂) = f(y₁, y₂) + g₁(y₁) + g₂(y₂) is convex once the smooth term and both penalties are
convex.
theorem
two_block_x1_partial_infimum_is_convex
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[IsProperExtendedRealFunction g1]
[IsProperExtendedRealFunction g2]
(hf_convex : ConvexOn ℝ Set.univ f)
(hg1_convex : is_convex_function g1)
(hg2_convex : is_convex_function g2)
:
is_convex_function (twoBlockX1PartialInfimum f g1 g2)
Helper for Theorem 14.8: the first full partial infimum
φ₁(y₁) = inf_z₂ F(y₁, z₂) is convex.
theorem
two_block_x2_partial_infimum_is_convex
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
[IsProperExtendedRealFunction g1]
[IsProperExtendedRealFunction g2]
(hf_convex : ConvexOn ℝ Set.univ f)
(hg1_convex : is_convex_function g1)
(hg2_convex : is_convex_function g2)
:
is_convex_function (twoBlockX2PartialInfimum f g1 g2)
Helper for Theorem 14.8: the second full partial infimum
φ₂(y₂) = inf_z₁ F(z₁, y₂) is convex.
theorem
two_block_x1_inactive_marginal_is_convex
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g2 : E2 → EReal}
[IsProperExtendedRealFunction g2]
(hf_convex : ConvexOn ℝ Set.univ f)
(hg2_convex : is_convex_function g2)
:
Helper for Theorem 14.8: the first inactive marginal
η₁(y₁) = inf_z₂ (f(y₁, z₂) + g₂(z₂)) is convex.
theorem
two_block_x2_inactive_marginal_is_convex
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
[IsProperExtendedRealFunction g1]
(hf_convex : ConvexOn ℝ Set.univ f)
(hg1_convex : is_convex_function g1)
:
Helper for Theorem 14.8: the second inactive marginal
η₂(y₂) = inf_z₁ (f(z₁, y₂) + g₁(z₁)) is convex.
theorem
two_block_x1_inactive_marginal_eq_current_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 : ℕ)
:
twoBlockX1InactiveMarginal f g2 (x1 n) = ↑(f (x1 n, x2 n)) + g2 (x2 n)
Helper for Theorem 14.8: once the current outer iterate is finite, the inactive marginal
η₁(y₁) = inf_z₂ (f(y₁, z₂) + g₂(z₂)) is attained at the current second block.
theorem
two_block_x1_inactive_marginal_le_optimal_witness
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g2 : E2 → EReal}
{xStar : E1 × E2}
:
twoBlockX1InactiveMarginal f g2 xStar.1 ≤ ↑(f xStar) + g2 xStar.2
Helper for Theorem 14.8: the optimal second block gives an upper witness for the inactive
first-block marginal η₁.
theorem
two_block_x1_inactive_marginal_eq_optimal_witness_value
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
[IsProperExtendedRealFunction g1]
[IsProperExtendedRealFunction g2]
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
twoBlockX1InactiveMarginal f g2 xStar.1 = ↑(f xStar) + g2 xStar.2
Helper for Theorem 14.8: if xStar globally minimizes the full objective, then the optimal
second block actually attains the inactive marginal η₁(xStar.1).
theorem
two_block_x1_inactive_marginal_add_active_penalty_eq_current_objective
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 : ℕ)
:
twoBlockX1InactiveMarginal f g2 (x1 n) + g1 (x1 n) = two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)
Helper for Theorem 14.8: reattaching the active penalty to η₁(x₁^n) recovers the full
current objective value.
theorem
two_block_x1_inactive_marginal_add_active_penalty_le_optimal_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
twoBlockX1InactiveMarginal f g2 xStar.1 + g1 xStar.1 ≤ ↑FOpt
Helper for Theorem 14.8: reattaching the active penalty to the optimal witness for η₁
compares the marginal value against F_opt.
theorem
two_block_x2_inactive_marginal_eq_current_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 : ℕ)
:
twoBlockX2InactiveMarginal f g1 (x2 n) = ↑(f (x1 (n + 1), x2 n)) + g1 (x1 (n + 1))
Helper for Theorem 14.8: 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
two_block_x2_inactive_marginal_le_optimal_witness
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{xStar : E1 × E2}
:
twoBlockX2InactiveMarginal f g1 xStar.2 ≤ ↑(f xStar) + g1 xStar.1
Helper for Theorem 14.8: the optimal first block gives an upper witness for the inactive
second-block marginal η₂.
theorem
two_block_x2_inactive_marginal_eq_optimal_witness_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
[IsProperExtendedRealFunction g1]
[IsProperExtendedRealFunction g2]
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
twoBlockX2InactiveMarginal f g1 xStar.2 = ↑(f xStar) + g1 xStar.1
Helper for Theorem 14.8: if xStar globally minimizes the full objective, then the optimal
first block actually attains the inactive marginal η₂(xStar.2).
theorem
x2_marginal_add_penalty_eq_half_step_objective
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 : ℕ)
:
twoBlockX2InactiveMarginal f g1 (x2 n) + g2 (x2 n) = two_block_alternating_minimization_objective (Function.toEReal f) g1 g2
(two_block_alternating_minimization_half_step x1 x2 n)
Helper for Theorem 14.8: reattaching the inactive penalty to η₂(x₂^n) recovers the
half-step objective value.
theorem
two_block_x2_inactive_marginal_add_inactive_penalty_le_optimal_value
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{xStar : E1 × E2}
{FOpt : ℝ}
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
:
twoBlockX2InactiveMarginal f g1 xStar.2 + g2 xStar.2 ≤ ↑FOpt
Helper for Theorem 14.8: reattaching the inactive penalty to the optimal witness for η₂
compares that marginal value against F_opt.
theorem
partial_infimum_support_of_attained_pair_support
{E V : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(H : E × V → EReal)
(x0 : E)
(v0 : V)
(g : Module.Dual ℝ E)
(hattained : sInf (Set.range fun (v : V) => H (x0, v)) = H (x0, v0))
(hsupport : ∀ (y : E) (v : V), H (y, v) ≥ H (x0, v0) + ↑(g (y - x0)))
(y : E)
:
sInf (Set.range fun (v : V) => H (y, v)) ≥ sInf (Set.range fun (v : V) => H (x0, v)) + ↑(g (y - x0))
Helper for Theorem 14.8: once a pair objective has a supporting affine lower bound at an attained fiber minimizer, the same support inequality descends to the partial infimum.
theorem
partial_infimum_support_at_fixed_point_of_attained_pair_support
{E V : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(H : E × V → EReal)
(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 Theorem 14.8: the source proof sometimes only needs to descend mixed pair support at one fixed active competitor, not uniformly over all active competitors.
theorem
convex_partial_infimum_support_of_exact_fiber_minimizer
{E V : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{H : E × V → EReal}
{x0 : E}
{v0 : V}
{g : Module.Dual ℝ E}
(hattained : sInf (Set.range fun (v : V) => H (x0, v)) = H (x0, v0))
(hpair_support : ∀ (y : E) (v : V), H (y, v) ≥ H (x0, v0) + ↑(g (y - x0)))
(y : E)
:
sInf (Set.range fun (v : V) => H (y, v)) ≥ sInf (Set.range fun (v : V) => H (x0, v)) + ↑(g (y - x0))
Helper for Theorem 14.8: for a jointly convex two-variable extended-real objective, affine support on an attained minimizing fiber descends to the partial infimum once the pair-support inequality is already available on the whole target fiber.
theorem
partial_infimum_support_of_exact_fiber_minimizer
{E V : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{h : E × V → ℝ}
{q : V → EReal}
{x0 : E}
{v0 : V}
{y : E}
{g : Module.Dual ℝ E}
(hattained : sInf (Set.range fun (v : V) => ↑(h (x0, v)) + q v) = ↑(h (x0, v0)) + q v0)
(hsupport : ∀ (v : V), ↑(h (y, v)) + q v ≥ ↑(h (x0, v0)) + q v0 + ↑(g (y - x0)))
:
sInf (Set.range fun (v : V) => ↑(h (y, v)) + q v) ≥ sInf (Set.range fun (v : V) => ↑(h (x0, v)) + q v) + ↑(g (y - x0))
Helper for Theorem 14.8: for the split objective H(y, v) = h(y, v) + q(v), the true
fixed-competitor bridge only descends support once the whole target fiber already satisfies the
same affine lower bound.
theorem
two_block_x1_inactive_marginal_support_of_pair_support
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
(n : ℕ)
(hattained : sInf (Set.range fun (z2 : E2) => ↑(f (x1 n, z2)) + g2 z2) = ↑(f (x1 n, x2 n)) + g2 (x2 n))
(hpair_support :
∀ (y1 : E1) (z2 : E2),
↑(f (y1, z2)) + g2 z2 ≥ ↑(f (x1 n, x2 n)) + g2 (x2 n) + ↑((fderiv ℝ (fun (z1 : E1) => f (z1, x2 n)) (x1 n)) (y1 - x1 n)))
(y1 : E1)
:
sInf (Set.range fun (z2 : E2) => ↑(f (y1, z2)) + g2 z2) ≥ sInf (Set.range fun (z2 : E2) => ↑(f (x1 n, z2)) + g2 z2) + ↑((fderiv ℝ (fun (z1 : E1) => f (z1, x2 n)) (x1 n)) (y1 - x1 n))
Helper for Theorem 14.8: once a uniform mixed pair-support inequality is available for the
inactive x₂ fibers, it descends directly to the first-block marginal η₁.
theorem
two_block_x2_inactive_marginal_support_of_pair_support
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
(n : ℕ)
(hattained : sInf (Set.range fun (z1 : E1) => ↑(f (z1, x2 n)) + g1 z1) = ↑(f (x1 (n + 1), x2 n)) + g1 (x1 (n + 1)))
(hpair_support :
∀ (y2 : E2) (z1 : E1),
↑(f (z1, y2)) + g1 z1 ≥ ↑(f (x1 (n + 1), x2 n)) + g1 (x1 (n + 1)) + ↑((fderiv ℝ (fun (z2 : E2) => f (x1 (n + 1), z2)) (x2 n)) (y2 - x2 n)))
(y2 : E2)
:
sInf (Set.range fun (z1 : E1) => ↑(f (z1, y2)) + g1 z1) ≥ sInf (Set.range fun (z1 : E1) => ↑(f (z1, x2 n)) + g1 z1) + ↑((fderiv ℝ (fun (z2 : E2) => f (x1 (n + 1), z2)) (x2 n)) (y2 - x2 n))
Helper for Theorem 14.8: the symmetric mixed pair-support inequality descends to the
second-block marginal η₂.
theorem
two_block_x1_frozen_slice_support_at_current_second_block
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{L1 : ↑PosReal}
(hf_convex : ConvexOn ℝ Set.univ f)
(hf_x1_smooth : ∀ (z2 : E2), is_l_smooth_on (fun (y1 : E1) => f (y1, z2)) Set.univ (PosReal.toNNReal L1))
(n : ℕ)
(y1 : E1)
:
f (y1, x2 n) ≥ f (x1 n, x2 n) + (fderiv ℝ (fun (z1 : E1) => f (z1, x2 n)) (x1 n)) (y1 - x1 n)
Helper for Theorem 14.8: convexity of the smooth term gives the first-order support inequality
on the frozen current second-block slice y₁ ↦ f(y₁, x₂^n).
theorem
two_block_x1_inactive_slice_support_at_current_first_block
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 : ℕ)
(z2 : E2)
:
↑(f (x1 n, z2)) + g2 z2 ≥ ↑(f (x1 n, x2 n)) + g2 (x2 n)
Helper for Theorem 14.8: exact minimization of the current second-block slice implies the inactive-slice support inequality at the current first block.
theorem
two_block_x2_frozen_slice_support_at_half_step_first_block
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{L2 : ↑PosReal}
(hf_convex : ConvexOn ℝ Set.univ f)
(hf_x2_smooth : ∀ (z1 : E1), is_l_smooth_on (fun (y2 : E2) => f (z1, y2)) Set.univ (PosReal.toNNReal L2))
(n : ℕ)
(y2 : E2)
:
f (x1 (n + 1), y2) ≥ f (x1 (n + 1), x2 n) + (fderiv ℝ (fun (z2 : E2) => f (x1 (n + 1), z2)) (x2 n)) (y2 - x2 n)
Helper for Theorem 14.8: convexity of the smooth term gives the first-order support inequality
on the frozen half-step first-block slice y₂ ↦ f(x₁^{n+1}, y₂).
theorem
two_block_x2_inactive_slice_support_at_current_second_block
{E1 E2 : Type u}
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{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 : ℕ)
(z1 : E1)
:
↑(f (z1, x2 n)) + g1 z1 ≥ ↑(f (x1 (n + 1), x2 n)) + g1 (x1 (n + 1))
Helper for Theorem 14.8: exact minimization of the half-step first-block slice implies the inactive-slice support inequality at the current second block.
theorem
two_block_x1_inactive_marginal_support_at_xStar_of_pair_support
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × 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 : ℕ)
(hpair_support :
∀ (z2 : E2),
↑(f (xStar.1, z2)) + g2 z2 ≥ ↑(f (x1 n, x2 n)) + g2 (x2 n) + ↑((fderiv ℝ (fun (z1 : E1) => f (z1, x2 n)) (x1 n)) (xStar.1 - x1 n)))
:
twoBlockX1InactiveMarginal f g2 xStar.1 ≥ twoBlockX1InactiveMarginal f g2 (x1 n) + ↑((fderiv ℝ (fun (z1 : E1) => f (z1, x2 n)) (x1 n)) (xStar.1 - x1 n))
Helper for Theorem 14.8: once the full source-faithful support inequality is known against the
fixed competitor xStar, it descends to the first inactive marginal η₁.
theorem
two_block_x2_inactive_marginal_support_at_xStar_of_pair_support
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × 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 : ℕ)
(hpair_support :
∀ (z1 : E1),
↑(f (z1, xStar.2)) + g1 z1 ≥ ↑(f (x1 (n + 1), x2 n)) + g1 (x1 (n + 1)) + ↑((fderiv ℝ (fun (z2 : E2) => f (x1 (n + 1), z2)) (x2 n)) (xStar.2 - x2 n)))
:
twoBlockX2InactiveMarginal f g1 xStar.2 ≥ twoBlockX2InactiveMarginal f g1 (x2 n) + ↑((fderiv ℝ (fun (z2 : E2) => f (x1 (n + 1), z2)) (x2 n)) (xStar.2 - x2 n))
Helper for Theorem 14.8: once the full source-faithful support inequality is known against the
fixed competitor xStar, it descends to the second inactive marginal η₂.
theorem
two_block_x1_split_objective_support_on_active_slice
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{L1 : ↑PosReal}
(hf_convex : ConvexOn ℝ Set.univ f)
(hf_x1_smooth : ∀ (z2 : E2), is_l_smooth_on (fun (y1 : E1) => f (y1, z2)) Set.univ (PosReal.toNNReal L1))
(n : ℕ)
(y1 : E1)
:
↑(f (y1, x2 n)) + g2 (x2 n) ≥ ↑(f (x1 n, x2 n)) + g2 (x2 n) + ↑((fderiv ℝ (fun (z1 : E1) => f (z1, x2 n)) (x1 n)) (y1 - x1 n))
Helper for Theorem 14.8: adding back the frozen inactive penalty turns the current first-block
slice support inequality into support for the split objective on the active slice
y₁ ↦ f(y₁, x₂^n) + g₂(x₂^n).
theorem
two_block_x2_split_objective_support_on_active_slice
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{L2 : ↑PosReal}
(hf_convex : ConvexOn ℝ Set.univ f)
(hf_x2_smooth : ∀ (z1 : E1), is_l_smooth_on (fun (y2 : E2) => f (z1, y2)) Set.univ (PosReal.toNNReal L2))
(n : ℕ)
(y2 : E2)
:
↑(f (x1 (n + 1), y2)) + g1 (x1 (n + 1)) ≥ ↑(f (x1 (n + 1), x2 n)) + g1 (x1 (n + 1)) + ↑((fderiv ℝ (fun (z2 : E2) => f (x1 (n + 1), z2)) (x2 n)) (y2 - x2 n))
Helper for Theorem 14.8: adding back the frozen active penalty turns the current second-block
slice support inequality into support for the split objective on the active slice
y₂ ↦ f(x₁^{n+1}, y₂) + g₁(x₁^{n+1}).
theorem
active_slice_fderiv_is_subgradient
{E V : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{h : E × V → ℝ}
{x0 : E}
{v0 : V}
(hh_convex : ConvexOn ℝ Set.univ h)
(hslice_diff : DifferentiableAt ℝ (fun (z : E) => h (z, v0)) x0)
:
is_subgradient_at (fun (x : E) => ↑(h (x, v0))) x0 ↑(fderiv ℝ (fun (z : E) => h (z, v0)) x0)
Helper for Theorem 14.8: convexity and differentiability of the active slice make its Fréchet derivative a genuine Chapter 3 subgradient of the active-slice extended-real function.
theorem
zero_mem_subdifferential_of_exact_inactive_split_minimizer
{E V : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{h : E × V → ℝ}
{q : V → EReal}
{x0 : E}
{v0 : V}
(hv0_mem : v0 ∈ effective_domain fun (v : V) => ↑(h (x0, v)) + q v)
(hmin : ∀ (v : V), ↑(h (x0, v)) + q v ≥ ↑(h (x0, v0)) + q v0)
:
Helper for Theorem 14.8: exact minimization of the inactive split slice makes the zero functional a Chapter 3 subgradient of that one-variable slice objective.
theorem
two_block_x1_trial_point_distance_le_current_distance
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × E2}
(n : ℕ)
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
‖((1 - t) • x1 n + t • xStar.1, x2 n) - xStar‖ ≤ ‖(x1 n, x2 n) - xStar‖
Helper for Theorem 14.8: moving only the first block along the segment from x₁^n to
xStar.1 can only shrink the distance to the optimizer pair.
theorem
two_block_x1_trial_point_distance_le_radius
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × E2}
{R : ↑PosReal}
(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))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
‖((1 - t) • x1 n + t • xStar.1, x2 n) - xStar‖ ≤ ↑R
Helper for Theorem 14.8: the first-block segment trial point inherits the same radius bound as the current iterate.
theorem
two_block_x2_trial_point_distance_le_half_step_distance
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × E2}
(n : ℕ)
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
‖(x1 (n + 1), (1 - t) • x2 n + t • xStar.2) - xStar‖ ≤ ‖two_block_alternating_minimization_half_step x1 x2 n - xStar‖
Helper for Theorem 14.8: moving only the second block along the segment from x₂^n to
xStar.2 can only shrink the distance to the half-step pair.
theorem
two_block_x2_trial_point_distance_le_radius
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × E2}
{R : ↑PosReal}
(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))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
‖(x1 (n + 1), (1 - t) • x2 n + t • xStar.2) - xStar‖ ≤ ↑R
Helper for Theorem 14.8: the second-block segment trial point inherits the same radius bound as the half-step pair.
theorem
two_block_x1_current_first_block_distance_le_radius
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedAddCommGroup E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{xStar : E1 × E2}
{R : ↑PosReal}
(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))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
:
‖xStar.1 - x1 n‖ ≤ ↑R
Helper for Theorem 14.8: the current first-block distance to the optimizer is bounded by the same initial-sublevel radius as the full pair iterate.
theorem
two_block_x1_half_step_gap_le_affine_quadratic
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{xStar : E1 × E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
(t : ℝ)
(ht : t ∈ Set.Icc 0 1)
:
have xHalf := two_block_alternating_minimization_half_step x1 x2 n;
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xHalf).toReal - FOpt ≤ (1 - t) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)).toReal - FOpt) + ↑L1 / 2 * t ^ 2 * ↑R ^ 2
Helper for Theorem 14.8: the source x₁-branch first compares the exact half-step against
the segment trial point toward xStar.1, yielding the affine-quadratic estimate in the trial
parameter t.
theorem
two_block_x2_next_gap_le_affine_quadratic
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{xStar : E1 × E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
(t : ℝ)
(ht : t ∈ Set.Icc 0 1)
:
have xHalf := two_block_alternating_minimization_half_step x1 x2 n;
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt ≤ (1 - t) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xHalf).toReal - FOpt) + ↑L2 / 2 * t ^ 2 * ↑R ^ 2
Helper for Theorem 14.8: the source x₂-branch compares the exact next iterate against the
segment trial point toward xStar.2, giving the affine-quadratic estimate in the trial
parameter t.
theorem
two_block_x1_half_step_quadratic_gap
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{xStar : E1 × E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
:
have xHalf := two_block_alternating_minimization_half_step x1 x2 n;
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)).toReal - FOpt - ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xHalf).toReal - FOpt) ≥ 1 / (2 * ↑L1 * ↑R ^ 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xHalf).toReal - FOpt) ^ 2
Helper for Theorem 14.8: the source equation (14.35) is the x₁-half-step quadratic gap
estimate.
theorem
two_block_x2_next_step_quadratic_gap
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{xStar : E1 × E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
:
have xHalf := two_block_alternating_minimization_half_step x1 x2 n;
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xHalf).toReal - FOpt - ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt) ≥ 1 / (2 * ↑L2 * ↑R ^ 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt) ^ 2
Helper for Theorem 14.8: the source equation (14.36) contributes the x₂-next-step
quadratic gap estimate.
theorem
two_block_objective_gap_quadratic_recurrence
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{xStar : E1 × E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(n : ℕ)
:
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 n, x2 n)).toReal - FOpt - ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt) ≥ 1 / (2 * min ↑L1 ↑L2 * ↑R ^ 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 (n + 1), x2 (n + 1))).toReal - FOpt) ^ 2
Helper for Theorem 14.8: the source proof's real work is the quadratic one-step recurrence for the two-block objective-gap sequence.
theorem
two_block_objective_gap_le_max_geometric_or_sublinear_core
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{xStar : E1 × E2}
{FOpt : ℝ}
{L1 L2 R : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(htraj : is_two_block_alternating_minimization_trajectory (Function.toEReal f) g1 g2 x1 x2)
(hxStar : IsMinOn (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2) Set.univ xStar)
(hFOpt : two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 xStar = ↑FOpt)
(hx0 : (x1 0, x2 0) ∈ effective_domain (two_block_alternating_minimization_objective (Function.toEReal f) g1 g2))
(hR :
∀ ⦃y : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
‖y - xStar‖ ≤ ↑R)
(k : ℕ)
(hk : 2 ≤ k)
:
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 k, x2 k)).toReal - FOpt ≤ max
((1 / 2) ^ (↑(k - 1) / 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0)).toReal - FOpt))
(8 * min ↑L1 ↑L2 * ↑R ^ 2 / ↑(k - 1))
Helper for Theorem 14.8: the source proof reduces the theorem to a Chapter 14 quadratic recurrence and then to the Chapter 11 scalar recurrence estimate.
theorem
two_block_alternating_minimization_objective_gap_le_max_geometric_or_sublinear_of_initial_radius
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(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))
(R : ↑PosReal)
(hR :
∀ ⦃y xStar : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
xStar ∈ XStar → ‖y - xStar‖ ≤ ↑R)
(k : ℕ)
(hk : 2 ≤ k)
:
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 k, x2 k)).toReal - FOpt ≤ max
((1 / 2) ^ (↑(k - 1) / 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0)).toReal - FOpt))
(8 * min ↑L1 ↑L2 * ↑R ^ 2 / ↑(k - 1))
Helper for Theorem 14.8: if the initial pair x^0 = (x₁^0, x₂^0) lies in dom(F), then under
an explicit initial-sublevel radius witness R, every k ≥ 2 objective gap is
bounded by the maximum of the geometric term
(1 / 2)^((k - 1) / 2) (F(x^0) - F_opt) and the sublinear term
8 min {L₁, L₂} R^2 / (k - 1).
theorem
two_block_objective_gap_le_max_geometric_or_sublinear
{E1 E2 : Type u}
[NormedAddCommGroup E1]
[NormedSpace ℝ E1]
[NormedAddCommGroup E2]
[NormedSpace ℝ E2]
{f : E1 × E2 → ℝ}
{g1 : E1 → EReal}
{g2 : E2 → EReal}
{x1 : ℕ → E1}
{x2 : ℕ → E2}
{XStar : Set (E1 × E2)}
{FOpt : ℝ}
{L1 L2 : ↑PosReal}
[hproblem : IsTwoBlockAlternatingMinimizationConvexRateProblem f g1 g2 XStar FOpt L1 L2]
(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))
:
∃ (R : ↑PosReal),
(∀ ⦃y xStar : E1 × E2⦄,
two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 y ≤ two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0) →
xStar ∈ XStar → ‖y - xStar‖ ≤ ↑R) ∧ ∀ (k : ℕ),
2 ≤ k →
(two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 k, x2 k)).toReal - FOpt ≤ max
((1 / 2) ^ (↑(k - 1) / 2) * ((two_block_alternating_minimization_objective (Function.toEReal f) g1 g2 (x1 0, x2 0)).toReal - FOpt))
(8 * min ↑L1 ↑L2 * ↑R ^ 2 / ↑(k - 1))
Theorem 14.8: if Assumption 14.12 holds and (x₁^k, x₂^k) is generated by the exact
two-block alternating-minimization method from Algorithm 14.8, then there exists a radius
R = R_{F(x^0)} controlling the initial sublevel set {y | F y ≤ F x[0]} such that, for every
k ≥ 2, provided the initial pair x^0 = (x₁^0, x₂^0) lies in dom(F), the objective gap is
bounded by the maximum of the geometric term
(1 / 2)^((k - 1) / 2) (F(x^0) - F_opt) and the sublinear term
8 min {L₁, L₂} R^2 / (k - 1).