theorem simplexProximalValue_exists_primalMinimizer_fin (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hn : 0 < n) : ∃ xstar ∈ standardSimplex n, IsMinOn (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) xstar

A continuous objective attains its minimum on the finite simplex.

theorem standardSimplex_mass_transfer_mem {n : ℕ} {x : Fin n → ℝ} (hx : x ∈ standardSimplex n) {i j : Fin n} (hij : i ≠ j) {t : ℝ} (ht0 : 0 ≤ t) (htle : t ≤ x i) : (fun (k : Fin n) => if k = i then x k - t else if k = j then x k + t else x k) ∈ standardSimplex n

Moving mass between two coordinates preserves membership in the simplex.

theorem simplexProximalValue_small_t_linear_from_linear_quadratic {A B t0 : ℝ} (hB : 0 ≤ B) (ht0 : 0 < t0) (hineq : ∀ (t : ℝ), 0 < t → t ≤ t0 → 0 ≤ t * A + t ^ 2 * B) : 0 ≤ A

Extract the linear coefficient from a nonnegative quadratic for small t.

theorem simplexProximalValue_primal_optimality_transfer_ineq (n : ℕ) (xbar gbar xstar : Fin n → ℝ) (L : ℝ) (hL : 0 < L) (hxstar : xstar ∈ standardSimplex n) (hxmin : IsMinOn (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) xstar) {i j : Fin n} (hpos : 0 < xstar i) : have h := fun (k : Fin n) => xstar k - xbar k; have a := ∑ k : Fin n, |h k|; gbar i + L * a * simplexProximalValue_signMinus (h i) ≤ gbar j + L * a * simplexProximalValue_signPlus (h j)

Primal optimality yields a transfer inequality between coordinates.

theorem dot_l1Quadratic_argmax_fin_with_free_zero_coords (n : ℕ) (g h sstar : Fin n → ℝ) (L : ℝ) (hL : 0 < L) (hmatch : ∀ (i : Fin n), h i ≠ 0 → sstar i = (L * ∑ i : Fin n, |h i|) * (h i).sign) (hbound : ∀ (i : Fin n), |sstar i| ≤ L * ∑ i : Fin n, |h i|) (s : Fin n → ℝ) : ∑ i : Fin n, (g i + s i) * h i - 1 / (2 * L) * ‖s‖ ^ 2 ≤ ∑ i : Fin n, (g i + sstar i) * h i - 1 / (2 * L) * ‖sstar‖ ^ 2

A maximizer for the finite l1/l∞ quadratic payoff, allowing free coordinates when h i = 0.

theorem simplexProximalValue_signPlus_eq_real_sign_of_ne_zero {z : ℝ} (hz : z ≠ 0) : simplexProximalValue_signPlus z = z.sign

One-sided signs agree with Real.sign away from zero (right derivative).

theorem simplexProximalValue_signMinus_eq_real_sign_of_ne_zero {z : ℝ} (hz : z ≠ 0) : simplexProximalValue_signMinus z = z.sign

One-sided signs agree with Real.sign away from zero (left derivative).

theorem simplexProximalValue_exists_sstar_support_constant (n : ℕ) (xbar gbar xstar : Fin n → ℝ) (L : ℝ) (hL : 0 < L) (hxstar : xstar ∈ standardSimplex n) (hxmin : IsMinOn (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) xstar) : have h := fun (i : Fin n) => xstar i - xbar i; have a := ∑ i : Fin n, |h i|; ∃ (c : ℝ) (sstar : Fin n → ℝ), (∀ (i : Fin n), h i ≠ 0 → sstar i = L * a * (h i).sign) ∧ (∀ (i : Fin n), |sstar i| ≤ L * a) ∧ (∀ (i : Fin n), 0 < xstar i → gbar i + sstar i = c) ∧ ∀ (i : Fin n), c ≤ gbar i + sstar i

Build a dual maximizer with coefficients constant on the simplex support.

theorem simplex_linear_min_support_constant (n : ℕ) {xstar r : Fin n → ℝ} {c : ℝ} (hxstar : xstar ∈ standardSimplex n) (hconst : ∀ (i : Fin n), 0 < xstar i → r i = c) (hbound : ∀ (i : Fin n), c ≤ r i) (x : Fin n → ℝ) : x ∈ standardSimplex n → ∑ i : Fin n, r i * xstar i ≤ ∑ i : Fin n, r i * x i

If the linear coefficients are constant on the support and bounded below, the support minimizes.

theorem simplexProximalValue_saddlePoint_fin_hsmin (n : ℕ) (xbar xstar r : Fin n → ℝ) {c : ℝ} (hxstar : xstar ∈ standardSimplex n) (hconst : ∀ (i : Fin n), 0 < xstar i → r i = c) (hbound : ∀ (i : Fin n), c ≤ r i) (x : Fin n → ℝ) : x ∈ standardSimplex n → ∑ i : Fin n, r i * (xstar i - xbar i) ≤ ∑ i : Fin n, r i * (x i - xbar i)

Reduce the simplex best-response to a linear minimization over the support.

theorem simplexProximalValue_saddlePoint_fin (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hL : 0 < L) (hn : 0 < n) : ∃ 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

Existence of a saddle point for the finite simplex payoff.

theorem simplexProximalValue_minmax_exchange_fin (n : ℕ) (xbar gbar : Fin n → ℝ) (L : ℝ) (hL : 0 < 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) = 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)

Swap the min and max in the simplex proximal value (minimax step).