theorem mirrorCOptimalPoint_memEffectiveDomain {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g : E → EReal} {XStar : Set E} {FOpt : ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) {xStar : E} (hxStar : xStar ∈ XStar) : xStar ∈ effective_domain g

Helper for Lemma 9.25: every optimal point of the composite problem lies in effective_domain g.

theorem compositeOptimalPoint_toReal_eq_FOpt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g : E → EReal} {XStar : Set E} {FOpt : ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) {xStar : E} (hxStar : xStar ∈ XStar) : (f xStar + g xStar).toReal = FOpt

Helper for Lemma 9.25: an optimal point attains the recorded optimal value in real form.

theorem mirrorCThreePointAddForm {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_traj : is_mirror_c_trajectory f g ω x s t) (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 Lemma 9.25: the Chapter 9 three-point identity can be written directly in add form for the Mirror-C trajectory.

noncomputable def mirrorCLinearPenalty {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (g : E → EReal) (sn : StrongDual ℝ E) (step : ℝ) : E → EReal

Helper for Lemma 9.25: the one-step perturbation fed into the Chapter 9 second-prox theorem.

theorem mirrorCStepBregmanForm_isMinOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (h_traj : is_mirror_c_trajectory f g ω x s t) (n : ℕ) : IsMinOn (secondProxObjective (mirrorCLinearPenalty g (s n) (t n)) ω (x n)) Set.univ (x (n + 1))

Helper for Lemma 9.25: Text 9.10 rewrites the stored Mirror-C update minimizer into the equation (9.33) Bregman-form objective.

theorem mirrorCObjectiveValue_toReal_eq_add {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (h_traj : is_mirror_c_trajectory f g ω x s t) (n : ℕ) : (f (x n) + g (x n)).toReal = (f (x n)).toReal + (g (x n)).toReal

Helper for Lemma 9.25: along a Mirror-C trajectory, each finite composite objective value splits into the sum of the finite real parts of f and g.

theorem mirrorCLinearPenalty_effectiveDomain_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (g : E → EReal) (sn : StrongDual ℝ E) {step : ℝ} (hstep : 0 < step) : effective_domain (mirrorCLinearPenalty g sn step) = effective_domain g

Helper for Lemma 9.25: positive stepsizes preserve the effective domain when passing from g to the linear-plus-penalty perturbation.

theorem mirrorCLinearPenalty_toReal_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {g : E → EReal} (hg_proper : IsProperExtendedRealFunction g) (sn : StrongDual ℝ E) {step : ℝ} (hstep : 0 < step) {u : E} (hu : u ∈ effective_domain g) : (mirrorCLinearPenalty g sn step u).toReal = step * sn u + step * (g u).toReal

Helper for Lemma 9.25: on dom(g), the second-prox perturbation has the expected real value.

theorem mirrorCLinearPenaltyData {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g : E → EReal} {XStar : Set E} {FOpt : ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (sn : StrongDual ℝ E) {step : ℝ} (hstep : 0 < step) : IsProperExtendedRealFunction (mirrorCLinearPenalty g sn step) ∧ is_convex_function (mirrorCLinearPenalty g sn step)

Helper for Lemma 9.25: the second-prox perturbation is proper and convex for positive stepsizes.

theorem secondProxOptimality_real_of_differentiableAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ω ψ : E → EReal} {a b u : E} (hψ_proper : IsProperExtendedRealFunction ψ) (hψ_convex : is_convex_function ψ) (hmin : IsMinOn (secondProxObjective ψ ω b) Set.univ a) (ha : a ∈ effective_domain ψ) (hu : u ∈ effective_domain ψ) (hω_diff : DifferentiableAt ℝ (fun (z : E) => (ω z).toReal) a) : inner ℝ (gradient (fun (z : E) => (ω z).toReal) b - gradient (fun (z : E) => (ω z).toReal) a) (u - a) ≤ (ψ u).toReal - (ψ a).toReal

First-order comparison for a second-prox minimizer when membership in dom(∂ω) is already known. This directional proof avoids the relative-interior sum-rule qualification needed only to derive that membership in Theorem 9.12.

theorem mirrorCStepPairingPenalty_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (hω_diff : ∀ z ∈ subdifferential_domain ω, DifferentiableAt ℝ (fun (w : E) => (ω w).toReal) z) (h_traj : is_mirror_c_trajectory f g ω x s t) (n : ℕ) {u : E} (hu : u ∈ effective_domain g) : t n * (s n) (x n - u) + t n * ((g (x (n + 1))).toReal - (g u).toReal) ≤ B[ω] u (x n) - B[ω] u (x (n + 1)) - B[ω] (x (n + 1)) (x n) + t n * (s n) (x n - x (n + 1))

Helper for Lemma 9.25: each Mirror-C step satisfies the textbook pairing-plus-penalty inequality.

theorem mirrorCSubgradientShiftedGap_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (h_traj : is_mirror_c_trajectory f g ω x s t) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) : (f (x n)).toReal + (g (x (n + 1))).toReal - FOpt ≤ (s n) (x n - xStar) + ((g (x (n + 1))).toReal - (g xStar).toReal)

Helper for Lemma 9.25: the optimality of xStar rewrites the shifted composite objective gap into the current subgradient pairing plus the shifted penalty difference.

theorem mirrorCStepMixedTerm_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (hω_diff : ∀ z ∈ subdifferential_domain ω, DifferentiableAt ℝ (fun (w : E) => (ω w).toReal) z) (h_traj : is_mirror_c_trajectory f g ω x s t) (n : ℕ) : t n * (s n) (x n - x (n + 1)) - B[ω] (x (n + 1)) (x n) ≤ t n ^ 2 * ‖s n‖ ^ 2 / (2 * σ)

Helper for Lemma 9.25: the mixed linear/Bregman term is controlled by the usual Young inequality and the lower quadratic bound for the Bregman distance.

theorem mirrorCStepShiftedObjectiveGap_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (hω_diff : ∀ z ∈ subdifferential_domain ω, DifferentiableAt ℝ (fun (w : E) => (ω w).toReal) z) (h_traj : is_mirror_c_trajectory f g ω x s t) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) : t n * ((f (x n)).toReal + (g (x (n + 1))).toReal - FOpt) ≤ B[ω] xStar (x n) - B[ω] xStar (x (n + 1)) + t n ^ 2 * ‖s n‖ ^ 2 / (2 * σ)

Helper for Lemma 9.25: the one-step shifted Mirror-C estimate.

theorem mirrorCShiftedGapPrefixSum_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (hω_diff : ∀ z ∈ subdifferential_domain ω, DifferentiableAt ℝ (fun (w : E) => (ω w).toReal) z) (h_traj : is_mirror_c_trajectory f g ω x s t) {xStar : E} (hxStar : xStar ∈ XStar) (k : ℕ) : ∑ n ∈ Finset.range (k + 1), t n * ((f (x n)).toReal + (g (x (n + 1))).toReal - FOpt) ≤ B[ω] xStar (x 0) + 1 / (2 * σ) * ∑ n ∈ Finset.range (k + 1), t n ^ 2 * ‖s n‖ ^ 2

Helper for Lemma 9.25: summing the one-step shifted Mirror-C estimate gives the shifted prefix gap bound.

theorem mirrorCPenaltyPrefix_le_shiftedPenaltyPrefix {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_nonneg : ∀ z ∈ effective_domain g, 0 ≤ g z) (h_traj : is_mirror_c_trajectory f g ω x s t) (h_stepsize_antitone : Antitone t) (k : ℕ) : ∑ n ∈ Finset.range (k + 1), t n * (g (x n)).toReal ≤ t 0 * (g (x 0)).toReal + ∑ n ∈ Finset.range (k + 1), t n * (g (x (n + 1))).toReal

Helper for Lemma 9.25: the weighted prefix sum of penalty values is bounded by the initial penalty term plus the shifted weighted prefix sum.

theorem shiftedMirrorCGapSumDominatesObjectiveGap {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (h_nonneg : ∀ z ∈ effective_domain g, 0 ≤ g z) (h_traj : is_mirror_c_trajectory f g ω x s t) (h_stepsize_antitone : Antitone t) (k : ℕ) : ∑ n ∈ Finset.range (k + 1), t n * ((f (x n) + g (x n)).toReal - FOpt) ≤ t 0 * (g (x 0)).toReal + ∑ n ∈ Finset.range (k + 1), t n * ((f (x n)).toReal + (g (x (n + 1))).toReal - FOpt)

Helper for Lemma 9.25: the shifted penalty bookkeeping dominates the weighted prefix sum of composite objective gaps.

theorem mirror_c_weighted_objective_gap_sum_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (hω_diff : ∀ z ∈ subdifferential_domain ω, DifferentiableAt ℝ (fun (w : E) => (ω w).toReal) z) (h_nonneg : ∀ z ∈ effective_domain g, 0 ≤ g z) (h_traj : is_mirror_c_trajectory f g ω x s t) (h_stepsize_antitone : Antitone t) {xStar : E} (hxStar : xStar ∈ XStar) (k : ℕ) : ∑ n ∈ Finset.range (k + 1), t n * ((f (x n) + g (x n)).toReal - FOpt) ≤ t 0 * (g (x 0)).toReal + B[ω] xStar (x 0) + 1 / (2 * σ) * ∑ n ∈ Finset.range (k + 1), t n ^ 2 * ‖s n‖ ^ 2

Companion to Lemma 9.25: under the composite convex minimization assumptions of Definition 9.4, together with the mirror-map assumptions of Definition 9.5 and the Mirror-C trajectory data of Definition 9.6, if g is nonnegative on dom(g) and the Mirror-C stepsizes are nonincreasing, then for every optimal point xStar ∈ XStar = X^* and every iteration index k, the weighted prefix sum of composite objective gaps is bounded by t₀ g(x⁰) + B_ω(xStar, x⁰) + (1 / (2σ)) * ∑_{n=0}^k t_n^2 ‖f'(x^n)‖^2.

theorem mirror_c_best_value_gap_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g ω : E → EReal} {XStar : Set E} {FOpt σ : ℝ} {x : ℕ → E} {s : ℕ → StrongDual ℝ E} {t : ℕ → ℝ} (h_problem : IsCompositeConvexMinimizationProblem f g XStar FOpt) (hω : IsBregmanPotentialOn ω (effective_domain g) σ) (hω_diff : ∀ z ∈ subdifferential_domain ω, DifferentiableAt ℝ (fun (w : E) => (ω w).toReal) z) (h_nonneg : ∀ z ∈ effective_domain g, 0 ≤ g z) (h_traj : is_mirror_c_trajectory f g ω x s t) (h_stepsize_antitone : Antitone t) {xStar : E} (hxStar : xStar ∈ XStar) (k : ℕ) : best_achieved_function_value (fun (y : E) => (f y + g y).toReal) x k - FOpt ≤ (t 0 * (g (x 0)).toReal + B[ω] xStar (x 0) + 1 / (2 * σ) * ∑ n ∈ Finset.range (k + 1), t n ^ 2 * ‖s n‖ ^ 2) / ∑ n ∈ Finset.range (k + 1), t n

Lemma 9.25: under the composite convex minimization assumptions extracted from Definition 9.4, together with the mirror-map assumptions of Definition 9.5 and the Mirror-C trajectory data of Definition 9.6, if g is nonnegative on dom(g) and the Mirror-C stepsizes are nonincreasing, then for every optimal point xStar ∈ XStar = X^* and every iteration index k, the running-best composite objective gap up to time k is bounded by the weighted ratio (t₀ g(x⁰) + B_ω(xStar, x⁰) + (1 / (2σ)) * ∑_{n=0}^k t_n^2 ‖f'(x^n)‖^2) / ∑_{n=0}^k t_n.