Proof theory and non-smooth analysis

We develop a general proof-theoretic framework for various classes of set-valued operators, including maximally as well as cyclically monotone and rectangular operators and we discuss a treatment for sums of set-valued operators A, B in that context such that all of the previous fits into logical metatheorems on bound extractions. In particular, we introduce quantitative forms for A being (weakly) uniformly rectangular with witnessing moduli. Based on this, we give quantitative forms of the Brezis–Haraux theorem that use such moduli as input. It turns out that a modulus for weak uniform rectangularity, which can be extracted even from non-effective proofs of rectangularity, is sufficient while the bound gets simpler in the case of a modulus for A being uniform rectangular which can be extracted from semi-constructive proofs. We use our results to explain recent proof minings in the context of Bauschke’s solution to the zero displacement conjecture and its extensions to other classes of functions than metric projections as instances of logical metatheorems. This article is part of the theme issue ‘Modern perspectives in Proof Theory’.