We shall use proof mining techniques in order to obtain finitary versions with effective bounds of some important results in metric analysis, geometric group theory and ergodic theory.
Proof mining is a paradigm of research concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of highly infinitary principles.
This new information is obtained after a logical analysis of the original mathematical proof,
using proof-theoretic techniques called proof interpretations.
In this way one obtains highly uniform effective bounds for results that are more general
than the initial ones. While the methods used to obtain these new results come from mathematical
logic, their proofs can be written in ordinary mathematics.
This research direction can be related to Terence Tao's proposal of "hard analysis", based on finitary arguments, instead of the infinitary ones from "soft analysis".
We want to obtain new results in metric analysis, ergodic theory and geometric group theory by applying proof mining methods