Recursive Inequalities in Applied Proof Theory

在数学中，有许多陈述为特定的性质提供了给定的条件。对于某些性质，有一个定量的类似物，例如“收敛”的概念和相关的“收敛速度”作为其定量的类似物。我们经常可以从一个提供了收敛假设的陈述及其证明中提取收敛速度。这里使用的关键工具通常是一个引理，它明确地陈述了更一般、更抽象的设置的收敛速度。因此，我们采取这个收敛的声明，然后操纵它，通常通过削弱起始假设和使用一些“基本”定理和引理，这样当应用关键工具时，我们的起始假设会返回一个显式的收敛率。有了这些明确的收敛速度，我们可以将其应用于具有某种递归不等式的算法，从而让我们了解它收敛到所需解的速度。使用上面概述的过程，我将在数学的其他领域探索这个想法，例如寻找和考虑一类尚未在这个角度分析的收敛语句。通过这个应用证明理论中的递归不等式的探索，我可能会发现新的相关数学结果，并发现新的链接到不相关的主题沿着。这个项目的另一个方面是这些语句的形式化。通过这一点，我们可能能够发现如何提取定量属性的模式。在操作语句的过程中，类似的论点被反复使用，因此有可能创建一个库来自动化该过程，从而为数学家提供一个程序来“量化”他们的结果。至于方法，我将主要研究学术文献，以调查应用证明论中的递归不等式。在形式化方面，我将使用精益证明助手作为编程语言来实现这一点。

In mathematics, there are many statements which provide given conditions for a particular property. With some properties, there is a quantitative analogue, take for instance the idea of 'convergence' and the associated 'rate of convergence' as its quantitative analogue. We can often take a statement which provides a hypothesis for convergence and extract from the statement and its proof, the rate of convergence. The key tool used here is often a lemma that states explicitly the rate of convergence of a more general, abstract setting. Hence, we take this convergent statement and then manipulate it, commonly by weakening the starting hypothesis and using some 'elementary' theorems and lemmas, such that when applying the key tool, an explicit rate of convergence is returned for our starting hypothesis. With these explicit rates of convergence, we can potentially apply this to algorithms featuring some kind of recursive inequality, thus giving us an idea of how fast it converges to the desired solution. Working with the procedure outlined above, I'll explore this idea in other areas of mathematics, for instance finding and considering a class of convergence statements that hasn't yet been analysed in this perspective. Through this exploration of recursive inequalities in applied proof theory, I may possibly uncover new related mathematical results and discover new links to unseemly unrelated topics along the way.Another aspect of this project is the formalisation of these statements. Through this, we may be able to discover patterns in how quantitative properties are extracted. During the manipulation of the statements, similar arguments are repeatedly used so there may be the possibility of creating a library to automate the procedure, and thus providing a program for mathematicians to 'quantify' their results.As for the methodology, I will primarily study the academic literature to investigate recursive inequalities in applied proof theory. With the formalisation aspects, I will use the Lean proof assistant as the programming language to implement this.