# The cotype–cotype conjecture under the approximation property

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

- [The cotype–cotype conjecture under the approximation property](../../preprints/The-cotype-cotype-conjecture-under-the-approximation-property-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/Cotype.lean) |