@[simp]

theorem mem_adlpmm_x_step_linear_composite_iff {X : Type u} {Y : Type v} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] {f₁ : X → EReal} {ρ : ↑PosReal} {A : X →ₗ[ℝ] Y} {α : ↑PosReal} {xk xNext : X} {zk yk : Y} : xNext ∈ adlpmm_x_step f₁ ρ α A (-LinearMap.id) 0 xk zk yk ↔ xNext ∈ prox[↑↑(1 / α) • f₁] (xk - ↑(ρ / α) • (LinearMap.adjoint A) (A xk - zk + (1 / ↑ρ) • yk))

In the linear-composite specialization B = -I, c = 0, membership in the AD-LPMM x-update set is exactly the textbook proximal clause x^(k+1) ∈ prox[((1 / α) f₁)] (x^k - (ρ / α) Aᵀ (A x^k - z^k + (1 / ρ) y^k)).

@[simp]

theorem mem_adlpmm_z_step_linear_composite_iff {X : Type u} {Y : Type v} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] {f₂ : Y → EReal} {ρ β : ↑PosReal} {A : X →ₗ[ℝ] Y} {xNext : X} {zk yk zNext : Y} : zNext ∈ adlpmm_z_step f₂ ρ β A (-LinearMap.id) 0 xNext zk yk ↔ zNext ∈ prox[↑↑(1 / β) • f₂] (zk + ↑(ρ / β) • (A xNext - zk + (1 / ↑ρ) • yk))

In the linear-composite specialization B = -I, c = 0, membership in the AD-LPMM z-update set is exactly the textbook proximal clause z^(k+1) ∈ prox[((1 / β) f₂)] (z^k + (ρ / β) (A x^(k+1) - z^k + (1 / ρ) y^k)).

theorem IsADLPMMTrajectory.x_step_linear_composite {X : Type u} {Y : Type v} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] {ρ : ↑PosReal} {A : X →ₗ[ℝ] Y} {α : ADLPMMLinearizationParameter ρ A} {β : ADLPMMLinearizationParameter ρ (-LinearMap.id)} {h₁ : X → EReal} {h₂ : Y → EReal} {x : ℕ → X} {z y : ℕ → Y} {x0 : X} {z0 y0 : Y} (h : IsADLPMMTrajectory ρ A (-LinearMap.id) 0 α β h₁ h₂ x z y x0 z0 y0) (k : ℕ) : x (k + 1) ∈ prox[↑↑(1 / ↑α) • h₁] (x k - ↑(ρ / ↑α) • (LinearMap.adjoint A) (A (x k) - z k + (1 / ↑ρ) • y k))

In the linear-composite specialization of Algorithm 15.8, the generic AD-LPMM x-step is exactly the textbook proximal update from part (a).

theorem IsADLPMMTrajectory.z_step_linear_composite {X : Type u} {Y : Type v} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] {ρ : ↑PosReal} {A : X →ₗ[ℝ] Y} {α : ADLPMMLinearizationParameter ρ A} {β : ADLPMMLinearizationParameter ρ (-LinearMap.id)} {h₁ : X → EReal} {h₂ : Y → EReal} {x : ℕ → X} {z y : ℕ → Y} {x0 : X} {z0 y0 : Y} (h : IsADLPMMTrajectory ρ A (-LinearMap.id) 0 α β h₁ h₂ x z y x0 z0 y0) (k : ℕ) : z (k + 1) ∈ prox[↑↑(1 / ↑β) • h₂] (z k + ↑(ρ / ↑β) • (A (x (k + 1)) - z k + (1 / ↑ρ) • y k))

In the linear-composite specialization of Algorithm 15.8, the generic AD-LPMM z-step is exactly the textbook proximal update from part (b).

theorem IsADLPMMTrajectory.y_step_linear_composite {X : Type u} {Y : Type v} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] {ρ : ↑PosReal} {A : X →ₗ[ℝ] Y} {α : ADLPMMLinearizationParameter ρ A} {β : ADLPMMLinearizationParameter ρ (-LinearMap.id)} {h₁ : X → EReal} {h₂ : Y → EReal} {x : ℕ → X} {z y : ℕ → Y} {x0 : X} {z0 y0 : Y} (h : IsADLPMMTrajectory ρ A (-LinearMap.id) 0 α β h₁ h₂ x z y x0 z0 y0) (k : ℕ) : y (k + 1) = y k + ↑ρ • (A (x (k + 1)) - z (k + 1))

In the linear-composite specialization of Algorithm 15.8, the generic AD-LPMM multiplier update simplifies to y^(k+1) = y^k + ρ (A x^(k+1) - z^(k+1)).