noncomputable def dual_based_proximal_gradient_dual_lipschitz_constant {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : E →L[ℝ] V) (σ : ↑PosReal) : ℝ

The dual smoothness bound L_F = ‖A‖² / σ attached to the dual representation.

theorem dual_based_proximal_gradient_dual_lipschitz_constant_eq {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : E →L[ℝ] V) (σ : ↑PosReal) : dual_based_proximal_gradient_dual_lipschitz_constant A σ = ‖A‖ ^ 2 / ↑σ

Expanding the dual smoothness bound gives the textbook value ‖A‖² / σ.

@[reducible, inline]

abbrev DualBasedProximalGradientDualStepsizeParameter {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : E →L[ℝ] V) (σ : ↑PosReal) : Type

An admissible constant parameter for the dual proximal-gradient method is a positive real L satisfying the textbook lower bound L_F = ‖A‖² / σ ≤ L.

theorem DualBasedProximalGradientDualStepsizeParameter.lower_bound {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {A : E →L[ℝ] V} {σ : ↑PosReal} (L : DualBasedProximalGradientDualStepsizeParameter A σ) : dual_based_proximal_gradient_dual_lipschitz_constant A σ ≤ ↑↑L

Every admissible dual proximal-gradient parameter satisfies ‖A‖² / σ ≤ L.

def dual_based_proximal_gradient_dual_step {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (G : V → EReal) (gradF : V → V) (L : ↑PosReal) (yk : V) : Set V

The admissible next dual iterates from y^k are the proximal points of (1 / L) G at the forward-gradient point y^k - (1 / L) gradF(y^k), where gradF represents the gradient of the smooth term F.

@[simp]

theorem mem_dual_based_proximal_gradient_dual_step_iff {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] {G : V → EReal} {gradF : V → V} {L : ↑PosReal} {yk yNext : V} : yNext ∈ dual_based_proximal_gradient_dual_step G gradF L yk ↔ yNext ∈ prox[↑↑(1 / L) • G] (yk - (1 / ↑L) • gradF yk)

A point belongs to the dual proximal-gradient step set exactly when it is a proximal point of (1 / L) G at y^k - (1 / L) gradF(y^k).

class is_dual_based_proximal_gradient_dual_trajectory {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (F G : V → EReal) [InnerProductSpace ℝ V] [CompleteSpace V] {A : E →L[ℝ] V} {σ : ↑PosReal} (L : DualBasedProximalGradientDualStepsizeParameter A σ) (y : ℕ → V) (y0 : V) : Prop

Algorithm 12.1: given an initial point y^0 = y0 and a constant admissible parameter L ≥ ‖A‖² / σ, a sequence y is a dual proximal-gradient trajectory for the dual representation for the dual objective F + G when it starts at y0 and follows the canonical proximal-gradient trajectory for F + G with the constant parameter L.

• zero_eq : y 0 = y0
• trajectory : is_proximal_gradient_trajectory F G y fun (x : ℕ) => ↑L

theorem is_dual_based_proximal_gradient_dual_trajectory_zero {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F G : V → EReal} [InnerProductSpace ℝ V] [CompleteSpace V] {A : E →L[ℝ] V} {σ : ↑PosReal} {L : DualBasedProximalGradientDualStepsizeParameter A σ} {y : ℕ → V} {y0 : V} (h : is_dual_based_proximal_gradient_dual_trajectory F G L y y0) : y 0 = y0

A dual proximal-gradient trajectory starts from the prescribed initial point y^0 = y0.

theorem is_dual_based_proximal_gradient_dual_trajectory_step {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F G : V → EReal} [InnerProductSpace ℝ V] [CompleteSpace V] {A : E →L[ℝ] V} {σ : ↑PosReal} {L : DualBasedProximalGradientDualStepsizeParameter A σ} {y : ℕ → V} {y0 : V} (h : is_dual_based_proximal_gradient_dual_trajectory F G L y y0) (k : ℕ) : y k ∈ interior (effective_domain F) ∧ y (k + 1) ∈ proximal_gradient_step F G (y k) ↑L

At every iteration k, a dual proximal-gradient trajectory satisfies the Chapter 10 interior-domain condition and the constant-stepsize proximal-gradient update for F + G.

theorem dual_based_proximal_gradient_dual_step_eq_proximal_gradient_step {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (F G : V → EReal) (L : ↑PosReal) (yk : V) : dual_based_proximal_gradient_dual_step G (fun (y : V) => gradient (fun (z : V) => (F z).toReal) y) L yk = proximal_gradient_step F G yk L

The Chapter 12 dual-step formula with the canonical gradient of F is exactly the Chapter 10 proximal-gradient step for the composite objective F + G.

theorem is_dual_based_proximal_gradient_dual_trajectory.toIsProximalGradientTrajectory {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F G : V → EReal} {A : E →L[ℝ] V} {σ : ↑PosReal} {L : DualBasedProximalGradientDualStepsizeParameter A σ} {y : ℕ → V} {y0 : V} (h : is_dual_based_proximal_gradient_dual_trajectory F G L y y0) : is_proximal_gradient_trajectory F G y fun (x : ℕ) => ↑L

A Chapter 12 dual proximal-gradient trajectory is, by construction, the corresponding Chapter 10 proximal-gradient trajectory with constant parameter L.

theorem dual_based_proximal_gradient_identity_stepsize_parameter_lower_bound {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (σ : ↑PosReal) : dual_based_proximal_gradient_dual_lipschitz_constant (ContinuousLinearMap.id ℝ E) σ ≤ ↑σ⁻¹

The reciprocal parameter σ⁻¹ is an admissible dual proximal-gradient stepsize for the identity map.

@[reducible, inline]

noncomputable abbrev dual_based_proximal_gradient_identity_stepsize_parameter {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (σ : ↑PosReal) : DualBasedProximalGradientDualStepsizeParameter (ContinuousLinearMap.id ℝ E) σ

The canonical admissible dual proximal-gradient stepsize parameter for the identity map is the reciprocal value σ⁻¹.