Prove2Me

OAI.MarkovSuperreflexivity.FiniteTriangularObstruction.sequenceL2: intermediate lemma from OpenAI, Nontrivial Markov Type Forces Superreflexivity

Proved
OAI.MarkovSuperreflexivity.FiniteTriangularObstruction.sequenceL2

by dbenbenn · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Nontrivial Markov Type Forces Superreflexivity, OpenAI Math Release, September 23, 2026, result family 327, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.MarkovSuperreflexivity.FiniteTriangularObstruction.sequenceL2 of lean/OAI/Analysis/MarkovType/MarkovType/StructuralL2Estimates.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.MarkovSuperreflexivity):

theorem FiniteTriangularObstruction.sequenceL2
    (h : FiniteTriangularObstruction X) :
    FiniteTriangularObstruction (SequenceL2 X)

Definitions. The statement is written with OAI.MarkovSuperreflexivity.FiniteTriangularObstruction, OAI.MarkovSuperreflexivity.SequenceL2 and OAI.MarkovSuperreflexivity.sequenceL2ExponentAtLeastOne (definitions bundle OAISMk000 of this split).

Used by. The proofs of OAI.MarkovSuperreflexivity.exists_power_smooth_equivalentNorm and OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteTriangularObstruction of this split import it.

Preamble
import Mathlib
import Lean.Elab.Tactic.Omega
import Definitions.Def_OAISMk000
Formal statement
section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

namespace MarkovSuperreflexivity

universe u
variable {X : Type u} [NormedAddCommGroup X] [NormedSpace ℝ X]

theorem FiniteTriangularObstruction.sequenceL2
    (h : FiniteTriangularObstruction X) :
    FiniteTriangularObstruction (SequenceL2 X) := by
  sorry

end MarkovSuperreflexivity

end OAI
end
Source
OpenAI, Nontrivial Markov Type Forces Superreflexivity, OpenAI Math Release, September 23, 2026, https://github.com/openai/math (result family 327; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/MarkovType/MarkovType/StructuralL2Estimates.lean (declaration OAI.MarkovSuperreflexivity.FiniteTriangularObstruction.sequenceL2)

View graph