Browse › Functional analysis › 326 The cotype–cotype conjecture under the approximation property
The cotype–cotype conjecture under the approximation property
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove the cotype–cotype conjecture under the ordinary approximation property. A nonzero real Banach space with this property is K-convex if and only if both the space and its dual have finite Rademacher cotype, possibly with different exponents.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, The cotype–cotype conjecture under the approximation property — Lean scope note (lean/docs/326.md, 2026-10-06). The release's scope note says the formalized result is the equivalence of K-convexity with finite cotype of $X$ and $X^*$ for nonzero real Banach spaces with AP, and links the comparator statement
Cotype.lean. [family-level] - anxkhn, Add the cotype–cotype characterization under the approximation property (google-deepmind/formal-conjectures issue #7148, opened 2026-10-11). An open issue proposing to add Theorem 1.1 to formal-conjectures, with ordinary AP modelled without a common norm bound on the approximants.
- anxkhn, feat(Paper): add the cotype–cotype theorem under AP (google-deepmind/formal-conjectures PR #7153, opened 2026-10-11, open). It adds a Lean statement of Theorem 1.1 and finite-cube
RademacherCotypedefinitions without aformal_proofattribute; a review comment by bocowgill (2026-10-12) says the statement matches Theorem 1.1 and asks for proof-certification evidence before marking it solved.
Possibly relevant literature (found by the agent, not checked)
- S. Artstein, V. Milman, S. J. Szarek, Duality of metric entropy (arXiv:math/0407236; Ann. of Math. 159 (2004), 1313–1328). Proves dimension-free entropy duality when one of the spaces is Hilbertian; it is the predecessor of the K-convex case [AMSTJ2004] used for the entropy-duality part of Corollary 1.2.
- A. Hinrichs, Hilbert space factorization and Fourier type of operators (Studia Math. 145 (2001), 199–212, doi:10.4064/sm145-3-2). Compares Hilbert-space factorization norms with Fourier-type norms of operators, including a Walsh-function analogue, which may relate to the paper's step bounding the Walsh transform of a finite-rank operator via Hilbert-space factorization.
Digests and expositions
- Latent Seminar, Cotype, duality, and the approximation property (2026-10-06). An exposition outlining the manuscript's moment lifts, uniform Walsh decay, compact-domain use of ordinary AP, and restricted entropy-duality consequence; it states that it does not independently verify the complete proofs. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 326
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-cotype-cotype-conjecture-under-the-approximation-property-September-23-2026,
author = {{OpenAI}},
title = {{The cotype--cotype conjecture under the approximation property}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-cotype-cotype-conjecture-under-the-approximation-property-September-23-2026/paper.pdf}{OAI:The-cotype-cotype-conjecture-under-the-approximation-property-September-23-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/326.md. The Lean statements have not been checked by people against the paper's claims.
Family 326: The cotype–cotype conjecture under the approximation property
Resolves the cotype–cotype conjecture for real Banach spaces with the approximation property. Such a nonzero space is K-convex if and only if both it and its dual have finite Rademacher cotype, with possibly different exponents. Equivalently, these cotype assumptions force nontrivial Rademacher type.
This is the only paper in this family.