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.