theorem quadratic_bound (r a L : ℝ) (hL : 0 < L) : r * a - 1 / (2 * L) * r ^ 2 ≤ 1 / 2 * L * a ^ 2

Quadratic bound used in the dual pairing estimate.

theorem dualNormDef_smul_le_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (a : ℝ) (ha : 0 ≤ a) (s : Module.Dual ℝ E) : DualNormDef (a • s) ≤ a * DualNormDef s

Dual norm is positively homogeneous (≤ direction) for nonnegative scalars.

theorem exists_dual_norming_functional_DualNormDef {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (h : E) (hh : h ≠ 0) : ∃ (s0 : Module.Dual ℝ E), DualNormDef s0 ≤ 1 ∧ DualPairing s0 h = ‖h‖

Existence of a dual functional attaining the norm on a nonzero vector.

theorem dualNormDef_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : DualNormDef 0 = 0

The dual norm of the zero functional is zero.

theorem dual_pairing_quadratic_sup_pointwise_upper {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (g : Module.Dual ℝ E) (h : E) (L : ℝ) (hL : 0 < L) (s : Module.Dual ℝ E) : DualPairing s h - 1 / (2 * L) * DualNormDef (s - g) ^ 2 ≤ DualPairing g h + 1 / 2 * L * ‖h‖ ^ 2

Pointwise upper bound for the dual quadratic payoff.

theorem dual_pairing_quadratic_sup_attaining_point {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (g : Module.Dual ℝ E) (h : E) (L : ℝ) (hL : 0 < L) : ∃ (s : Module.Dual ℝ E), DualPairing g h + 1 / 2 * L * ‖h‖ ^ 2 ≤ DualPairing s h - 1 / (2 * L) * DualNormDef (s - g) ^ 2

A candidate point achieving the lower bound in the dual supremum.

theorem dual_pairing_quadratic_sup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (g : Module.Dual ℝ E) (h : E) (L : ℝ) (hL : 0 < L) : DualPairing g h + 1 / 2 * L * ‖h‖ ^ 2 = sSup ((fun (s : Module.Dual ℝ E) => DualPairing s h - 1 / (2 * L) * DualNormDef (s - g) ^ 2) '' Set.univ)

Lemma 1.5.1. For any g ∈ E*, h ∈ E, and L > 0, we have ⟪g, h⟫_1 + (1/2) L ‖h‖_1^2 = max_{s ∈ E*} { ⟪s, h⟫_1 - (1/(2L)) ‖s - g‖_{1,*}^2 } (equation (eq:lem6)).

noncomputable def simplexProximalValue (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) : ℝ

Definition 1.5.1. Let xbar ∈ Δ_n and gbar ∈ ℝ^n. Define the proximal subproblem value for the simplex with the l1-norm by psi* = min_{x ∈ Δ_n} { <gbar, x - xbar>_1 + (1/2) L ‖x - xbar‖_1^2 } (equation (5.1)).

Equations

• simplexProximalValue n xbar gbar L = sInf ((fun (x : Fin n → ℝ) => ∑ i : Fin n, gbar i * (x i - xbar i) + 1 / 2 * L * (∑ i : Fin n, |x i - xbar i|) ^ 2) '' standardSimplex n)

theorem simplex_sum_sub_eq_zero {n : ℕ} {x xbar : Fin n → ℝ} (hx : x ∈ standardSimplex n) (hxbar : xbar ∈ standardSimplex n) : ∑ i : Fin n, (x i - xbar i) = 0

On the simplex, the coordinatewise sum of a difference is zero.

theorem simplexProximalValue_shift_gbar_const (n : ℕ) (xbar gbar : Fin n → ℝ) (L c : ℝ) (hxbar : xbar ∈ standardSimplex n) : simplexProximalValue n xbar (fun (i : Fin n) => gbar i + c) L = simplexProximalValue n xbar gbar L

Shifting gbar by a constant does not change the simplex proximal value.

theorem sInf_image_sub_sInf_eq_zero_fin (n : ℕ) (gbar : Fin n → ℝ) (hn : 0 < n) : have α := sInf ((fun (i : Fin n) => gbar i) '' Set.univ); sInf ((fun (i : Fin n) => gbar i - α) '' Set.univ) = 0

Shifting by the minimum coordinate makes the infimum zero for a finite index set.

theorem simplexProximalValue_wlog_min_zero (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hxbar : xbar ∈ standardSimplex n) : ∃ (gbar' : Fin n → ℝ), sInf ((fun (i : Fin n) => gbar' i) '' Set.univ) = 0 ∧ simplexProximalValue n xbar gbar' L = simplexProximalValue n xbar gbar L

Proposition 1.5.1. In the setting of Definition 1.5.1, we may normalize gbar so that min_{1 ≤ i ≤ n} gbar^(i) = 0 (equation (5.2)) without changing the proximal value.

theorem sign_mul_eq_abs (r : ℝ) : r.sign * r = |r|

The real sign recovers absolute value by multiplication.

noncomputable def simplexProximalValue_signPlus (z : ℝ) : ℝ

One-sided sign for right-derivatives of |·|.

Equations

• simplexProximalValue_signPlus z = if z < 0 then -1 else 1

noncomputable def simplexProximalValue_signMinus (z : ℝ) : ℝ

One-sided sign for left-derivatives of |·|.

Equations

• simplexProximalValue_signMinus z = if 0 < z then 1 else -1

theorem simplexProximalValue_abs_add_oneSided (z t : ℝ) (ht : 0 ≤ t) (htle : z < 0 → t ≤ -z) : |z + t| = |z| + simplexProximalValue_signPlus z * t

One-sided absolute value expansion for z + t with t ≥ 0.

theorem simplexProximalValue_abs_sub_oneSided (z t : ℝ) (ht : 0 ≤ t) (htle : 0 < z → t ≤ z) : |z - t| = |z| - simplexProximalValue_signMinus z * t

One-sided absolute value expansion for z - t with t ≥ 0.

theorem sum_mul_le_norm_sum_abs (n : ℕ) (s h : Fin n → ℝ) : ∑ i : Fin n, s i * h i ≤ ‖s‖ * ∑ i : Fin n, |h i|

The dot product is bounded by the sup norm times the l1 norm.

theorem dot_l1Quadratic_eq_sSup_linf_fin (n : ℕ) (g h : Fin n → ℝ) (L : ℝ) (hL : 0 < L) : ∑ i : Fin n, g i * h i + 1 / 2 * L * (∑ i : Fin n, |h i|) ^ 2 = sSup ((fun (s : Fin n → ℝ) => ∑ i : Fin n, (g i + s i) * h i - 1 / (2 * L) * ‖s‖ ^ 2) '' Set.univ)

A finite-dimensional l1/l∞ quadratic conjugacy identity.

theorem simplexProximalValue_as_minimax_fin (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hL : 0 < L) : simplexProximalValue n xbar gbar L = sInf ((fun (x : Fin n → ℝ) => sSup ((fun (s : Fin n → ℝ) => ∑ i : Fin n, (gbar i + s i) * (x i - xbar i) - 1 / (2 * L) * ‖s‖ ^ 2) '' Set.univ)) '' standardSimplex n)

Rewriting the simplex proximal value as a min-max expression.

theorem dual_inner_min_over_simplex (n : ℕ) (r : Fin n → ℝ) : sInf ((fun (x : Fin n → ℝ) => ∑ i : Fin n, r i * x i) '' standardSimplex n) = sInf (r '' Set.univ)

The infimum of a linear form over the simplex equals the minimum coefficient.

theorem simplexProximalValue_minmax_exchange_fin_le (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hn : 0 < n) (hL : 0 < L) : sSup ((fun (s : Fin n → ℝ) => sInf ((fun (x : Fin n → ℝ) => ∑ i : Fin n, (gbar i + s i) * (x i - xbar i) - 1 / (2 * L) * ‖s‖ ^ 2) '' standardSimplex n)) '' Set.univ) ≤ sInf ((fun (x : Fin n → ℝ) => sSup ((fun (s : Fin n → ℝ) => ∑ i : Fin n, (gbar i + s i) * (x i - xbar i) - 1 / (2 * L) * ‖s‖ ^ 2) '' Set.univ)) '' standardSimplex n)

The trivial minimax inequality (sup-inf ≤ inf-sup) for the finite simplex payoff.

theorem simplexProximalValue_minmax_exchange_fin_le_of_saddlePoint (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hL : 0 < L) (hsaddle : ∃ xstar ∈ standardSimplex n, ∃ (sstar : Fin n → ℝ), (∀ (s : Fin n → ℝ), ∑ i : Fin n, (gbar i + s i) * (xstar i - xbar i) - 1 / (2 * L) * ‖s‖ ^ 2 ≤ ∑ i : Fin n, (gbar i + sstar i) * (xstar i - xbar i) - 1 / (2 * L) * ‖sstar‖ ^ 2) ∧ ∀ x ∈ standardSimplex n, ∑ i : Fin n, (gbar i + sstar i) * (xstar i - xbar i) - 1 / (2 * L) * ‖sstar‖ ^ 2 ≤ ∑ i : Fin n, (gbar i + sstar i) * (x i - xbar i) - 1 / (2 * L) * ‖sstar‖ ^ 2) : sInf ((fun (x : Fin n → ℝ) => sSup ((fun (s : Fin n → ℝ) => ∑ i : Fin n, (gbar i + s i) * (x i - xbar i) - 1 / (2 * L) * ‖s‖ ^ 2) '' Set.univ)) '' standardSimplex n) ≤ sSup ((fun (s : Fin n → ℝ) => sInf ((fun (x : Fin n → ℝ) => ∑ i : Fin n, (gbar i + s i) * (x i - xbar i) - 1 / (2 * L) * ‖s‖ ^ 2) '' standardSimplex n)) '' Set.univ)

A saddle point yields infsup ≤ supinf for the finite simplex payoff.