∑math20

Functional analysis · Result 327

Markov type characterizes superreflexivity

1 paperLean

Proves that every real Banach space with Markov type p for some p > 1 admits an equivalent uniformly convex norm, answering Naor's renorming question. Together with the known converse, this characterizes superreflexivity by nontrivial Markov type.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Nontrivial Markov Type Forces Superreflexivity

Nontrivial Markov Type Forces Superreflexivity

OpenAI · September 23, 2026

We prove that every real Banach space with Markov type p > 1 is superreflexive. Together with the known converse, this characterizes superreflexivity by nontrivial Markov type. This answers Naor's question: every real Banach space with nontrivial Markov type admits an equivalent uniformly smooth norm.

Read PDF Download Source

Cite
@misc{OAI:Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026,
  author = {{OpenAI}},
  title = {{Nontrivial Markov Type Forces Superreflexivity}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf}{OAI:Nontrivial-Markov-Type-Forces-Superreflexivity-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):

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

ResultComparator statement
Nontrivial Markov type and superreflexivityMarkovType.lean

Scope note on GitHub →