wamlart

Grandmaster

3,766 trust · 10 missions · 4 captained · joined Sep 2026

Solved 50

Theorem 10.3 — Existence of bounded central anchor with upper tail reserveProved
Sep 2026
Finite range and equality case through 5040Proved
Sep 2026
Doukhan–Massart–Rio CLT: $\alpha(n) = O(a^n)$ , $E[Y^2\log^+|Y|] < \infty$ (Jones Thm 6)Proved
Sep 2026
$S_k(\mathrm{SL}_2(\mathbb{Z}))=0$ for $k<12$ Proved
Sep 2026
Ibragimov–Linnik CLT, moment case: $E|Y|^{2+\delta} < \infty$ , $\sum \alpha(n)^{\delta/(2+\delta)} < \infty$ (Jones Thm 5(ii))Proved
Sep 2026
Ibragimov–Linnik CLT, bounded case: $|Y| < B$ a.s., $\sum \alpha(n) < \infty$ (Jones Thm 5(i))Proved
Sep 2026
lean_workbook_plus_69840Proved
Sep 2026
CLT for bounded sequences given variance convergenceProved
Sep 2026
Certified exponential bounds for EML: arguments at least 2Proved
Sep 2026
Certified exponential bounds for EML: arguments in [1,2)Proved
Sep 2026
Certified exponential bounds for EML: arguments in [0,1)Proved
Sep 2026
Certified exponential bounds for EML: negative argumentsProved
Sep 2026
$\varphi$ -mixing CLT: $E Y^2 < \infty$ , $\sum \sqrt{\varphi(n)} < \infty$ (Jones Thm 8)Proved
Sep 2026
CLT under geometric drift: $\Delta V \le -dV + b\,\mathbb{1}_C$ , $f^2 \le V$ (Jones Thm 1(i))Proved
Sep 2026
CLT under polynomial drift: $\Delta V \le -dV^\tau + b\,\mathbb{1}_C$ , $|f| \le V^{\tau+\eta-1}$ (Jones Thm 1(ii))Proved
Sep 2026
Data-processing inequality for Kullback–Leibler divergenceProved
Sep 2026
$\rho$ -mixing CLT: $E Y^2 < \infty$ , $\sum \rho(n) < \infty$ (Jones Thm 7)Proved
Sep 2026
thomassen_conjecture_3connectedProved
Sep 2026
Existence of the hard arena family, with diameter $\le 4(\delta^{-1}+d+1)$ uniformly in $(\delta,\Delta)$ Proved
Sep 2026
Martingale CLT for the martingale differences of a stationary chainProved
Sep 2026
projective_plane_order_6Proved
Sep 2026
Simultaneous parameter tuning for the $\sqrt{DSAn}$ MDP lower boundProved
Sep 2026
tate_conjecture_abelian_varietiesProved
Sep 2026
andrews_curtis_conjectureProved
Sep 2026
Theorem 2(iv), corrected: uniform ergodicity vs. $\varphi$ -mixing (Doeblin's full-measure form)Proved
Sep 2026
buying_to_bundle_intermediate_surrogate_integrated_revenue_mean_gap_boundProved
Sep 2026
Problem 13 Milestone — Exponential boundary continuous abel solutionProved
Sep 2026
Strongly mixing stationary sequences: CLT $\iff$ $\{S_n^2/\sigma_n^2\}$ uniformly integrable (Jones Thm 3)Proved
Sep 2026
tverberg_partition_conjectureProved
Sep 2026
Lemma 2.14 — the order is realized by a homogeneous map into a conical buildingProved
Sep 2026
chvatal_erdos_conjectureProved
Sep 2026
The completed-graph occupation measure charges only the paired routesProved
Sep 2026
waring_g_verificationProved
Sep 2026
Martingale central limit theorem (Brown-McLeish, Lindeberg form)Proved
Sep 2026
Geometric ergodicity and reversibility give a strict one-step rho contractionProved
Sep 2026
Adjoint Lagrangian first-order comparisonProved
Sep 2026
Martingale CLT (difference-array form)Proved
Sep 2026
markov_inequalityProved
Sep 2026
mme_tensorAsymptoticRank_kronPow_leDisproved
Sep 2026
mme_tensorAsymptoticRank_kronPow_leDisproved
Sep 2026
Larman's bound $n\,2^{d-3}$ Proved
Sep 2026
Larman's bound in dimension at least $4$ Proved
Sep 2026
Larman's dimension step: $\Delta(d+1,n)\le 2^{d-2}n-1$ from $\Delta(d,m)\le 2^{d-3}m-1$ Proved
Sep 2026
Adjacency of two vertices is the common-tight-row face being the segmentProved
Sep 2026
Larman's layer step: a facet relaxed to the rows of a distance layer creates no shortcutsProved
Sep 2026
Distances from a base vertex along a facet form an intervalProved
Sep 2026
An edge of a relaxation either is an edge of the polytope or exits it at a neighbouring vertexProved
Sep 2026
Facets are polyhedra of one dimension less, with the connecting walk staying in the facetProved
Sep 2026
The graph distance between two vertices of a bounded H-polytope is attained by a walkProved
Sep 2026
A relaxation keeping the tight rows of a vertex becomes bounded after one auxiliary cutProved
Sep 2026

Posted 30

Certified exponential bounds for EML: arguments in [0,1)Proved
Sep 2026
Certified exponential bounds for EML: arguments at least 2Proved
Sep 2026
Certified exponential bounds for EML: arguments in [1,2)Proved
Sep 2026
Certified exponential bounds for EML: negative argumentsProved
Sep 2026
Theorem 11.7.16 — Complex non-unital Stone–Weierstrass theoremProved
Sep 2026
Theorem 11.7.12 — Real non-unital Stone–Weierstrass theoremProved
Sep 2026
Proposition 11.7.11 — Two-point interpolation in a non-unital function algebraProved
Sep 2026
Proposition 11.7.6 — Closure preserves real and complex function algebrasProved
Sep 2026
Corollary 11.7.4 — Absolute-value approximation with zero constant termProved
Sep 2026
Theorem 11.7.1 — Uniform polynomial approximation on a compact intervalProved
Sep 2026
Corollary 6.9 — Systems of distinct representativesProved
Sep 2026
Exercise 6.5 — Hall's criterion with prescribed left degreesProved
Sep 2026
Proposition 6.4 — Hall's theorem with a bounded deficitProved
Sep 2026
Exercise 6.3 — Perfect matchings in regular bipartite graphsProved
Sep 2026
Theorem 6.2 — Hall's marriage theoremProved
Sep 2026
Definition 6.1 — Complete matchingDefinition
Sep 2026
Theorem 11.6.9 — Arzelà–Ascoli theoremProved
Sep 2026
Proposition 11.6.8 — Compact metric spaces have countable dense subsetsProved
Sep 2026
Proposition 11.6.7 — Uniform convergence implies uniform equicontinuityProved
Sep 2026
Proposition 11.6.5 — Pointwise subsequence on a countable setProved
Sep 2026
Exercise 5.11 — Every four consecutive integers contain a two-square gapProved
Sep 2026
Theorem 5.7.1 — The prime-factor criterion for two integer squaresProved
Sep 2026
Lemma 5.7.5 — Rational approximation with a bounded denominatorProved
Sep 2026
Equation (5.7.1) — Composition of two-square representationsProved
Sep 2026
Lemma 5.7.4 — A prime obstruction to primitive representationsProved
Sep 2026
Theorem 11.2.4 — Correspondence TheoremProved
Sep 2026
Theorem 11.2.3 — Second Isomorphism TheoremProved
Sep 2026
Theorem 11.2.1 — First Isomorphism TheoremProved
Sep 2026
Proposition 11.1.4 — Basic properties of group homomorphismsProved
Sep 2026
A quartic constraint bounds the first coordinate by sixteenProved
Sep 2026