def alphaNormPenalty {E : Type u} [AddCommGroup E] [Module ℝ E] (alpha : Seminorm ℝ E) (lam : ℝ) : E → EReal

The penalty x ↦ λ ‖x‖_α built from the auxiliary seminorm alpha.

@[simp]

theorem alphaNormPenalty_apply {E : Type u} [AddCommGroup E] [Module ℝ E] (alpha : Seminorm ℝ E) (lam : ℝ) (x : E) : alphaNormPenalty alpha lam x = ↑(lam * alpha x)

Evaluating alphaNormPenalty alpha λ at x gives the scalar value λ ‖x‖_α.

def alphaDualUnitBall {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (alpha : Seminorm ℝ E) : Set E

The closed dual unit ball {y ∈ E | ‖y‖_{α,*} ≤ 1} under the ambient Riesz identification y ↦ toDualMap ℝ E y, defined through the support function of the canonical seminorm unit ball alpha.closedBall 0 1.

@[simp]

theorem mem_alphaDualUnitBall_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (alpha : Seminorm ℝ E) (y : E) : y ∈ alphaDualUnitBall alpha ↔ (σ_ (alpha.closedBall 0 1)) ↑((InnerProductSpace.toDualMap ℝ E) y) ≤ 1

A point belongs to alphaDualUnitBall alpha exactly when its Riesz functional has auxiliary dual norm at most 1.

theorem mem_alphaDualUnitBall_iff_le_seminorm {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (alpha : Seminorm ℝ E) (y : E) : y ∈ alphaDualUnitBall alpha ↔ ∀ (z : E), ((InnerProductSpace.toDualMap ℝ E) y) z ≤ alpha z

Helper for Example 6.47: a vector lies in the auxiliary dual unit ball exactly when its Riesz functional is pointwise dominated by the auxiliary seminorm.

theorem alphaDualUnitBall_nonempty {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (alpha : Seminorm ℝ E) : (alphaDualUnitBall alpha).Nonempty

The dual unit ball of the auxiliary norm is nonempty.

theorem alphaDualUnitBall_isClosed {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (alpha : Seminorm ℝ E) : IsClosed (alphaDualUnitBall alpha)

The dual unit ball of the auxiliary norm is closed in the ambient Euclidean topology.

theorem alphaDualUnitBall_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (alpha : Seminorm ℝ E) : Convex ℝ (alphaDualUnitBall alpha)

The dual unit ball of the auxiliary norm is convex.

theorem support_function_alphaDualUnitBall_eq_alpha {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (alpha : Seminorm ℝ E) (x : E) : (σ_ (alphaDualUnitBall alpha)) ↑((InnerProductSpace.toDualMap ℝ E) x) = ↑(alpha x)

The support function of the auxiliary dual unit ball recovers the auxiliary norm ‖·‖_α.

theorem alphaNormPenalty_eq_smul_support_function_primal_alphaDualUnitBall {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (alpha : Seminorm ℝ E) (lam : ℝ) : alphaNormPenalty alpha lam = ↑lam • σ[alphaDualUnitBall alpha]

Helper for Example 6.47: the auxiliary penalty is the scalar multiple of the support function of its auxiliary dual unit ball.

theorem prox_alphaNormPenalty_eq_sub_smul_projection_mapping_alphaDualUnitBall {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (alpha : Seminorm ℝ E) (lam : ℝ) (hlam : 0 < lam) (x : E) : prox[alphaNormPenalty alpha lam] x = (fun (u : E) => x - lam • u) '' P[alphaDualUnitBall alpha] (lam⁻¹ • x)

Example 6.47: let f(x) = λ ‖x‖_α for λ > 0, where the source norm ‖·‖_α on the ambient Euclidean space E is encoded by the canonical owner alpha : Seminorm ℝ E, and let C = {y ∈ E | ‖y‖_{α,*} ≤ 1} be its dual unit ball under the Riesz identification E ≃ E*. Then the proximal mapping of f is the affine image of the projection set P[alphaDualUnitBall alpha] (x / λ) under u ↦ x - λ • u. This is the chapter's set-valued rendering of the textbook identity prox_{λ ‖·‖_α}(x) = x - λ P_C(x / λ).