A proof-theoretic metatheorem for nonlinear semigroups generated by an accretive operator and applications

TL;DR

This paper develops a logical framework to extract quantitative information from proofs involving nonlinear semigroups generated by accretive operators, with applications to differential equations and convergence rates.

Contribution

It establishes new proof-theoretic metatheorems for nonlinear semigroups, enabling the extraction of explicit bounds from classical proofs in this area.

Findings

Derived polynomial rates of convergence for semigroup limits

Applied the metatheorems to classical results by Reich and Plant

Provided a logical foundation for proof mining in nonlinear analysis

Abstract

We further develop the theoretical framework of proof mining, a program in mathematical logic that seeks to quantify and extract computational information from prima facie `non-computational' proofs from the mainstream mathematical literature. To that end, we establish logical metatheorems that allow for the treatment of proofs involving nonlinear semigroups generated by an accretive operator, structures which in particular arise in the study of the solutions and asymptotic behavior of differential equations. In that way, the here established metatheorems facilitate a theoretical basis for the application of methods from the proof mining program to the wide variety of mathematical results established in the context of that theory since the 1970's. We in particular illustrate the applicability of the new systems and their metatheorems introduced here by providing two case studies on two central results due to Reich and Plant, respectively, on the asymptotic behavior of said semigroups and the resolvents of their generators where we derive rates of convergence for the limits involved which are, moreover, polynomial in all data.