def ClassicalSubgradientComplexityBenchmark (iter : ℝ → ℝ) : Prop

Definition 1.1.1 (Classical complexity benchmark for subgradient schemes). A classical worst-case iteration-complexity estimate for subgradient-type schemes for non-smooth convex minimization in the black-box oracle model is of order O(1/eps^2) (equation (1.1)), where eps > 0 is the desired absolute accuracy in objective value.

Equations

• ClassicalSubgradientComplexityBenchmark iter = ∃ C > 0, ∀ eps > 0, iter eps ≤ C / eps ^ 2

noncomputable def HardInstanceProblem (n : ℕ) : Set (Fin n → ℝ) × ((Fin n → ℝ) → ℝ)

Definition 1.1.2 (Constructive lower-bound illustration in the black-box model). In the black-box oracle model for non-smooth convex minimization, a cited hard instance is the problem of minimizing x ↦ max_{1 ≤ i ≤ n} x i subject to ∑ i, (x i)^2 ≤ 1 (equation (1.1) and (eq:intro:hard_instance)).

Equations

• HardInstanceProblem n = ({x : Fin n → ℝ | ∑ i : Fin n, x i ^ 2 ≤ 1}, fun (x : Fin n → ℝ) => sSup (Set.range x))

def SmoothConvexComplexityBenchmark (L : ℝ) (iter : ℝ → ℝ) : Prop

Definition 1.1.3 (Complexity benchmark for smooth convex minimization). For minimizing a convex function with L-Lipschitz continuous gradient by an optimal first-order method, the cited iteration complexity estimate is O(√(L/eps)) (equation (eq:intro:smooth_complexity)) for reaching absolute accuracy eps > 0 in objective value.

Equations

• SmoothConvexComplexityBenchmark L iter = ∃ C > 0, ∀ eps > 0, iter eps ≤ C * √(L / eps)

def DualPairing {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Module.Dual ℝ E) (x : E) : ℝ

Definition 1.1.4 (Spaces, duals, and pairing). Let E be a finite-dimensional real normed vector space and let E* be the dual space of linear functionals on E (mathlib Module.Dual). For s ∈ E* and x ∈ E, the pairing ⟪s, x⟫ is the value s x. When an inner product is used, the same bracket notation is employed, with an index when needed.

Equations

• DualPairing s x = s x

noncomputable def DualNormDef {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Module.Dual ℝ E) : ℝ

Definition 1.1.5 (Dual norm). Given a norm ‖·‖ on E, the dual norm ‖·‖_* on E* is defined by ‖s‖_* = max { ⟪s, x⟫ : x ∈ E, ‖x‖ = 1 } (equation (eq:dual_norm_def)).

Equations

• DualNormDef s = sSup {r : ℝ | ∃ (x : E), ‖x‖ = 1 ∧ r = DualPairing s x}

def AdjointOperator {E1 : Type u_1} {E2 : Type u_2} [SeminormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [SeminormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) : E2 →ₗ[ℝ] Module.Dual ℝ E1

Definition 1.1.6 (Adjoint operator). Let A : E1 → E2* be a linear operator. The adjoint A* : E2 → E1* is defined by ⟪A x, u⟫_2 = ⟪A* u, x⟫_1 for all x ∈ E1 and u ∈ E2 (equation (eq:adjoint_def)).

Equations

• AdjointOperator A = A.flip

noncomputable def OperatorNormDef {E1 : Type u_1} {E2 : Type u_2} [SeminormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [SeminormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) : ℝ

Definition 1.1.7 (Operator norm ‖A‖_{1,2}). For a linear operator A : E1 → E2*, define ‖A‖_{1,2} = max { ⟪A x, u⟫_2 : ‖x‖_1 = 1, ‖u‖_2 = 1 } (equation (eq:operator_norm_def)).

Equations

• OperatorNormDef A = sSup {r : ℝ | ∃ (x : E1) (u : E2), ‖x‖ = 1 ∧ ‖u‖ = 1 ∧ r = DualPairing (A x) u}

theorem dualPairing_adjointOperator {E1 : Type u_1} {E2 : Type u_2} [SeminormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [SeminormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) (u : E2) (x : E1) : DualPairing ((AdjointOperator A) u) x = DualPairing (A x) u

Adjoint pairing matches evaluation of the original map.

theorem norm_inv_smul_eq_one_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : E} (hu : u ≠ 0) : ‖‖u‖⁻¹ • u‖ = 1

Normalizing a nonzero vector by its norm gives unit norm.

theorem bddAbove_operatorNormDefSet {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) : BddAbove {r : ℝ | ∃ (x : E1) (v : E2), ‖x‖ = 1 ∧ ‖v‖ = 1 ∧ r = DualPairing (A x) v}

The operator-norm defining set is bounded above.

theorem dualPairing_le_operatorNormDef {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) {x : E1} {v : E2} (hx : ‖x‖ = 1) (hv : ‖v‖ = 1) : DualPairing (A x) v ≤ OperatorNormDef A

Unit-sphere pairing is bounded by the operator norm definition.

theorem adjointOperator_dualNorm_le_pointwise {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) (u : E2) {x : E1} (hx : ‖x‖ = 1) : DualPairing ((AdjointOperator A) u) x ≤ OperatorNormDef A * ‖u‖

Pointwise adjoint bound on the unit sphere.

theorem adjointOperator_dualNorm_le {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (A : E1 →ₗ[ℝ] Module.Dual ℝ E2) (u : E2) : DualNormDef ((AdjointOperator A) u) ≤ OperatorNormDef A * ‖u‖

Proposition 1.1.1. For any u ∈ E2, the adjoint operator satisfies the bound ‖A* u‖_{1,*} ≤ ‖A‖_{1,2} ‖u‖_2 (equation (eq:1.2)).