# Markov type characterizes superreflexivity

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

- [Nontrivial Markov Type Forces Superreflexivity](../../preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf)

## Scope

The formalized result proves that a real Banach space has nontrivial Markov type exactly when it admits an equivalent uniformly convex norm, hence exactly when it is superreflexive. Nontrivial Markov type means a uniform Markov-type bound for some exponent $p>1$ over all finite stationary reversible chains and all positive times. The exponent and equivalent norm may depend on the space, and the zero space is included. Additional formalized consequences concern uniformly smooth renormings and reflexivity of finitely representable spaces.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Nontrivial Markov type and superreflexivity | [MarkovType.lean](../ComparatorChallenges/MarkovType.lean) |