noncomputable def MainOptimizationProblemValue {E1 : Type u_1} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] (Q1 : Set E1) (f : E1 → ℝ) : ℝ

Definition 1.2.1 (Main problem). Let Q1 be a bounded closed convex set in a finite-dimensional real vector space E1, and let f : E1 → ℝ be continuous and convex on Q1. The main optimization problem is f* = min { f x : x ∈ Q1 } (equation (2.1)).

Equations

• MainOptimizationProblemValue Q1 f = sInf (f '' Q1)

def AdmitsExplicitMaxStructure {E1 : Type u} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] (Q1 : Set E1) (f : E1 → ℝ) : Prop

Definition 1.2.2 (Explicit max-structure model). We say that f admits an explicit max-structure if there exist a finite-dimensional real vector space E2, a closed convex bounded set Q2 in E2, a linear operator A : E1 → E2*, and continuous convex functions fhat : Q1 → ℝ and phihat : Q2 → ℝ, such that for all x ∈ Q1, f x = fhat x + max { <A x, u>_2 - phihat u : u ∈ Q2 } (equation (2.2)). The text also notes an implicit simplicity assumption on phihat and Q2, and illustrates non-uniqueness via the conjugate representation (equation (conjugate_representation)).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AdjointFormPotential {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (Q1 : Set E1) (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (fhat : E1 → ℝ) (phihat : E2 → ℝ) : ↑Q2 → ℝ

Definition 1.2.3 (Adjoint form). Assume equation (2.2). Define φ : Q2 → ℝ by φ(u) = -phihat u + min { ⟪A x, u⟫_2 + fhat x : x ∈ Q1 } (equation (2.3)).

Equations

• AdjointFormPotential Q1 Q2 A fhat phihat u = -phihat ↑u + sInf ((fun (x : E1) => (A x) ↑u + fhat x) '' Q1)

noncomputable def AdjointOptimizationProblemValue {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (Q1 : Set E1) (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (fhat : E1 → ℝ) (phihat : E2 → ℝ) : ℝ

Definition 1.2.3 (Adjoint form, adjoint optimization problem). Assume equation (2.2). The associated adjoint optimization problem is max { φ(u) : u ∈ Q2 } (equation (adjoint_problem)).

Equations

• AdjointOptimizationProblemValue Q1 Q2 A fhat phihat = sSup (Set.range (AdjointFormPotential Q1 Q2 A fhat phihat))

theorem image_eq_setOf_exists_eq {α : Type u_1} (g : α → ℝ) (p : α → Prop) : g '' {x : α | p x} = {r : ℝ | ∃ (x : α), p x ∧ r = g x}

Rewriting an image as a set of existence statements.

theorem maxAbs_l1_duality_fin_succ {m : ℕ} (t : Fin m.succ → ℝ) : sSup (Set.range fun (j : Fin m.succ) => |t j|) = sSup {r : ℝ | ∃ (u : Fin m.succ → ℝ), ∑ j : Fin m.succ, |u j| ≤ 1 ∧ r = ∑ j : Fin m.succ, u j * t j}

The ℓ¹-ℓ∞ duality identity for Fin (succ m) indices.

theorem l1Ball_closed_convex_bounded_succ {m : ℕ} : have Q2 := {u : Fin m.succ → ℝ | ∑ j : Fin m.succ, |u j| ≤ 1}; IsClosed Q2 ∧ Convex ℝ Q2 ∧ Bornology.IsBounded Q2

The ℓ¹-ball in Fin (succ m) → ℝ is closed, convex, and bounded.

theorem maxAbs_simplexLift_exists_of_l1Ball_succ {m : ℕ} {u : Fin m.succ → ℝ} (hu : ∑ j : Fin m.succ, |u j| ≤ 1) : ∃ (u1 : Fin m.succ → ℝ) (u2 : Fin m.succ → ℝ), (∀ (j : Fin m.succ), 0 ≤ u1 j) ∧ (∀ (j : Fin m.succ), 0 ≤ u2 j) ∧ ∑ j : Fin m.succ, (u1 j + u2 j) = 1 ∧ ∀ (j : Fin m.succ), u j = u1 j - u2 j

Simplex lifting: split an ℓ¹-ball element into nonnegative parts with slack.

theorem maxAbs_l1Ball_exists_of_simplexLift_succ {m : ℕ} {u1 u2 : Fin m.succ → ℝ} (hu1 : ∀ (j : Fin m.succ), 0 ≤ u1 j) (hu2 : ∀ (j : Fin m.succ), 0 ≤ u2 j) (hsum : ∑ j : Fin m.succ, (u1 j + u2 j) = 1) : ∑ j : Fin m.succ, |u1 j - u2 j| ≤ 1

Simplex lifting: a simplex point yields an ℓ¹-ball point.

theorem maxAbs_simplex_lifting_valueSet_eq_succ {m : ℕ} (t : Fin m.succ → ℝ) : {r : ℝ | ∃ (u : Fin m.succ → ℝ), ∑ j : Fin m.succ, |u j| ≤ 1 ∧ r = ∑ j : Fin m.succ, u j * t j} = {r : ℝ | ∃ (u1 : Fin m.succ → ℝ) (u2 : Fin m.succ → ℝ), (∀ (j : Fin m.succ), 0 ≤ u1 j) ∧ (∀ (j : Fin m.succ), 0 ≤ u2 j) ∧ ∑ j : Fin m.succ, (u1 j + u2 j) = 1 ∧ r = ∑ j : Fin m.succ, (u1 j - u2 j) * t j}

Simplex lifting for the ℓ¹-ball representation on Fin (succ m).

theorem maxAbs_A_phihat_succ_eval {E1 : Type u_1} [NormedAddCommGroup E1] [NormedSpace ℝ E1] {m : ℕ} (a : Fin m.succ → E1 →L[ℝ] ℝ) (b : Fin m.succ → ℝ) (x : E1) (u : Fin m.succ → ℝ) : have projCLM := fun (j : Fin m.succ) => LinearMap.toContinuousLinearMap { toFun := fun (u : Fin m.succ → ℝ) => u j, map_add' := ⋯, map_smul' := ⋯ }; ((∑ j : Fin m.succ, (a j).smulRight (projCLM j)) x) u - (∑ j : Fin m.succ, b j • projCLM j) u = ∑ j : Fin m.succ, u j * ((a j) x - b j)

Evaluation formula for the Fin (succ m) linear maps.

theorem maxAbs_admitsExplicitMaxStructure_succ {E1 : Type u_1} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] {m : ℕ} (a : Fin m.succ → E1 →L[ℝ] ℝ) (b : Fin m.succ → ℝ) : AdmitsExplicitMaxStructure Set.univ fun (x : E1) => sSup (Set.range fun (j : Fin m.succ) => |(a j) x - b j|)

Explicit max-structure in the Fin (succ m) case.

theorem maxAbs_explicit_max_structure {E1 : Type u_1} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] {m : ℕ} (a : Fin m → E1 →L[ℝ] ℝ) (b : Fin m → ℝ) : have f := fun (x : E1) => sSup (Set.range fun (j : Fin m) => |(a j) x - b j|); AdmitsExplicitMaxStructure Set.univ f ∧ (∃ (phihat : (E1 →L[ℝ] ℝ) → ℝ), ∀ (u : E1 →L[ℝ] ℝ), phihat u = sInf {r : ℝ | ∃ (s : Fin m → ℝ), u = ∑ j : Fin m, s j • a j ∧ ∑ j : Fin m, |s j| ≤ 1 ∧ r = ∑ j : Fin m, s j * b j}) ∧ (∀ (x : E1), f x = sSup {r : ℝ | ∃ (u : Fin m → ℝ), ∑ j : Fin m, |u j| ≤ 1 ∧ r = ∑ j : Fin m, u j * ((a j) x - b j)}) ∧ ∀ (x : E1), f x = sSup {r : ℝ | ∃ (u1 : Fin m → ℝ) (u2 : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ u1 j) ∧ (∀ (j : Fin m), 0 ≤ u2 j) ∧ ∑ j : Fin m, (u1 j + u2 j) = 1 ∧ r = ∑ j : Fin m, (u1 j - u2 j) * ((a j) x - b j)}

Proposition 1.2.1. Let a_1, …, a_m ∈ E1* and b ∈ ℝ^m, and define f(x) = max_{1 ≤ j ≤ m} |⟪a_j, x⟫_1 - b^(j)| (equation (eq:ex1:f_def)). Then f admits explicit max-structure representations (equation (2.2)). In particular:

1. (Conjugate-style representation.) Taking A = I, E2 = E1*, one can define phihat by the minimum over s ∈ ℝ^m with u = ∑ s^(j) a_j and ∑ |s^(j)| ≤ 1 (equation (eq:ex1:phi_hat_conjugate_like)).
2. (ℝ^m representation.) One can write f(x) = max_{u ∈ ℝ^m} { ∑ u^(j)(⟪a_j, x⟫_1 - b^(j)) : ∑ |u^(j)| ≤ 1 } (equation (eq:ex1:Rm_representation)), so Q2 is the l1-ball and phihat(u) = ⟪b, u⟫_2.
3. (Simplex lifting.) Using u = (u_1, u_2) ∈ ℝ^{2m} with u ≥ 0 and ∑ (u_1^(j) + u_2^(j)) = 1, one obtains the simplex representation (equation (eq:ex1:simplex_representation)).

def IsProxFunction {E2 : Type u_1} [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (d2 : E2 → ℝ) : Prop

Definition 1.2.4 (Prox-function and prox-center). Let Q2 ⊆ E2 be closed, convex, and bounded. A function d2 : Q2 → ℝ is a prox-function for Q2 if it is continuous and σ2-strongly convex on Q2 for some σ2 > 0. We may normalize d2 so that d2 u0 = 0 at a prox-center.

Equations

• IsProxFunction Q2 d2 = ∃ σ2 > 0, ContinuousOn d2 Q2 ∧ StrongConvexOn Q2 σ2 d2

def IsProxCenter {E2 : Type u_1} [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (d2 : E2 → ℝ) (u0 : E2) : Prop

Definition 1.2.4 (Prox-function and prox-center). A prox-center u0 ∈ Q2 is any minimizer u0 ∈ argmin { d2 u : u ∈ Q2 } (equation (prox_center_def)).

Equations

• IsProxCenter Q2 d2 u0 = (u0 ∈ Q2 ∧ IsMinOn d2 Q2 u0)

theorem le_of_forall_one_sub_mul_le {a b c : ℝ} (h : ∀ t ∈ Set.Ioo 0 1, a + (1 - t) * c ≤ b) : a + c ≤ b

If a + (1 - t) * c ≤ b for all t ∈ (0,1), then a + c ≤ b.

theorem prox_center_lower_bound_aux_t {E2 : Type u_1} [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (d2 : E2 → ℝ) (σ2 : ℝ) (u0 : E2) (hconv : StrongConvexOn Q2 σ2 d2) (hu0 : IsProxCenter Q2 d2 u0) {u : E2} (hu : u ∈ Q2) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : d2 u0 + (1 - t) * (σ2 / 2 * ‖u0 - u‖ ^ 2) ≤ d2 u

Intermediate inequality for a fixed t ∈ (0,1).

theorem prox_center_lower_bound {E2 : Type u_1} [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (d2 : E2 → ℝ) (σ2 : ℝ) (u0 : E2) (hconv : StrongConvexOn Q2 σ2 d2) (hu0 : IsProxCenter Q2 d2 u0) (h0 : d2 u0 = 0) (u : E2) : u ∈ Q2 → d2 u ≥ 1 / 2 * σ2 * ‖u - u0‖ ^ 2

Proposition 1.2.2. Assume d2 is σ2-strongly convex on Q2, and let u0 be a prox-center normalized by d2 u0 = 0. Then for all u ∈ Q2, d2 u ≥ (1/2) σ2 ‖u - u0‖^2 (equation (2.4)).

noncomputable def SmoothedMaxFunction {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) : E1 → ℝ

Definition 1.2.5 (Smoothed max-function). Let μ > 0. Define f_μ(x) = max { ⟪A x, u⟫_2 - phihat u - μ d2 u : u ∈ Q2 } (equation (2.5)). Denote by u_μ(x) ∈ Q2 an optimal solution (a maximizer) of (2.5). Since d2 is strongly convex and phihat is convex on Q2, the maximizer is unique.

Equations

• SmoothedMaxFunction Q2 A phihat d2 μ x = sSup ((fun (u : E2) => (A x) u - phihat u - μ * d2 u) '' Q2)

def IsSmoothedMaximizer {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (x : E1) (u : E2) : Prop

Definition 1.2.5 (Smoothed max-function, maximizers). A point u ∈ Q2 is a maximizer for the smoothed max-function at x if it attains the maximum in (2.5).

Equations

• IsSmoothedMaximizer Q2 A phihat d2 μ x u = (u ∈ Q2 ∧ ∀ v ∈ Q2, (A x) v - phihat v - μ * d2 v ≤ (A x) u - phihat u - μ * d2 u)

theorem smoothedMaxFunction_eq_of_isSmoothedMaximizer {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (x : E1) (u : E2) (hU : IsSmoothedMaximizer Q2 A phihat d2 μ x u) : SmoothedMaxFunction Q2 A phihat d2 μ x = (A x) u - phihat u - μ * d2 u ∧ BddAbove ((fun (u : E2) => (A x) u - phihat u - μ * d2 u) '' Q2)

A maximizer attains the smoothed max-function and yields a bounded-above image set.

theorem smoothedMaxFunction_convexOn_univ {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (uμ : E1 → E2) (hmax : ∀ (x : E1), IsSmoothedMaximizer Q2 A phihat d2 μ x (uμ x)) : ConvexOn ℝ Set.univ (SmoothedMaxFunction Q2 A phihat d2 μ)

The smoothed max-function is convex on Set.univ when maximizers exist everywhere.

theorem d2_le_D2_section02 {E2 : Type u_1} (Q2 : Set E2) (d2 : E2 → ℝ) (hbdd_d2 : BddAbove (d2 '' Q2)) {u : E2} (hu : u ∈ Q2) : d2 u ≤ sSup (d2 '' Q2)

Values of d2 on Q2 are bounded above by the supremum D2.

theorem bddAbove_smoothedImage_of_bddAbove_base_section02 {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (x : E1) (hbdd0x : BddAbove ((fun (u : E2) => (A x) u - phihat u) '' Q2)) (hμ : 0 ≤ μ) (hd2_nonneg : ∀ u ∈ Q2, 0 ≤ d2 u) : BddAbove ((fun (u : E2) => (A x) u - phihat u - μ * d2 u) '' Q2)

Boundedness of the smoothed image set from boundedness of the unsmoothed one.

theorem smoothedMaxFunction_le_f0_section02 {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (x : E1) (hbdd0x : BddAbove ((fun (u : E2) => (A x) u - phihat u) '' Q2)) (hμ : 0 ≤ μ) (hd2_nonneg : ∀ u ∈ Q2, 0 ≤ d2 u) : sSup ((fun (u : E2) => (A x) u - phihat u - μ * d2 u) '' Q2) ≤ sSup ((fun (u : E2) => (A x) u - phihat u) '' Q2)

Smoothed max-function is bounded above by the unsmoothed max-function.

theorem f0_le_smoothedMaxFunction_add_section02 {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (x : E1) (hbdd0x : BddAbove ((fun (u : E2) => (A x) u - phihat u) '' Q2)) (hbdd_d2 : BddAbove (d2 '' Q2)) (hμ : 0 ≤ μ) (hd2_nonneg : ∀ u ∈ Q2, 0 ≤ d2 u) : sSup ((fun (u : E2) => (A x) u - phihat u) '' Q2) ≤ sSup ((fun (u : E2) => (A x) u - phihat u - μ * d2 u) '' Q2) + μ * sSup (d2 '' Q2)

Unsmooth max-function is bounded by the smoothed max plus μ * D2.

theorem smoothedMaxFunction_bounds {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (hμ : 0 ≤ μ) (hd2_nonneg : ∀ u ∈ Q2, 0 ≤ d2 u) (hbdd0 : ∀ (x : E1), BddAbove ((fun (u : E2) => (A x) u - phihat u) '' Q2)) (hbdd_d2 : BddAbove (d2 '' Q2)) : have D2 := sSup (d2 '' Q2); have f0 := fun (x : E1) => sSup ((fun (u : E2) => (A x) u - phihat u) '' Q2); have fμ := SmoothedMaxFunction Q2 A phihat d2 μ; ∀ (x : E1), fμ x ≤ f0 x ∧ f0 x ≤ fμ x + μ * D2

Proposition 1.2.3. Define D2 = max { d2 u : u ∈ Q2 } (equation (eq:D2_def)) and f0(x) = max { ⟪A x, u⟫_2 - phihat u : u ∈ Q2 } (equation (eq:f0_def)). Then for all x ∈ E1, f_μ(x) ≤ f0(x) ≤ f_μ(x) + μ D2 (equation (2.7)).