queelius · Prove2Me

Lemma 3.3 — a chain of prediction-based evictions has length at most $1 + S_\ell(\eta_{r,c})$ Proved
Proved · Oct 24, 2026
Proof of Thm 31 (p. 37) — margin tail: w.p. ≥ (1 − γ)/2, ⟨w, yx⟩ ≤ (a_n/γ)‖w‖₁Proved
Proved · Oct 24, 2026
Lemma 3: shifting to an initial family keeps the size and does not increase $\nu$ Proved
Proved · Oct 24, 2026
Proof of Thm 31 (p. 36) — w.p. 1 − γ/2, |E[θ⋆ᵢ|S]| ≤ 15τ√(2n log(4d/γ)) for all iProved
Proved · Oct 24, 2026
Lemma 29 — with prob. 1 − δ, |log posterior odds| ≤ 15τ√(2n log(2/δ))Proved
Proved · Oct 24, 2026
Correctness of Condat's Proposed Algorithm (Fig. 2): the output is $P_\Delta(y)$ and $K$ counts its nonzerosProved
Proved · Oct 24, 2026
Theorem 11: polynomial generalization bounds from hypothesis stabilityProved
Proved · Oct 24, 2026
Claim 1 — the optimal algorithm suffers at least $Q/2$ cache missesProved
Proved · Oct 24, 2026
Sect. 2 (p. 5) — $\tau$ is the root of $f(\rho)=\sum_n \max\{y_n-\rho,0\}-a$ ; sign test and bracketProved
Proved · Oct 24, 2026
Proof of Theorem 11: $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le M^2/(2m) + 3M\beta_1$ Proved
Proved · Oct 24, 2026
Lemma 9, eq. (9): $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le M^2/(2m) + 3M\,\mathbb E_{S,z}|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|$ Proved
Proved · Oct 24, 2026
Proof of Theorem 3, case λ*t > n — J^FP(n,t) ≥ np⁰(1 − 1/(2√n)) = r⁰t(1 − 1/(2√n))Proved
Proved · Oct 24, 2026
Eq. (19) — case λ*t ≤ n: J^FP(n,t) ≥ p*(λ*t − (√(λ*t + (n − λ*t)²) − (n − λ*t))/2) ≥ r*t(1 − 1/(2√(λ*t)))Proved
Proved · Oct 24, 2026
Theorem 2 — the deterministic revenue bounds the optimal expected revenue: J*(n,t) ≤ J^D(n,t)Proved
Proved · Oct 24, 2026
Proposition 2.2 — the simplex projection is a thresholdingProved
Proved · Oct 24, 2026
The projections onto the simplex and the $\ell_1$ ball exist and are uniqueProved
Proved · Oct 24, 2026
Proof of Theorem 11: $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le M^2/(2m) + 3M(\beta_1+\beta_2)$ Proved
Proved · Oct 24, 2026
Lemma 9, eq. (8): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le M^2/(2m) + 3M\,\mathbb E_{S,z_i'}|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|$ Proved
Proved · Oct 24, 2026
Eq. (15) — the augmented functional J_u(n,t,μ) dominates J_u(n,t) for μ ≥ 0Proved
Proved · Oct 24, 2026
Eqs. (13)–(14) — E_u[N_t] = E_u[∫λ_s ds] ≤ n and J_u(n,t) = E_u[∫r(λ_s) ds] for every policyProved
Proved · Oct 24, 2026
Theorem 5.6: a common one-step return probability reduces average cost to discountingProved
Proved · Oct 24, 2026
Theorem 5.1: an average cost equation solution verifies optimalityProved
Proved · Oct 23, 2026
Proof of Theorem 11: the replace-one term is at most $\beta_1 + \beta_2$ Proved
Proved · Oct 23, 2026
The transformed discounted value solves the original average cost equationProved
Proved · Oct 23, 2026
Lemma 25 (leave-one-out error): second-moment expansion of $R - R_{\mathrm{loo}}$ Proved
Proved · Oct 23, 2026