Proof mining in L^p spaces

2016/09/07 by Andrei Sipoş, Sipos, Andrei
Computer Science · Mathematics · #03F10 #46B25 #46E30 #Advanced Algebra and Logic #Advanced Topology and Set Theory #FOS: Mathematics #Functional Analysis (math.FA) #Logic (math.LO) #Logic, Reasoning, and Knowledge

paper · pdf · doi:10.48550/arxiv.1609.02080

openalex publication_date 2016/09/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We obtain an equivalent implicit characterization of L^p Banach spaces that is amenable to a logical treatment. Using that, we obtain an axiomatization for such spaces into a higher-order logical system, the kind of which is used in proof mining, a research program that aims to obtain the hidden computational content of mathematical proofs using tools from mathematical logic. As an aside, we obtain a concrete way of formalizing L^p spaces in positive-bounded logic. The axiomatization is followed by a corresponding metatheorem in the style of proof mining. We illustrate its use with the derivation for this class of spaces of the standard modulus of uniform convexity.

Related

• Proof mining and probability theory
• On the removal of weak compactness arguments in proof mining
• Logical metatheorems for accretive and (generalized) monotone set-valued operators
• Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory
• An application of proof mining to the proximal point algorithm in CAT(0) spaces