Logical Extraction of Effective Bounds in
Nonlinear Analysis
Metastability and Abstract Cauchy Problems

Ulrich Kohlenbach
Department of Mathematics
Technische Universität Darmstadt
Kickoff Meeting JSPS-DFG Graduate School
Mathematical Fluid Dynamics
Waseda University
June 17-18, 2014
Logical Extraction of Bounds

Proof Theory and Consistency Proofs

Proof Theory started with D. Hilbert’s program to prove theconsistency of mathematics by finitistic means.

Logical Extraction of Bounds

Proof Theory and Consistency Proofs

Proof Theory started with D. Hilbert’s program to prove theconsistency of mathematics by finitistic means.
Not possible in the strict sense due to Gödel’s 2nd incompletenesstheorem.

Logical Extraction of Bounds

Proof Theory and Consistency Proofs

Proof Theory started with D. Hilbert’s program to prove theconsistency of mathematics by finitistic means.
Not possible in the strict sense due to Gödel’s 2nd incompletenesstheorem.
Program is still alive: partial realizations possible, relative
consistency proofs.

Logical Extraction of Bounds

Proof Theory and Consistency Proofs

Proof Theory started with D. Hilbert’s program to prove theconsistency of mathematics by finitistic means.
Not possible in the strict sense due to Gödel’s 2nd incompletenesstheorem.
Program is still alive: partial realizations possible, relative
consistency proofs.
Important tools (so-called proof interpretation) where developed inthis program which are now used in mathematical practice.

Logical Extraction of Bounds

Proof Theory and Consistency Proofs

Proof Theory started with D. Hilbert’s program to prove theconsistency of mathematics by finitistic means.
Not possible in the strict sense due to Gödel’s 2nd incompletenesstheorem.
Program is still alive: partial realizations possible, relative
consistency proofs.
Important tools (so-called proof interpretation) where developed inthis program which are now used in mathematical practice.
G. Kreisel (since 50’s): use proof interpretations to extract new
information from (prima facie noneffective) proofs.

Logical Extraction of Bounds

Extractive Proof Theory: Proof Interpretations

Let T1 and T2 be theories with languages L(T1 ) and L(T2 ).

Logical Extraction of Bounds

Extractive Proof Theory: Proof Interpretations

Let T1 and T2 be theories with languages L(T1 ) and L(T2 ).
Interpret propositions A from L(T1 ) (inductively over the logicalstructure of A) by propositions AI from L(T2 ).

Logical Extraction of Bounds

Extractive Proof Theory: Proof Interpretations

Let T1 and T2 be theories with languages L(T1 ) and L(T2 ).
Interpret propositions A from L(T1 ) (inductively over the logicalstructure of A) by propositions AI from L(T2 ).
Transform a proof p of A into a proof p I of AI (induction on p).

Logical Extraction of Bounds

Extractive Proof Theory: Proof Interpretations

Let T1 and T2 be theories with languages L(T1 ) and L(T2 ).
Interpret propositions A from L(T1 ) (inductively over the logicalstructure of A) by propositions AI from L(T2 ).
Transform a proof p of A into a proof p I of AI (induction on p).
AI contains the additional computational quantitative
information on A we are looking for such as effective bounds.

Logical Extraction of Bounds

Extractive Proof Theory: Proof Interpretations

Let T1 and T2 be theories with languages L(T1 ) and L(T2 ).
Interpret propositions A from L(T1 ) (inductively over the logicalstructure of A) by propositions AI from L(T2 ).
Transform a proof p of A into a proof p I of AI (induction on p).
AI contains the additional computational quantitative
information on A we are looking for such as effective bounds.
Central Method: Modern extensions of Gödel’s 1958 (developed as partof modified Hilbert program) Functional (‘Dialectica’) Interpretation!

Logical Extraction of Bounds

‘Proof Mining’ in core mathematics

During the last 20 years this proof-theoretic approach has resulted innumerous new quantitative results as well as qualitative
uniformity results e.g. in: nonlinear analysis, fixed point theory,
ergodic theory, topological dynamics, approximation theory etc.

Logical Extraction of Bounds

‘Proof Mining’ in core mathematics

During the last 20 years this proof-theoretic approach has resulted innumerous new quantitative results as well as qualitative
uniformity results e.g. in: nonlinear analysis, fixed point theory,
ergodic theory, topological dynamics, approximation theory etc.
General logical metatheorems explain this as instances of logicalphenomena (K. 2005, Gerhardy/K. 2008, TAMS).

Logical Extraction of Bounds

‘Proof Mining’ in core mathematics

During the last 20 years this proof-theoretic approach has resulted innumerous new quantitative results as well as qualitative
uniformity results e.g. in: nonlinear analysis, fixed point theory,
ergodic theory, topological dynamics, approximation theory etc.
General logical metatheorems explain this as instances of logicalphenomena (K. 2005, Gerhardy/K. 2008, TAMS).
Some of the logical tools used have recently been rediscovered in
special cases by Terence Tao prompted by concrete mathematicalneeds “finitary analysis”!

Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.

Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.
Goal: Effective bounds for∀x ∈ P ∀y ∈ K ∀z1 ∈ X ∀z2 ∈ XX ∀z3 ∈ XIN ∃n ∈ IN A(x, y, z, n)-theorems.

Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.
Goal: Effective bounds for∀x ∈ P ∀y ∈ K ∀z1 ∈ X ∀z2 ∈ XX ∀z3 ∈ XIN ∃n ∈ IN A(x, y, z, n)-theorems.
Restriction: Because of classical logic: in general A must be existential.

Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.
Goal: Effective bounds for∀x ∈ P ∀y ∈ K ∀z1 ∈ X ∀z2 ∈ XX ∀z3 ∈ XIN ∃n ∈ IN A(x, y, z, n)-theorems.
Restriction: Because of classical logic: in general A must be existential.
If only restricted use of ϕ ∨ ¬ϕ : arbitrary A.

Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.
Goal: Effective bounds for∀x ∈ P ∀y ∈ K ∀z1 ∈ X ∀z2 ∈ XX ∀z3 ∈ XIN ∃n ∈ IN A(x, y, z, n)-theorems.
Restriction: Because of classical logic: in general A must be existential.
If only restricted use of ϕ ∨ ¬ϕ : arbitrary A.
Then general logical metatheorems (K. Trans.AMS 2005) guarantee
the extractability of effective bounds ‘∃n ∈ Φ(x, b1 , b2 , b3 )’Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.
Goal: Effective bounds for∀x ∈ P ∀y ∈ K ∀z1 ∈ X ∀z2 ∈ XX ∀z3 ∈ XIN ∃n ∈ IN A(x, y, z, n)-theorems.
Restriction: Because of classical logic: in general A must be existential.
If only restricted use of ϕ ∨ ¬ϕ : arbitrary A.
Then general logical metatheorems (K. Trans.AMS 2005) guarantee
the extractability of effective bounds ‘∃n ∈ Φ(x, b1 , b2 , b3 )’ which are
independent from parameters y ∈ K (compactness necessary forseparable spaces);

Logical Extraction of Bounds

Setting: Let P, K be concrete Polish resp. compact Polish spaces and
X an abstract metric/normed space.
Goal: Effective bounds for∀x ∈ P ∀y ∈ K ∀z1 ∈ X ∀z2 ∈ XX ∀z3 ∈ XIN ∃n ∈ IN A(x, y, z, n)-theorems.
Restriction: Because of classical logic: in general A must be existential.
If only restricted use of ϕ ∨ ¬ϕ : arbitrary A.
Then general logical metatheorems (K. Trans.AMS 2005) guarantee
the extractability of effective bounds ‘∃n ∈ Φ(x, b1 , b2 , b3 )’ which are
independent from parameters y ∈ K (compactness necessary forseparable spaces);
independent from parameters z1 , z2 , z3 provided that appropriate
norm-bounds b1 , b2 , b3 on z1 , z2 , z3 are available.
Logical Extraction of Bounds

Abstract (nonseparable) structures
Examples of such spaces X : metric, hyperbolic, CAT(0), normed, theircompletions, Hilbert, uniformly convex, uniformly smooth, uniformly
nonsquare, abstract Lp and C (K ) spaces (Günzel/K.)... (not: separable,
strictly convex or smooth spaces).

Logical Extraction of Bounds

Abstract (nonseparable) structures
Examples of such spaces X : metric, hyperbolic, CAT(0), normed, theircompletions, Hilbert, uniformly convex, uniformly smooth, uniformly
nonsquare, abstract Lp and C (K ) spaces (Günzel/K.)... (not: separable,
strictly convex or smooth spaces).
Also several metric structures X1 , . . . , Xn simultaneously (Günzel/K.).

Logical Extraction of Bounds

Abstract (nonseparable) structures
Examples of such spaces X : metric, hyperbolic, CAT(0), normed, theircompletions, Hilbert, uniformly convex, uniformly smooth, uniformly
nonsquare, abstract Lp and C (K ) spaces (Günzel/K.)... (not: separable,
strictly convex or smooth spaces).
Also several metric structures X1 , . . . , Xn simultaneously (Günzel/K.).
For separable (Polish) structures (represented as continuous
image of ININ ), the compactness is necessary for the independence
from y ∈ K.

Logical Extraction of Bounds

Abstract (nonseparable) structures
Examples of such spaces X : metric, hyperbolic, CAT(0), normed, theircompletions, Hilbert, uniformly convex, uniformly smooth, uniformly
nonsquare, abstract Lp and C (K ) spaces (Günzel/K.)... (not: separable,
strictly convex or smooth spaces).
Also several metric structures X1 , . . . , Xn simultaneously (Günzel/K.).
For separable (Polish) structures (represented as continuous
image of ININ ), the compactness is necessary for the independence
from y ∈ K.
Theorems for abstract spaces X (not assumed to be separable!):uniform bounds depending only on norm bounds on the X -data.

Logical Extraction of Bounds

Abstract (nonseparable) structures
Examples of such spaces X : metric, hyperbolic, CAT(0), normed, theircompletions, Hilbert, uniformly convex, uniformly smooth, uniformly
nonsquare, abstract Lp and C (K ) spaces (Günzel/K.)... (not: separable,
strictly convex or smooth spaces).
Also several metric structures X1 , . . . , Xn simultaneously (Günzel/K.).
For separable (Polish) structures (represented as continuous
image of ININ ), the compactness is necessary for the independence
from y ∈ K.
Theorems for abstract spaces X (not assumed to be separable!):uniform bounds depending only on norm bounds on the X -data.
Crucially used for this that the proof treats X as abstract structurethat is not represented as separable space (via ININ ).
Logical Extraction of Bounds

Formal systems for analysis with abstract spaces X
Types: (i) IN, X are types, (ii) with ρ, τ also ρ → τ is a type.

Logical Extraction of Bounds

Formal systems for analysis with abstract spaces X
Types: (i) IN, X are types, (ii) with ρ, τ also ρ → τ is a type.
PAω,X is the extension of Peano Arithmetic to all types.
Aω,X :=PAω,X +DC, where
DC: axiom of dependent choice for all types
Implies full comprehension for numbers (higher order arithmetic).

Logical Extraction of Bounds

Formal systems for analysis with abstract spaces X
Types: (i) IN, X are types, (ii) with ρ, τ also ρ → τ is a type.
PAω,X is the extension of Peano Arithmetic to all types.
Aω,X :=PAω,X +DC, where
DC: axiom of dependent choice for all types
Implies full comprehension for numbers (higher order arithmetic).
Equality defined notion: xX =X yX :≡ dX (x, y) =IR 0IR .. In general
only rule
If s =X t has been proved, then f(s) =X f(t).

Logical Extraction of Bounds

Formal systems for analysis with abstract spaces X
Types: (i) IN, X are types, (ii) with ρ, τ also ρ → τ is a type.
PAω,X is the extension of Peano Arithmetic to all types.
Aω,X :=PAω,X +DC, where
DC: axiom of dependent choice for all types
Implies full comprehension for numbers (higher order arithmetic).
Equality defined notion: xX =X yX :≡ dX (x, y) =IR 0IR .. In general
only rule
If s =X t has been proved, then f(s) =X f(t).
Aω [X , k · k . . .] results by adding constants with axioms expressing e.g.
that (X , k · k, . . .) is a normmed, uniformly convex, Hilbert . . . space.
Logical Extraction of Bounds

Keeping track of uniform bounds: majorizationy , x functionals of types ρ, ρb := ρ[IN/X ] :xIN &IN yIN :≡ x ≥ y
xIN &X yX :≡ x ≥ kyk.

Logical Extraction of Bounds

Keeping track of uniform bounds: majorizationy , x functionals of types ρ, ρb := ρ[IN/X ] :xIN &IN yIN :≡ x ≥ y
xIN &X yX :≡ x ≥ kyk.
For complex types ρ → τ this is extended in a hereditary fashion.

Logical Extraction of Bounds

Keeping track of uniform bounds: majorizationy , x functionals of types ρ, ρb := ρ[IN/X ] :xIN &IN yIN :≡ x ≥ y
xIN &X yX :≡ x ≥ kyk.
For complex types ρ → τ this is extended in a hereditary fashion.
Example:f ∗ &X→X f ≡ ∀n ∈ IN, x ∈ X[n ≥ kxk → f ∗ (n) ≥ kf(x)k].

Logical Extraction of Bounds

Keeping track of uniform bounds: majorizationy , x functionals of types ρ, ρb := ρ[IN/X ] :xIN &IN yIN :≡ x ≥ y
xIN &X yX :≡ x ≥ kyk.
For complex types ρ → τ this is extended in a hereditary fashion.
Example:f ∗ &X→X f ≡ ∀n ∈ IN, x ∈ X[n ≥ kxk → f ∗ (n) ≥ kf(x)k].
If f : X → X is nonexpansive (n.e.), i.e. d(f(x), f(y)) ≤ d(x, y).

Logical Extraction of Bounds

Keeping track of uniform bounds: majorizationy , x functionals of types ρ, ρb := ρ[IN/X ] :xIN &IN yIN :≡ x ≥ y
xIN &X yX :≡ x ≥ kyk.
For complex types ρ → τ this is extended in a hereditary fashion.
Example:f ∗ &X→X f ≡ ∀n ∈ IN, x ∈ X[n ≥ kxk → f ∗ (n) ≥ kf(x)k].
If f : X → X is nonexpansive (n.e.), i.e. d(f(x), f(y)) ≤ d(x, y).
Then for kak, ka − f(a)k ≤ b and f ∗ (n) := n + 3b: f ∗ &X→X f.

Logical Extraction of Bounds

Theorem (K., Trans.AMS 2005, Gerhardy/K.,Trans.AMS 2008)
Let P, K be Polish resp. compact metric spaces, A∃ ∃-formula,z := z1 , . . . zk variables ranging over X , IN → X or X → X .

Logical Extraction of Bounds

Theorem (K., Trans.AMS 2005, Gerhardy/K.,Trans.AMS 2008)
Let P, K be Polish resp. compact metric spaces, A∃ ∃-formula,z := z1 , . . . zk variables ranging over X , IN → X or X → X .
If Aω [X , k · k] proves∀x ∈ P∀y ∈ K∀zτ ∃vIN A∃ (x, y, z, v),

Logical Extraction of Bounds

Theorem (K., Trans.AMS 2005, Gerhardy/K.,Trans.AMS 2008)
Let P, K be Polish resp. compact metric spaces, A∃ ∃-formula,z := z1 , . . . zk variables ranging over X , IN → X or X → X .
If Aω [X , k · k] proves∀x ∈ P∀y ∈ K∀zτ ∃vIN A∃ (x, y, z, v),
then one can extract a computable Φ : ININ × IN(IN) → IN s.t. thefollowing holds in every nontrivial normed space: for all representatives
rx ∈ ININ of x ∈ P and all z τ and z ∗ ∈ IN(IN) s.t. z ∗ &τ z:∀y ∈ K∃v ≤ Φ(rx , z∗ ) A∃ (x, y, z, v).

Logical Extraction of Bounds

Theorem (K., Trans.AMS 2005, Gerhardy/K.,Trans.AMS 2008)
Let P, K be Polish resp. compact metric spaces, A∃ ∃-formula,z := z1 , . . . zk variables ranging over X , IN → X or X → X .
If Aω [X , k · k] proves∀x ∈ P∀y ∈ K∀zτ ∃vIN A∃ (x, y, z, v),
then one can extract a computable Φ : ININ × IN(IN) → IN s.t. thefollowing holds in every nontrivial normed space: for all representatives
rx ∈ ININ of x ∈ P and all z τ and z ∗ ∈ IN(IN) s.t. z ∗ &τ z:∀y ∈ K∃v ≤ Φ(rx , z∗ ) A∃ (x, y, z, v).

Interesting connections to uniformity in ultraproducts (continuous
model theory; Keisler, Henson,. . .).
Logical Extraction of Bounds

The running theme: convergence statements in analysis

Let (xn ) be a Cauchy sequence in a metric space (X , ρ), i.e.
∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi , xj ) ≤ 2−k ) ∈ ∀∃∀Logical Extraction of Bounds

The running theme: convergence statements in analysis

Let (xn ) be a Cauchy sequence in a metric space (X , ρ), i.e.
∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi , xj ) ≤ 2−k ) ∈ ∀∃∀is noneffectively equivalent to its Gödel functional interpretation∀k ∈ IN ∀g ∈ ININ ∃n ∈ IN∀i, j ∈ [n; n+g(n)] (ρ(xi , xj ) < 2−k ) ∈ ∀∃Logical Extraction of Bounds

The running theme: convergence statements in analysis

Let (xn ) be a Cauchy sequence in a metric space (X , ρ), i.e.
∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi , xj ) ≤ 2−k ) ∈ ∀∃∀is noneffectively equivalent to its Gödel functional interpretation∀k ∈ IN ∀g ∈ ININ ∃n ∈ IN∀i, j ∈ [n; n+g(n)] (ρ(xi , xj ) < 2−k ) ∈ ∀∃Herbrand normal form or metastability (Tao).

Logical Extraction of Bounds

The running theme: convergence statements in analysis

Let (xn ) be a Cauchy sequence in a metric space (X , ρ), i.e.
∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi , xj ) ≤ 2−k ) ∈ ∀∃∀is noneffectively equivalent to its Gödel functional interpretation∀k ∈ IN ∀g ∈ ININ ∃n ∈ IN∀i, j ∈ [n; n+g(n)] (ρ(xi , xj ) < 2−k ) ∈ ∀∃Herbrand normal form or metastability (Tao).
A bound Φ(k, g ) on ‘∃n’ in the latter formula is a rate of metastability(introduced by Kreisel in 1951 as no-counterexample interpretation).

Logical Extraction of Bounds

Effective full rates of convergence?

Logical Extraction of Bounds

Effective full rates of convergence?
In general impossible: There exists a computable decreasing
sequence (an ) of rationals in [0, 1] (an ) with no computable rateof convergence (Specker 1949).

Logical Extraction of Bounds

Effective full rates of convergence?
In general impossible: There exists a computable decreasing
sequence (an ) of rationals in [0, 1] (an ) with no computable rateof convergence (Specker 1949).
Usually possible for asymptotic regularity results
ρ(xn , f(xn )) → 0,even when (xn ) may not converge to a fixed point of f .

Logical Extraction of Bounds

Effective full rates of convergence?
In general impossible: There exists a computable decreasing
sequence (an ) of rationals in [0, 1] (an ) with no computable rateof convergence (Specker 1949).
Usually possible for asymptotic regularity results
ρ(xn , f(xn )) → 0,even when (xn ) may not converge to a fixed point of f .
Possible for (xn ) if sequence converges to unique fixed
point/solution.

Logical Extraction of Bounds

Effective full rates of convergence?
In general impossible: There exists a computable decreasing
sequence (an ) of rationals in [0, 1] (an ) with no computable rateof convergence (Specker 1949).
Usually possible for asymptotic regularity results
ρ(xn , f(xn )) → 0,even when (xn ) may not converge to a fixed point of f .
Possible for (xn ) if sequence converges to unique fixed
point/solution.
Possible if proof is ‘semi-constructive’.

Logical Extraction of Bounds

Effective full rates of convergence?
In general impossible: There exists a computable decreasing
sequence (an ) of rationals in [0, 1] (an ) with no computable rateof convergence (Specker 1949).
Usually possible for asymptotic regularity results
ρ(xn , f(xn )) → 0,even when (xn ) may not converge to a fixed point of f .
Possible for (xn ) if sequence converges to unique fixed
point/solution.
Possible if proof is ‘semi-constructive’.
Effective and uniform rates metastability: always possible.

Logical Extraction of Bounds

Ineffective convergence proofs in fluid dynamics

Logical Extraction of Bounds

Ineffective convergence proofs in fluid dynamics
Specialized weak and strong compactness arguments are ubiquitousin fluid dynamics to establish weak or strong solutions of NSE;

Logical Extraction of Bounds

Ineffective convergence proofs in fluid dynamics
Specialized weak and strong compactness arguments are ubiquitousin fluid dynamics to establish weak or strong solutions of NSE;
E.g. Temam 1995 shows that a sequence (uk ) based on a suitable
space/time discretization schema for NSE is bounded and so has aweak in L2 (as well as weak-star in L∞ ) convergent subsequence;

Logical Extraction of Bounds

Ineffective convergence proofs in fluid dynamics
Specialized weak and strong compactness arguments are ubiquitousin fluid dynamics to establish weak or strong solutions of NSE;
E.g. Temam 1995 shows that a sequence (uk ) based on a suitable
space/time discretization schema for NSE is bounded and so has aweak in L2 (as well as weak-star in L∞ ) convergent subsequence;
Using a specialized Ascoli-type compactness argument, thesubsequence even converges strongly in L2 (and even in Lq for
1 ≤ q < ∞), needed for the passage to the limit in the nonlinear
term, and so converges towards a solution u of NSE;

Logical Extraction of Bounds

Ineffective convergence proofs in fluid dynamics
Specialized weak and strong compactness arguments are ubiquitousin fluid dynamics to establish weak or strong solutions of NSE;
E.g. Temam 1995 shows that a sequence (uk ) based on a suitable
space/time discretization schema for NSE is bounded and so has aweak in L2 (as well as weak-star in L∞ ) convergent subsequence;
Using a specialized Ascoli-type compactness argument, thesubsequence even converges strongly in L2 (and even in Lq for
1 ≤ q < ∞), needed for the passage to the limit in the nonlinear
term, and so converges towards a solution u of NSE;
By the uniqueness of u (in the situation at hand) already the entire
sequence (uk ) converges to u.

Logical Extraction of Bounds

Ineffective convergence proofs in fluid dynamics
Specialized weak and strong compactness arguments are ubiquitousin fluid dynamics to establish weak or strong solutions of NSE;
E.g. Temam 1995 shows that a sequence (uk ) based on a suitable
space/time discretization schema for NSE is bounded and so has aweak in L2 (as well as weak-star in L∞ ) convergent subsequence;
Using a specialized Ascoli-type compactness argument, thesubsequence even converges strongly in L2 (and even in Lq for
1 ≤ q < ∞), needed for the passage to the limit in the nonlinear
term, and so converges towards a solution u of NSE;
By the uniqueness of u (in the situation at hand) already the entire
sequence (uk ) converges to u.
Many noneffective convergence proofs exist in the context of theabstract nonlinear semigroup approach to abstract Cauchy problems(see below).
Logical Extraction of Bounds

Rates of Asymptotic
Regularity

Logical Extraction of BoundsAccretive operators (F.E. Browder, T. Kato)
X Banach space, C ⊂ X convex, f : C → C pseudocontraction if∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k .

Logical Extraction of BoundsAccretive operators (F.E. Browder, T. Kato)
X Banach space, C ⊂ X convex, f : C → C pseudocontraction if∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k .
f is a pseudocontraction iff A := Id − f is accretive (monotone), i.e∀u, v ∈ C∀s > 0 ku − vk ≤ ku − v + s(Au − Av)k, i.e.

Logical Extraction of BoundsAccretive operators (F.E. Browder, T. Kato)
X Banach space, C ⊂ X convex, f : C → C pseudocontraction if∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k .
f is a pseudocontraction iff A := Id − f is accretive (monotone), i.e∀u, v ∈ C∀s > 0 ku − vk ≤ ku − v + s(Au − Av)k, i.e.
∀u, v ∈ C (hAu − Av, u − vi ≥ 0) in Hilbert space.

Logical Extraction of BoundsAccretive operators (F.E. Browder, T. Kato)
X Banach space, C ⊂ X convex, f : C → C pseudocontraction if∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k .
f is a pseudocontraction iff A := Id − f is accretive (monotone), i.e∀u, v ∈ C∀s > 0 ku − vk ≤ ku − v + s(Au − Av)k, i.e.
∀u, v ∈ C (hAu − Av, u − vi ≥ 0) in Hilbert space.
Accretive (pseudocontractive, dissipative) operators are used (often
set-valued) in the nonlinear semigroup approach to PDE’s (Brezis,
Crandall, Liggett, Lions..., Barbu, Bothe).

Logical Extraction of BoundsAccretive operators (F.E. Browder, T. Kato)
X Banach space, C ⊂ X convex, f : C → C pseudocontraction if∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k .
f is a pseudocontraction iff A := Id − f is accretive (monotone), i.e∀u, v ∈ C∀s > 0 ku − vk ≤ ku − v + s(Au − Av)k, i.e.
∀u, v ∈ C (hAu − Av, u − vi ≥ 0) in Hilbert space.
Accretive (pseudocontractive, dissipative) operators are used (often
set-valued) in the nonlinear semigroup approach to PDE’s (Brezis,
Crandall, Liggett, Lions..., Barbu, Bothe).
See application further below!
Logical Extraction of Bounds

Connection to Fluid Dynamics
That y : [0, T ] → V 0 with V :=:= {y ∈ (H01 (Ω))N : ∇y = 0} is a weaksolution to the classical Navier-Stokes equations can be written asdydt(t) + v0 Ay(t) + By(t) = f(t), a.e. t ∈ (0, T),

Logical Extraction of Bounds

Connection to Fluid Dynamics
That y : [0, T ] → V 0 with V :=:= {y ∈ (H01 (Ω))N : ∇y = 0} is a weaksolution to the classical Navier-Stokes equations can be written asdydt(t) + v0 Ay(t) + By(t) = f(t), a.e. t ∈ (0, T),

where dy/dt is the strong derivative of y : [0, T] → V0 , A := −P∆,
B := P(y · ∇)y with the Helmholtz-Leray operator P.

Logical Extraction of Bounds

Connection to Fluid Dynamics
That y : [0, T ] → V 0 with V :=:= {y ∈ (H01 (Ω))N : ∇y = 0} is a weaksolution to the classical Navier-Stokes equations can be written asdydt(t) + v0 Ay(t) + By(t) = f(t), a.e. t ∈ (0, T),

where dy/dt is the strong derivative of y : [0, T] → V0 , A := −P∆,
B := P(y · ∇)y with the Helmholtz-Leray operator P.
Define for each M > 0(
BM y :=By,

if kyk ≤ M,

M2
By,
kyk2

if kyk > M.

Logical Extraction of Bounds

Connection to Fluid Dynamics
That y : [0, T ] → V 0 with V :=:= {y ∈ (H01 (Ω))N : ∇y = 0} is a weaksolution to the classical Navier-Stokes equations can be written asdydt(t) + v0 Ay(t) + By(t) = f(t), a.e. t ∈ (0, T),

where dy/dt is the strong derivative of y : [0, T] → V0 , A := −P∆,
B := P(y · ∇)y with the Helmholtz-Leray operator P.
Define for each M > 0(
BM y :=By,

if kyk ≤ M,

M2
By,
kyk2

if kyk > M.

Then for a suitable αM > 0 the operator v0 A + BM + αM · I is(m)-accretive (e.g. V. Barbu: Nonlinear Differential Equations of
Monotone Types in Banach spaces. Springer 2010).
Logical Extraction of BoundsAsymptotic regularity for pseudocontractions

Let X be a Banach space, C ⊂ X a bounded convex subset andf : C → C a (Lipschitzian) pseudocontraction.

Logical Extraction of BoundsAsymptotic regularity for pseudocontractions

Let X be a Banach space, C ⊂ X a bounded convex subset andf : C → C a (Lipschitzian) pseudocontraction.
In 1974 Bruck considered the following iteration schema
xn + 1 := (1 − λn )xn + λn f(xn ) − λn θn (xn − x1 ),for suitable (λn ), (θn ) in (0, 1] and showed asymptotic regularity andstrong convergence (towards a fixed point) results in Hilbert space.

Logical Extraction of BoundsAsymptotic regularity for Lipschitzian pseudocontractions
in arbitrary Banach spaces
Theorem (Chidume,Zegeye 2004): lim kxn − f(xn )k = 0, wheren→∞(i) lim θn = 0, (ii)θn−1(iv) lim

∞
P
n=1

−1
= 0,
λn θn

θn

λn θn = ∞, (iii) lim λθnn = 0,(v) λn (1 + θn ) ≤ 1.

Logical Extraction of BoundsAsymptotic regularity for Lipschitzian pseudocontractions
in arbitrary Banach spaces
Theorem (Chidume,Zegeye 2004): lim kxn − f(xn )k = 0, wheren→∞(i) lim θn = 0, (ii)θn−1(iv) lim

∞
P
n=1

−1
= 0,
λn θn

θn

λn θn = ∞, (iii) lim λθnn = 0,(v) λn (1 + θn ) ≤ 1.

Let D ≥ diam(C ), L-Lipschitz constant and (λn ), (θn ) ⊂ (0, 1] with rates
of conv./div. Ri : (0, ∞) → N
1∀ε > 0∀n ≥ R1 (ε) (θn ≤ ε), !
RP
2 (x)
2
∀x ∈ (0, ∞)λn θn ≥ x ,
n=1
3

4

∀ε > 0∀n ≥ R3 (ε) (λn ≤ θn ε),∀ε > 0∀n ≥ R4 (ε)

θn−1
θn −1

λn θn

!
≤ε .
Logical Extraction of Bounds

Theorem (D. Körnlein/K. Nonlinear Analysis 2011)∀ε > 0∀n ≥ Ψ (D, L, R1 , R2 , R3 , R4 , ε) (kxn − fxn k < ε)Logical Extraction of Bounds

Theorem (D. Körnlein/K. Nonlinear Analysis 2011)∀ε > 0∀n ≥ Ψ (D, L, R1 , R2 , R3 , R4 , ε) (kxn − fxn k < ε)
where


n
o
ε
Ψ (D, L, R1 , R2 , R3 , R4 , ε) = max N2 (C) + 1, R1
+1
2D
and

r

 
ε
ε
,
R
+
1
−
1
,
N1 (ε) := max R34
4D2 (2 + L)D2 x
N2 (x) := R2
+ 1,
2
!
!
2
8 (1 + L) D2
ε2
C :=+ 2 N1−1 .
2
ε2
8 (1 + L)

Logical Extraction of Bounds

Theorem (D. Körnlein/K. Nonlinear Analysis 2011)∀ε > 0∀n ≥ Ψ (D, L, R1 , R2 , R3 , R4 , ε) (kxn − fxn k < ε)
where


n
o
ε
Ψ (D, L, R1 , R2 , R3 , R4 , ε) = max N2 (C) + 1, R1
+1
2D
and

r

 
ε
ε
,
R
+
1
−
1
,
N1 (ε) := max R34
4D2 (2 + L)D2 x
N2 (x) := R2
+ 1,
2
!
!
2
8 (1 + L) D2
ε2
C :=+ 2 N1−1 .
2
ε2
8 (1 + L)

Exponential bound for unbounded C if Fix(f ) 6= ∅.
Logical Extraction of Bounds

Bounds on Metastability

Logical Extraction of Bounds

Bounds on Metastability
Tao used a rate of metastability for the von Neumann Mean Ergodic
Theorem as base step for a generalization to commuting families ofoperators.

Logical Extraction of Bounds

Bounds on Metastability
Tao used a rate of metastability for the von Neumann Mean Ergodic
Theorem as base step for a generalization to commuting families ofoperators.
‘We shall establish Theorem 1.6 by “finitary ergodic theory” techniques,reminiscent of those used in [Green-Tao]...’ ‘The main advantage ofworking in the finitary setting ... is that the underlying dynamical system
becomes extremely explicit’...‘In proof theory, this finitisation is known asGödel functional interpretation...which is also closely related to the
Kreisel no-counterexample interpretation’(T. Tao: Norm convergence of multiple ergodic averages for commuting
transformations, Ergodic Theor. and Dynam. Syst. 28, 2008)

Logical Extraction of Bounds

Let (xn ) be the Bruck iteration of an L-Lipschitzian pseudo-contraction
f : C → C, where C is a D-bounded closed and convex subset of a real
Hilbert space X.

Logical Extraction of Bounds

Let (xn ) be the Bruck iteration of an L-Lipschitzian pseudo-contraction
f : C → C, where C is a D-bounded closed and convex subset of a real
Hilbert space X.
Then (xn ) converges to a fixed point of f (Bruck, Chidume, Zegeye).

Logical Extraction of Bounds

Let (xn ) be the Bruck iteration of an L-Lipschitzian pseudo-contraction
f : C → C, where C is a D-bounded closed and convex subset of a real
Hilbert space X.
Then (xn ) converges to a fixed point of f (Bruck, Chidume, Zegeye).
Theorem (Körnlein/K., Num. Funct. Anal. Opt. 2013)((d64D2 /ε2 e)∀ε > 0 ∀g : IN → IN ∃n ≤ χM gh,χ(1) + Ψ(ε) + 1∀i, j ∈ [n; n + g (n)] ∀k ≥ n (kxi − xj k ≤ ε ∧ kTxk − xk k ≤ ε) ,Logical Extraction of Bounds

Let (xn ) be the Bruck iteration of an L-Lipschitzian pseudo-contraction
f : C → C, where C is a D-bounded closed and convex subset of a real
Hilbert space X.
Then (xn ) converges to a fixed point of f (Bruck, Chidume, Zegeye).
Theorem (Körnlein/K., Num. Funct. Anal. Opt. 2013)((d64D2 /ε2 e)∀ε > 0 ∀g : IN → IN ∃n ≤ χM gh,χ(1) + Ψ(ε) + 1∀i, j ∈ [n; n + g (n)] ∀k ≥ n (kxi − xj k ≤ ε ∧ kTxk − xk k ≤ ε) ,where h : IN → IN such that h(n) ≥ 1/θn for all n ∈ IN
and χ(n) := R1 (1/n), g0 (n) := g (n + 1 + Ψ (ε)) + Ψ (ε) + 1,
gh,χ (n) := max {h (i) : i ≤ χ(n) + g0 (χ(n))}
Here R1 and Ψ are as in the previous theorem.

Logical Extraction of Bounds

Cauchy problems and set-valued accretive operators
A set-valued operator A : D(A) → 2X is accretive if∀(x, u), (y, v) ∈ A hu − v, x − yi+ ≥ 0 ,where hy , xi+ := max{hy , ji : j ∈ J(x)} for the normalized duality map
J of the Banach space X .

Logical Extraction of Bounds

Cauchy problems and set-valued accretive operators
A set-valued operator A : D(A) → 2X is accretive if∀(x, u), (y, v) ∈ A hu − v, x − yi+ ≥ 0 ,where hy , xi+ := max{hy , ji : j ∈ J(x)} for the normalized duality map
J of the Banach space X .
A with 0 ∈ Az is uniformly accretive at zero with modulus
Θ : IN2 → IN if, moreover,∀k, K ∈ IN ∀(x, u) ∈ A kx−zk ∈ [2−k , K] → hu, x−zi+ ≥ 2−ΘK (k)(Koutsoukou-Argyraki/K. 2014).

Logical Extraction of BoundsCauchy problems and set-valued accretive operators
A set-valued operator A : D(A) → 2X is accretive if∀(x, u), (y, v) ∈ A hu − v, x − yi+ ≥ 0 ,where hy , xi+ := max{hy , ji : j ∈ J(x)} for the normalized duality map
J of the Banach space X .
A with 0 ∈ Az is uniformly accretive at zero with modulus
Θ : IN2 → IN if, moreover,∀k, K ∈ IN ∀(x, u) ∈ A kx−zk ∈ [2−k , K] → hu, x−zi+ ≥ 2−ΘK (k)(Koutsoukou-Argyraki/K. 2014). E.g. this holds for m-ψ-strongly
accretive operators or even for φ-accretive operators in the sense of
Garcı́a-Falset if φ has some normal form (which is the case in many
applications).
Logical Extraction of BoundsConsider the following homogeneous Cauchy problem for an accretive A(with range condition):(u0 (t) + A(u(t)) 3 0, t ∈ [0, ∞)(1)u(0) = x0 ,which has a unique integral solution for x0 ∈ D(A) given by the
Crandall-Liggett formulau(t) := S(t)(x0 ) := lim (I +
n→∞

t
n

A)−n (x0 ).

Logical Extraction of Bounds

Consider the following homogeneous Cauchy problem for an accretive A(with range condition):(u0 (t) + A(u(t)) 3 0, t ∈ [0, ∞)(1)u(0) = x0 ,which has a unique integral solution for x0 ∈ D(A) given by the
Crandall-Liggett formulau(t) := S(t)(x0 ) := lim (I +
n→∞

t
n

A)−n (x0 ).

A continuous v : [0, ∞) → D(A) is an almost-orbit of thenonexpansive semigroup S if
lim ( sup kv(t + s) − S(t)v(s)k) = 0.

s→∞ t∈[0,∞)Logical Extraction of Bounds

Theorem (Garcı́a-Falset 2005)
Let A be a φ-accretive (at zero) operator with range condition s.t. (1)has a strong solution for each xo ∈ D(A). Then every almost-orbit (forthe semigroup generated by −A) strongly converges to the zero z of A.

Logical Extraction of Bounds

Theorem (Garcı́a-Falset 2005)
Let A be a φ-accretive (at zero) operator with range condition s.t. (1)has a strong solution for each xo ∈ D(A). Then every almost-orbit (forthe semigroup generated by −A) strongly converges to the zero z of A.
Theorem (Koutsoukou-Argyraki/K. 2014)
Same as above but A uniformly accretive at zero with modulus Θ. Then∀k ∈ IN∀g : IN → IN∃n ≤ Ψ∀x ∈ [n, n + g(n)] kv(x) − zk < 2−k ,Logical Extraction of Bounds

Theorem (Garcı́a-Falset 2005)
Let A be a φ-accretive (at zero) operator with range condition s.t. (1)has a strong solution for each xo ∈ D(A). Then every almost-orbit (forthe semigroup generated by −A) strongly converges to the zero z of A.
Theorem (Koutsoukou-Argyraki/K. 2014)
Same as above but A uniformly accretive at zero with modulus Θ. Then∀k ∈ IN∀g : IN → IN∃n ≤ Ψ∀x ∈ [n, n + g(n)] kv(x) − zk < 2−k ,whereΨ(k, g, B, Φ, Θ) := Φ(k + 1, g) + h(Φ(k + 1, g)), with
ΘK(n) (k+2)+1
h(n) := (B(n), g(n) := g(n + h(n)) + h(n),lp + 2) · 2 m
K(n) :=
2(B(n) + 1) , B(n) ≥ 21 kv(n) − zk2 ,Logical Extraction of Bounds

Theorem (Garcı́a-Falset 2005)
Let A be a φ-accretive (at zero) operator with range condition s.t. (1)has a strong solution for each xo ∈ D(A). Then every almost-orbit (forthe semigroup generated by −A) strongly converges to the zero z of A.
Theorem (Koutsoukou-Argyraki/K. 2014)
Same as above but A uniformly accretive at zero with modulus Θ. Then∀k ∈ IN∀g : IN → IN∃n ≤ Ψ∀x ∈ [n, n + g(n)] kv(x) − zk < 2−k ,whereΨ(k, g, B, Φ, Θ) := Φ(k + 1, g) + h(Φ(k + 1, g)), with
ΘK(n) (k+2)+1
h(n) := (B(n), g(n) := g(n + h(n)) + h(n),lp + 2) · 2 m
K(n) :=
2(B(n) + 1) , B(n) ≥ 21 kv(n) − zk2 ,and Φ is rate of metastability for v, i.e.
∀k, g ∃n ≤ Φ(k, g)∀t ∈ [0, g(n)](kv(t + n) − S(t)v(n)k ≤ 2−k ).
Logical Extraction of Bounds

Application (compare Garcı́a-Falset, 2005)
Consider now the inhomogeneous Cauchy problem (A as before):(u0 (t) + A(u(t)) 3 f(t), t ∈ [0, ∞)(2)u(0) = x,where f ∈ L1 (0, ∞, X).

Logical Extraction of Bounds

Application (compare Garcı́a-Falset, 2005)
Consider now the inhomogeneous Cauchy problem (A as before):(u0 (t) + A(u(t)) 3 f(t), t ∈ [0, ∞)(2)u(0) = x,where f ∈ L1 (0, ∞, X).
Then for each x ∈ D(A) the integral solution u(·) of (2) is analmost-orbit (Miyadera-Kobayasi 1982)

Logical Extraction of Bounds

Application (compare Garcı́a-Falset, 2005)
Consider now the inhomogeneous Cauchy problem (A as before):(u0 (t) + A(u(t)) 3 f(t), t ∈ [0, ∞)(2)u(0) = x,where f ∈ L1 (0, ∞, X).
Then for each x ∈ D(A) the integral solution u(·) of (2) is analmost-orbit (Miyadera-Kobayasi 1982) and
Proposition (Koutsoukou-Argyraki/K., 2014)
R∞
k+1
ΦM (k, g) := g̃M·2 (0) with g̃(n) := n + g(n), M ≥ 0 kf(ξ)kdξ isa rate of metastability of u (and so can be used as Φ in the previous
theorem).

Logical Extraction of Bounds

A concrete Cauchy problem
Consider the following Cauchy problem (compare Andreu,Mazón, Moll
2005):
ut − div (|Du|p−2 Du) + ϕ(x, u) = f , on (0, ∞) × Ω,−∂u
∈ β(u) on [0, ∞) × ∂Ω,∂ηu(0, x) = u0 ∈ Lq (Ω),

where Ω is a bounded open domain in Rn with smooth boundary ∂Ω,∂uf ∈ L1 ((0, ∞), Lq (Ω)), 1 ≤ p, q < ∞, ∂η= h|Du|p−2 Du, ηi, η the unit
outward normal on ∂Ω, Du the gradient of u, β a maximal monotone
graph in R × R with 0 ∈ β(0) and ϕ : Ω × R → R satisfying the following
conditions:
Logical Extraction of Bounds

1

for almost all x ∈ Ω, r → ϕ(x, r ) is continuous and nondecreasing,2

for every r ∈ R, x → ϕ(x, r ) is in L1 (Ω),

3

ϕ(x, 0) = 0, ϕ(x, r ) 6= 0 whenever r 6= 0 and there exist λ > 0,
α ≥ 2 such that ϕ(x, r )r ≥ λ|r |α .

Logical Extraction of Bounds

1

for almost all x ∈ Ω, r → ϕ(x, r ) is continuous and nondecreasing,2

for every r ∈ R, x → ϕ(x, r ) is in L1 (Ω),

3

ϕ(x, 0) = 0, ϕ(x, r ) 6= 0 whenever r 6= 0 and there exist λ > 0,
α ≥ 2 such that ϕ(x, r )r ≥ λ|r |α .

Then the problem can be written in the form (2) s.t. (1) has a strong
solution (Garcı́a-Falset 2005) and A is even uniformly accretive at zerowith modulus being any
Θ(k) ≥ k · α − log2 Cα,Ω,λfor some constant Cα,Ω,λ depending only on the data indicated(Koutsoukou-Argyraki/K., 2014).

Logical Extraction of Bounds

Other Recent Applications to Nonlinear Analysis
Rates of asymptotic regularity and fluctuation bounds for the von
Neumann Mean Ergodic Theorem in uniformly convex Banach
spaces (K.,Leu¸stean ETDS 2009, Avigad, Rute ETDS 2013).

Logical Extraction of Bounds

Other Recent Applications to Nonlinear Analysis
Rates of asymptotic regularity and fluctuation bounds for the von
Neumann Mean Ergodic Theorem in uniformly convex Banach
spaces (K.,Leu¸stean ETDS 2009, Avigad, Rute ETDS 2013).
Metastability for Baillon’s nonlinear ergodic theorem(K., Comm.Contemp.Math. 2012).

Logical Extraction of Bounds

Other Recent Applications to Nonlinear Analysis
Rates of asymptotic regularity and fluctuation bounds for the von
Neumann Mean Ergodic Theorem in uniformly convex Banach
spaces (K.,Leu¸stean ETDS 2009, Avigad, Rute ETDS 2013).
Metastability for Baillon’s nonlinear ergodic theorem(K., Comm.Contemp.Math. 2012).
Metastability for Wittmann’s strong nonlinear ergodic theorem
on Halpern iterations (K., Adv.Math. 2011).

Logical Extraction of Bounds

Other Recent Applications to Nonlinear Analysis
Rates of asymptotic regularity and fluctuation bounds for the von
Neumann Mean Ergodic Theorem in uniformly convex Banach
spaces (K.,Leu¸stean ETDS 2009, Avigad, Rute ETDS 2013).
Metastability for Baillon’s nonlinear ergodic theorem(K., Comm.Contemp.Math. 2012).
Metastability for Wittmann’s strong nonlinear ergodic theorem
on Halpern iterations (K., Adv.Math. 2011).
Generalization of the above to CAT(0)-spaces (Saejung 2010)
and other iterations and uniformly smooth Banach spaces(Shioji,
Takahashi 1997) (K., Leu¸stean: Adv.Math. 2012, Schade, K.:
Fixed point theory 2012, K., Leu¸stean: Phil.Trans.RoyalSoc.2012, Körnlein (submitted)).

Logical Extraction of Bounds

Other Recent Applications to Nonlinear Analysis
Rates of asymptotic regularity and fluctuation bounds for the von
Neumann Mean Ergodic Theorem in uniformly convex Banach
spaces (K.,Leu¸stean ETDS 2009, Avigad, Rute ETDS 2013).
Metastability for Baillon’s nonlinear ergodic theorem(K., Comm.Contemp.Math. 2012).
Metastability for Wittmann’s strong nonlinear ergodic theorem
on Halpern iterations (K., Adv.Math. 2011).
Generalization of the above to CAT(0)-spaces (Saejung 2010)
and other iterations and uniformly smooth Banach spaces(Shioji,
Takahashi 1997) (K., Leu¸stean: Adv.Math. 2012, Schade, K.:
Fixed point theory 2012, K., Leu¸stean: Phil.Trans.RoyalSoc.2012, Körnlein (submitted)).
Generalization to CAT(κ) spaces κ > 0(Leu¸stean, Nicolae (submitted)).
Logical Extraction of Bounds

Metastable version of strong nonlinear ergodic theorem for
maps∀u, v ∈ C (kf(u) + f(v)k ≤ ku + vk).
(covers Baillon’s result for n.e. odd operators):
Safarik, JMAA 2012.

Logical Extraction of Bounds

Metastable version of strong nonlinear ergodic theorem for
maps∀u, v ∈ C (kf(u) + f(v)k ≤ ku + vk).
(covers Baillon’s result for n.e. odd operators):
Safarik, JMAA 2012.
Rates of convergence for Kirk’s 2003 fixed point theorem on
asymptotic contractions (proved originally using ultraproducts)(Gerhardy: JMAA 2006, Briseid: JMAA 2007).

Logical Extraction of Bounds

Metastable version of strong nonlinear ergodic theorem for
maps∀u, v ∈ C (kf(u) + f(v)k ≤ ku + vk).
(covers Baillon’s result for n.e. odd operators):
Safarik, JMAA 2012.
Rates of convergence for Kirk’s 2003 fixed point theorem on
asymptotic contractions (proved originally using ultraproducts)(Gerhardy: JMAA 2006, Briseid: JMAA 2007).
Rates of asymptotic regularity and metastability for
Krasnoselski-Mann iterations in normed and W -hyperbolic spaces(K., Num.Funct.Anal.Opt.2001, K., Nonlinear Anal.2005
K., Leu¸stean, Abstr.Appl.Anal.2003, JEMS 2010, ).

Logical Extraction of Bounds

Metastable version of strong nonlinear ergodic theorem for
maps∀u, v ∈ C (kf(u) + f(v)k ≤ ku + vk).
(covers Baillon’s result for n.e. odd operators):
Safarik, JMAA 2012.
Rates of convergence for Kirk’s 2003 fixed point theorem on
asymptotic contractions (proved originally using ultraproducts)(Gerhardy: JMAA 2006, Briseid: JMAA 2007).
Rates of asymptotic regularity and metastability for
Krasnoselski-Mann iterations in normed and W -hyperbolic spaces(K., Num.Funct.Anal.Opt.2001, K., Nonlinear Anal.2005
K., Leu¸stean, Abstr.Appl.Anal.2003, JEMS 2010, ).
Rates for algorithms computing common fixed points of familiesof nonexpansive maps. (M.A.A. Khan/K., JMAA 2013).

Logical Extraction of Bounds

Metastable version of strong nonlinear ergodic theorem for
maps∀u, v ∈ C (kf(u) + f(v)k ≤ ku + vk).
(covers Baillon’s result for n.e. odd operators):
Safarik, JMAA 2012.
Rates of convergence for Kirk’s 2003 fixed point theorem on
asymptotic contractions (proved originally using ultraproducts)(Gerhardy: JMAA 2006, Briseid: JMAA 2007).
Rates of asymptotic regularity and metastability for
Krasnoselski-Mann iterations in normed and W -hyperbolic spaces(K., Num.Funct.Anal.Opt.2001, K., Nonlinear Anal.2005
K., Leu¸stean, Abstr.Appl.Anal.2003, JEMS 2010, ).
Rates for algorithms computing common fixed points of familiesof nonexpansive maps. (M.A.A. Khan/K., JMAA 2013).
Rates of convergence for image recovery algorithms in uniformly
convex spaces. (M.A.A. Khan/K., Nonlinear Analysis 2014).
Logical Extraction of Bounds