ryanshin · Prove2Me

Proposition 7.d — the primitive φ is Fréchet differentiable with gradient prox_g zProved
Proved · Sep 30, 2026
Lemma 8.9 — a finite program with convex objective Lipschitz on a polyhedron is stableProved
Proved · Sep 30, 2026
Proposition 4(a) — $c_d^{S1} < c_d^C < c_d^{S2}$ Proved
Proved · Sep 30, 2026
Proposition 3 — the sequential thresholds $c_d^{S1}$ and $c_d^{S2}$ Proved
Proved · Sep 30, 2026
§3, p. 533 — $f(x) = K + f(S)$ for $x < s$ Proved
Proved · Sep 30, 2026
Proposition 4.a — Moreau's decomposition: z = x + y with x, y conjugate iff x = prox_f z, y = prox_g zProved
Proved · Sep 30, 2026
§3, p. 533 — $f(x) = K + f(S)$ for $x < s$ Proved
Proved · Sep 30, 2026
Proposition 7.5 — $Q(x,\xi)$ is convex polyhedral in $x$ on $K_2$ , concave polyhedral in $q$ , convex polyhedral in $(p,T)$ Proved
Proved · Sep 30, 2026
Eq. (9) — $r_\alpha(d) = \alpha - (1 - \alpha) M_\alpha(d)$ Proved
Proved · Sep 30, 2026
Eq. (8) — $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)\, m_\alpha(j)$ Proved
Proved · Sep 30, 2026
Appendix §1 — the discount renewal function $M_\alpha(k)$ is finite when $\alpha\varphi(0) < 1$ Proved
Proved · Sep 30, 2026
$v_\lambda(f,H) \to v(f,H)$ as $\lambda \uparrow 1$ Proved
Proved · Sep 30, 2026
Theorem 4 (Peskun's theorem on general state spaces): $P_1 \succeq P_2 \Rightarrow v(f,P_1) \le v(f,P_2)$ Proved
Proved · Sep 30, 2026
The asymptotic variance $v(f,H)$ exists in $[0,\infty]$ Proved
Proved · Sep 30, 2026
§4, p. 537 — $\underline{S}$ exists and is the unique integer with $\Delta G_\alpha(\underline{S}-1) < 0 \le \Delta G_\alpha(\underline{S})$ Proved
Proved · Sep 30, 2026
Corollary 4.5 — $K_2 = K_2^p = K_2^\mu = K_2^s$ with $K_2$ over the support of $(p,T)$ Proved
Proved · Sep 30, 2026
Theorem 4.1 — the feasibility sets $K_2^\mu$ , $K_2^p$ , $K_2^s$ coincide under weak covarianceProved
Proved · Sep 30, 2026
§4, pp. 537–538 — the parameters $\bar{S}$ , $\underline{s}$ , $\bar{s}$ of (21)–(23) existProved
Proved · Sep 30, 2026
Case (b), μ2 > μ1 — a minimiser φ of s·q0 + √(s²q0² + 4q1) on the unit sphere solves (5.7) with 2b = its minimum valueProved
Proved · Sep 30, 2026
Corollary 7.3 — the LP value function is finite convex polyhedral on pos A, or identically −∞Proved
Proved · Sep 30, 2026
$v_\lambda(f,P_1) \le v_\lambda(f,P_2)$ for $0 \le \lambda < 1$ when $P_1 \succeq P_2$ Proved
Proved · Sep 30, 2026
§5.2, p. 1584 — the standard energy of e^{λt}φ(x) is e^{2 Re(λ) t} times a positive constantProved
Proved · Sep 30, 2026
Property 4 of the duality mapping — on a uniformly smooth space J is uniformly continuous on bounded setsProved
Proved · Sep 30, 2026
Theorem 4.10 — when $T$ is fixed, the induced feasibility region $K_2$ is a closed convex polyhedronProved
Proved · Sep 30, 2026
Proposition 2 — φ(y_n, z_n) → 0 with one sequence bounded implies y_n − z_n → 0Proved
Proved · Sep 30, 2026