The cotype–cotype conjecture under the approximation property

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

The cotype–cotype conjecture under the approximation property

OpenAI · September 23, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

The cotype–cotype conjecture under the approximation property

Scope

The cotype–cotype problem asks whether finite cotype of a Banach space and its dual characterizes \(K\)-convexity. The formalized result establishes this equivalence for every nonzero real Banach space with the approximation property: \(X\) is \(K\)-convex exactly when both \(X\) and \(X^*\) have finite cotype.

Comparator links

Result	Comparator statement
Cotype–cotype equivalence with approximation property	Cotype.lean

Scope note on GitHub →