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. (Lean)

Manuscript

The cotype–cotype conjecture under the approximation property

September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:The-cotype-cotype-conjecture-under-the-approximation-property-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.

Result 326 · Functional analysis. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.