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.