$L^p$空间中的证明挖掘
Proof mining in $L^p$ spaces
摘要：
我们得到了一个等价的隐含特征的$L^p$巴拿赫空间，是服从逻辑处理。利用这一点，我们获得了一个公理化这样的空间到一个高阶逻辑系统，这是用于证明挖掘，一个研究计划，旨在获得隐藏的计算内容的数学证明使用工具从数理逻辑。另外，我们得到了一个形式化$L^p$空间在正有界逻辑中的具体方法。公理化之后是一个相应的元定理的风格证明挖掘。我们说明了它的使用与推导这类空间的标准模的一致凸性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
