ファイル置き場 Sendai Logic Homepage speaker9

(1)

Logical Extraction of Effective

bounds from Proofs in Nonlinear

Ergodic Theory

Ulrich Kohlenbach

Department of Mathematics

Technische Universit¨ at Darmstadt

Tokyo, February 20-23, 2012

(2)

Logical analysis of proofs P

Goal:Additional information on the conclusion C : Quantitative information: effective bounds.

(3)

Logical analysis of proofs P

Qualitative information: new uniformity results(relevance pointed out by T. Tao).

(4)

Logical analysis of proofs P

Logical methods: Proof Interpretations interpretthe formulas A in P : A 7→ A^I,

(5)

Logical analysis of proofs P

interpretation C^I contains theadditional information,

(6)

Logical analysis of proofs P

interpretation CÎ contains theadditional information, construct byrecursion on P a new proof PÎ of CÎ.

(7)

Logical analysis of proofs P

interpretation CÎ contains theadditional information, construct byrecursion on P a new proof PÎ of CÎ. Our approach is based on novel forms and extensions of:

K. G¨odel’s functional interpretation!

(8)

Goal:Extract uniform effective bounds for

∀x ∈ . . . ∃n ∈ IN A(x, n)-theorems.

(9)

Restriction:Because of classical logic: in general A must be purely existential.

(10)

Convergence in metric spaces:Let (x_n) be a Cauchy sequence in a metric space (X , ρ), i.e.

∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi, xj) ≤ 2^−k) ∈ Π⁰₃

(11)

∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi, xj) ≤ 2^−k) ∈ Π⁰₃ isineffectivelyequivalent to

∀k ∈ IN g ∈ IN^IN∃n ∈ IN∀i, j ∈ [n; n + g(n)] (ρ(xi, xj) < 2^−k) ∈ ∀∃

(12)

∀k ∈ IN ∃n ∈ IN ∀i, j ≥ n (ρ(xi, xj) ≤ 2^−k) ∈ Π⁰₃ isineffectivelyequivalent to

∀k ∈ IN g ∈ IN^IN∃n ∈ IN∀i, j ∈ [n; n + g(n)] (ρ(xi, xj) < 2^−k) ∈ ∀∃ Herbrand normal formormetastability(Tao).

(13)

Effective full rates of convergence?

(14)

Effective full rates of convergence?

Usuallypossible for asymptotic regularityresults

ρ(xn, f(xn)) → 0,

even when (x_n) may not converge to a fixed point of f .

(15)

Effective full rates of convergence?

Usuallypossible for asymptotic regularityresults

ρ(xn, f(xn)) → 0,

even when (x_n) may not converge to a fixed point of f . Possible for (x_n) if sequence converges to uniquefixed

point/solution. Extraction ofmodulus of uniquenessgives rate of convergence! Numerous applications in analysis!

(16)

An Example from Ergodic Theory

X Hilbert space, f : X → X linearandkf(x)k ≤ kxkfor all x ∈ X .

An(x) := ¹

n + 1^Sⁿ(x), where Sn(x) := Xn

i=0

fⁱ(x) (n ≥ 0)

(17)

An Example from Ergodic Theory

An(x) := ¹

i=0

fⁱ(x) (n ≥ 0)

Theorem (von Neumann Mean Ergodic Theorem) For every x ∈ X , the sequence (A_n(x))_nconverges.

(18)

An Example from Ergodic Theory

An(x) := ¹

i=0

fⁱ(x) (n ≥ 0)

Theorem (von Neumann Mean Ergodic Theorem)

For every x ∈ X , the sequence (A_n(x))_nconverges. Avigad/Gerhardy/Towsner (TAMS 2010):

in generalno computable rate of convergence. But:Prim.rec. bound on metastable version!

(19)

An Example from Ergodic Theory

An(x) := ¹

i=0

fⁱ(x) (n ≥ 0)

Theorem (von Neumann Mean Ergodic Theorem)

For every x ∈ X , the sequence (A_n(x))_nconverges. Avigad/Gerhardy/Towsner (TAMS 2010):

in generalno computable rate of convergence. But:Prim.rec. bound on metastable version! Theorem (Garrett Birkhoff 1939)

Mean Ergodic Theorem holds for uniformly convex Banach spaces.

(20)

Based on logical metatheorem to be discussed below:

Theorem (Leu¸stean/K., Ergodic Theor. Dynam. Syst. 2009) X uniformly convex Banach space, η a modulus of uniform convexity and f : X → X as above, b > 0.

Then for all x ∈ X with kxk ≤ b, all ε > 0, all g : IN → IN :

∃n ≤ Φ(ε, g, b, η) ∀i, j ∈ [n; n + g(n)] kAi(x) − Aj(x)k < ε,

(21)

where

Φ(ε, g, b, η) := M · ˜h^K(0), with

M :=^16b_ε , γ := ₁₆^εη _8b^ε, K :=^l^b_γ^m,

h, ˜h : IN → IN, h(n) := 2(Mn + g(Mn)), ^˜h(n) := maxi≤nh(i).

(22)

where

Φ(ε, g, b, η) := M · ˜h^K(0), with

M :=^16b_ε , γ := ₁₆^εη _8b^ε, K :=^l^b_γ^m,

h, ˜h : IN → IN, h(n) := 2(Mn + g(Mn)), ^˜h(n) := maxi≤nh(i).

Special Hilbert case: treated prior by Avigad/Gerhardy/Towsner (again based on logical metatheorem).

(23)

General logical metatheorems for abstract

(nonseparable) spaces

In the example of theMean Ergodic Theoremone got bounds on the metastable version that were

(24)

General logical metatheorems for abstract

(nonseparable) spaces

uniform in (i.e. independent of) the choice of the starting point kxkexcept for a norm upper bound b ≥ kxk although closed bounded convex sets in X are not compact (except for IRⁿ),

(25)

General logical metatheorems for abstract

(nonseparable) spaces

uniform in (i.e. independent of) the choice of the starting point kxkexcept for a norm upper bound b ≥ kxk although closed bounded convex sets in X are not compact (except for IRⁿ), uniform in the nonexpansive operator,

(26)

General logical metatheorems for abstract

(nonseparable) spaces

uniform in the choice of the space X (except for a modulus of uniform convexity).

(27)

General logical metatheorems for abstract

(nonseparable) spaces

Logical Metatheorems (K. TAMS2005, Gerhardy/K. TAMS 2008) explainthis strong uniformity in terms ofmajorizability(see below).

(28)

General logical metatheorems for abstract

(nonseparable) spaces

Logical Metatheorems (K. TAMS2005, Gerhardy/K. TAMS 2008) explainthis strong uniformity in terms ofmajorizability(see below). Crucial:no separability assumption on X was used.

(29)

A novel form of majorization

y , x functionals of types ρ and bρ := ρ[IN/X ]: xÎN &_INyÎN :≡ x ≥ y xÎN &Xy^X :≡ x ≥ kyk.

(30)

A novel form of majorization

Forcomplex typesρ → τ this is extended in ahereditary fashion.

(31)

A novel form of majorization

Forcomplex typesρ → τ this is extended in ahereditary fashion. Example:

f^∗&X→Xf ≡ ∀n ∈ IN, x ∈ X[n ≥ kxk → f^∗(n) ≥ kf(x)].

(32)

A novel form of majorization

f^∗&X→Xf ≡ ∀n ∈ IN, x ∈ X[n ≥ kxk → f^∗(n) ≥ kf(x)]. f : X → X isnonexpansive (n.e.) ifkf(x) − f(y)k ≤ kx − yk. Then λn.n + b &_{X →X} f , if b ≥ kf (0)k.

(33)

A novel form of majorization

f^∗&X→Xf ≡ ∀n ∈ IN, x ∈ X[n ≥ kxk → f^∗(n) ≥ kf(x)]. f : X → X isnonexpansive (n.e.) ifkf(x) − f(y)k ≤ kx − yk. Then λn.n + b &_{X →X} f , if b ≥ kf (0)k.

Forlinearandnonexpansivef : Id & f .

(34)

Baillon’s nonlinear ergodic theorem

Theorem(J.-B. Baillon 1975): X Hilbert space, C ⊂ X bounded closed and convex, f : C → C nonexpansive. Then for every x0∈ C , the sequence of Ces`aro means (x_n)

xn:= ¹ n + 1

Xn k=0

f^(k)(x0)

converges weaklyto a fixed point of f .

(35)

Baillon’s nonlinear ergodic theorem

xn:= ¹ n + 1

Xn k=0

f^(k)(x0)

All proofs of this celebrated theorem useweak sequential compactness. A particular simple proof is due to Br´ezis and Browder (1976).

(36)

Baillon’s nonlinear ergodic theorem

xn:= ¹ n + 1

Xn k=0

f^(k)(x0)

Strong convergence in general fails (counterexample by Baillon).

(37)

Baillon’s nonlinear ergodic theorem

xn:= ¹ n + 1

Xn k=0

f^(k)(x0)

Strong convergence in general fails (counterexample by Baillon). In important special cases(see below)strong convergencecan be established.

(38)

A quantitative ‘metastable’ version of

Baillon’s theorem

Theorem (K., Communications in Contemporary Math. 2012) Logical analysis of the proof of Baillon’s theorem due to Br´ezis-Browder yields a primitive recursive functional ϕ such that for a bar-recursive bound Ω^∗ extracted from the weak compactness proof and

ε > 0, g : IN → IN, we get ϕ(Ω^∗, ε, b, g ) as a bound on the metastable version of the weak Cauchy property of the Ces`aro means (x_n), i.e.

∀w ∈ B1(0) ∃n ≤ ϕ(Ω^∗, ε, b, g) ∀i, j ∈ [n; n+g(n)] |hxi−xj, wi| < ε.

(39)

A quantitative ‘metastable’ version of

Baillon’s theorem

Theorem (K., Communications in Contemporary Math. 2012) Logical analysis of the proof of Baillon’s theorem due to Br´ezis-Browder yields a primitive recursive functional ϕ such that for a bar-recursive bound Ω^∗ extracted from the weak compactness proof and

ε > 0, g : IN → IN, we get ϕ(Ω^∗, ε, b, g ) as a bound on the metastable version of the weak Cauchy property of the Ces`aro means (x_n), i.e.

∀w ∈ B1(0) ∃n ≤ ϕ(Ω^∗, ε, b, g) ∀i, j ∈ [n; n+g(n)] |hxi−xj, wi| < ε.

Based on the detailed construction of Ω^∗ and results of W.A. Howard it follows that Φ(ε, b, g ) := ϕ(Ω^∗, ε, b, g ) is definable in G¨odel’s T4(note that Φ has type level 2).

(40)

A theorem of R. Wittmann

(41)

A theorem of R. Wittmann

Halpern iterations:f : C → C nonexpansive, x0∈ C , α_n∈ [0, 1] xn+1:= αn+1x0+ (1 − αn+1) f(xn).

(42)

A theorem of R. Wittmann

Using weak compactness, Wittmann proved in 1992:

Theorem(R. Wittmann 1992): C ⊆ X closed and convex, x0∈ C and Fix(f ) 6= ∅. Under suitable conditions on (α_n) (satisfied e.g. for α_n:= _n+1¹ ) (x_n) converges strongly towards the fixed point of f that is closest to x0.

(43)

A theorem of R. Wittmann

Using weak compactness, Wittmann proved in 1992:

Theorem(R. Wittmann 1992): C ⊆ X closed and convex, x0∈ C and Fix(f ) 6= ∅. Under suitable conditions on (α_n) (satisfied e.g. for α_n:= _n+1¹ ) (x_n) converges strongly towards the fixed point of f that is closest to x0.

Remark:Wittmann’s theorem is anonlinear generalization of the Mean ergodic theorem: for α_n:= 1/(n + 1), C := X andlinearf , the Halpern iteration coincides with the Ces`aro means. Hence the Mean ergodic theorem follows as a special case.

(44)

General features of the logical analysis of

the proof due Wittmann

(45)

General features of the logical analysis of

the proof due Wittmann

In Wittmann’s proof the use of weak compactness gets in the end eliminated via a quantitative projection argument.

(46)

General features of the logical analysis of

the proof due Wittmann

As a consequence, the proof yields an ordinary primitive recursive bound withelementary verification.

(47)

General features of the logical analysis of

the proof due Wittmann

As a consequence, the proof yields an ordinary primitive recursive bound withelementary verification.

In the following letd ≥ diam(C) := sup{kx − yk : x, y ∈ C}or d ≥ 4kx0− pk for some p ∈ Fix(f ).

(48)

A quantitative metastable version of

Wittmann’s theorem

Theorem (K., Advances in Mathematics 2011)

Let α_n:= 1/(n + 1) and (x_n) the Halpern iteration. Then for ε ∈ (0, 1)

∀g : IN^IN∃k ≤ Φ(ε/2, g⁺, d) ∀i, j ∈ [k; k + g(k)] kxi− xjk ≤ ε,

(49)

A quantitative metastable version of

Wittmann’s theorem

Theorem (K., Advances in Mathematics 2011)

Let α_n:= 1/(n + 1) and (x_n) the Halpern iteration. Then for ε ∈ (0, 1)

∀g : IN^IN∃k ≤ Φ(ε/2, g⁺, d) ∀i, j ∈ [k; k + g(k)] kxi− xjk ≤ ε, where

Φ(ε, g, d) := ρ(ε²/4d², χd,ε(Nε,g,d)) with Nε,g,d:= 16d ·maxⁿ(∆^∗_ε,g)⁽ⁱ⁾(1) : i ≤ nε,d

o2

, nε,d :=^l^d_ε²

d

m,

εd:= _8192d^ε⁴2_, ∆_ε,g^∗ (n) := ⌈1/Ωd(ε/2, ˜g^M, χd,ε(16d · n²))⌉,

with Ωd(ε, g, j) := δε,˜g(ρ(ε²/2d²,j)), where δε,m:= _16dm^ε² , ρ(ε, n) :=ⁿ⁺¹_ε , χd,ε(n) := maxⁿχd(n),^l^32d_ε2²

mo,

χd(n) := 4dn(4dn + 2), ˜g(n) := max{n, g(n)}, g⁺(n) := n + g(n).

(50)

Recent developments

In 2010, Saejung generalized Wittmann’s theorem toCAT(0) spaces, i.e geodesic spaces (X , ρ) satisfying the Bruhat-Tits inequality

(51)

Recent developments

∀x, y, z, m ∈ X ρ(x, m) = ρ(y, m) = ¹₂ρ(x, y) → ρ(z, m)²≤ ¹₂ρ(z, x)²+₂¹ρ(z, y)²− ¹₄ρ(x, y)².

(52)

Recent developments

Rather than weak compactness, the proof uses Banach limits, i.e. linear, shift-invariant, positive, Norm-1 operators µ : l^∞→ IR (and hence AC).

(53)

Recent developments

Rather than weak compactness, the proof uses Banach limits, i.e. linear, shift-invariant, positive, Norm-1 operators µ : l^∞→ IR (and hence AC).

June 2011: Leu¸stean/K. extracted a primitive recursive rate of metastability from this proof (therebyeliminating any use of Banach limits).

(54)

Strategy of Elimination

Replace linear µ by sublinear operator

q : l^∞→ IR, q((an)) := lim sup

p→∞ ^sup_n≥1

1 p

n+p−1_X i=n

ai.

(55)

Strategy of Elimination

Replace linear µ by sublinear operator

q : l^∞→ IR, q((an)) := lim sup

p→∞ ^sup_n≥1

1 p

n+p−1_X i=n

ai.

Eliminate q by proving appropriate uniform quantitative lemmas on

Cn,p((ak)) = ¹ p

n+p−1_X i=n

ai.

(56)

Rate of Metastability in Saejung’s Theorem

Theorem (Leu¸stean/K., 2011)

X CAT(0), C ⊆ X convex, diam(C ) ≤ d, (x_n) as above, ε ∈ (0, 1) :

∀g : IN^IN∃k ≤ Σ(ε, g, d) ∀i, j ∈ [k; k + g(k)] ρ(xi, xj) ≤ ε,

(57)

Rate of Metastability in Saejung’s Theorem

Theorem (Leu¸stean/K., 2011)

X CAT(0), C ⊆ X convex, diam(C ) ≤ d, (x_n) as above, ε ∈ (0, 1) :

∀g : IN^IN∃k ≤ Σ(ε, g, d) ∀i, j ∈ [k; k + g(k)] ρ(xi, xj) ≤ ε,

Σ(ε, g, d) :=^l^3dχ^∗^L_ε^(ε/3)^m+ 1, with L := fh^∗^(⌈d

2/ε²₀⌉)

(0) +^l_ε¹2 0

m , χ^∗_k(ε) :=^l^16d²^(˜^P^k^(ε/2)+1)_ε +^96d⁴^(˜^P^k^(ε/2)+1)_ε2 ²

m

, ε0:= ε²/24(d + 1)², P˜k(ε) :=^l^12d²^(k+1)_ε ^l^48d(k+1)_ε +^2304d⁴_ε^(k+1)2 ²

m− 1^m,

Θk(ε) :=^l^3dχ^∗^k_ε^(ε/3)^m+ 1, ∆^∗_k(ε, g) := ^ε

3gε,k₍Θk(ε)−χ^∗_k(ε/3)₎^,

gε,k(n) := n + g n + χ^∗_k ^ε₃, h(k) := max^nl_∆∗ ^d² k^(ε²^/4,g)

m

, k^o− k, h^∗(k) := hk +^l_ε¹2

0

m +^l_ε¹2

0

m

, fh^∗(k) := k + h^∗(k).

(58)

Further consequences of the analysis

(59)

Further consequences of the analysis

Aquadraticfull rate of convergence for the asymptotic regularity ρ(xn, f(xn)) → 0:

∀ε > 0 ∀n ≥ ^4d ε ⁺

16d²

ε² ^(ρ(xⁿ^{, f(x}ⁿ)) < ε).

(60)

Further consequences of the analysis

∀ε > 0 ∀n ≥ ^4d ε ⁺

16d²

ε² ^(ρ(xⁿ^{, f(x}ⁿ)) < ε).

Let z_k be the unique fixed point of thecontraction fk(x) := ¹

k^{x ⊕ (1 −} 1 k^)f(x).

Then the analysis yields primitive recursively in a given rate K of convergence of the resolvent (z_k) a rate of convergence of (x_n).

(61)

Further consequences of the analysis

∀ε > 0 ∀n ≥ ^4d ε ⁺

16d²

ε² ^(ρ(xⁿ^{, f(x}ⁿ)) < ε).

k^{x ⊕ (1 −} 1 k^)f(x).

Then the analysis yields primitive recursively in a given rate K of convergence of the resolvent (z_k) a rate of convergence of (x_n). For effective X , f , x and z := lim z_k :K is computableiffkz − xk is computable.

(62)

Further consequences of the analysis

∀ε > 0 ∀n ≥ ^4d ε ⁺

16d²

ε² ^(ρ(xⁿ^{, f(x}ⁿ)) < ε).

k^{x ⊕ (1 −} 1 k^)f(x).

Then the analysis yields primitive recursively in a given rate K of convergence of the resolvent (z_k) a rate of convergence of (x_n). For effective X , f , x and z := lim z_k :K is computableiffkz − xk is computable.

Similar results for uniformly smooth Banach spaces:Leustean/K., Phil. Trans. Royal Soc. A, to appear.

(63)

Another strong nonlinear ergodic theorem

Already in 1976 Baillon proved strong convergence of Ces`aro means if

∀v ∈ C (−v ∈ C ) and f is nonexpansive and odd, i.e. f (−v ) = −f (v ).

(64)

Another strong nonlinear ergodic theorem

∀v ∈ C (−v ∈ C ) and f is nonexpansive and odd, i.e. f (−v ) = −f (v ). This was generalized by Wittmann in 1990:

Theorem[R. Wittmann 1990]: Let C ⊆ X be an arbitrarysubset and f : C → C s.t.

∀u, v ∈ C (kf(u) + f(v)k ≤ ku + vk). Then the sequence of Ces`aro means (x_n) converges strongly.

(65)

Another strong nonlinear ergodic theorem

Holds for C closed under v 7→ −v and nonexpansive, odd f .

(66)

Another strong nonlinear ergodic theorem

Holds for C closed under v 7→ −v and nonexpansive, odd f .

The condition above doesnot evenimply that f iscontinuous. But f has atrivial majorantf^∗:= Id (v := u).

Hence: Metatheorem applicable!

(67)

Recently, P. Safarik extracted a primitive recursive bound Φ(k, b, g^M) on the rate of metastability from the proof (with IN ∋ b ≥ kx0k):

Theorem (P. Safarik, to appear in: J. Math. Anal. Appl.)

∀k ∈ IN ∀g ∈ IN^IN∃m ≤ Φ(k, b, g^M) (kxm− xm+g(m)k ≤ 2^−k),

(68)

Recently, P. Safarik extracted a primitive recursive bound Φ(k, b, g^M) on the rate of metastability from the proof (with IN ∋ b ≥ kx0k):

Theorem (P. Safarik, to appear in: J. Math. Anal. Appl.)

∀k ∈ IN ∀g ∈ IN^IN∃m ≤ Φ(k, b, g^M) (kxm− xm+g(m)k ≤ 2^−k), where

Φ(k, b, g) := (N(2k + 7, g) + P(2k + 7, g)) · b · 2^2k+8+ 1, P(k, g) := P0(k, F(k, g, N(k, g))),

F(k, g, n)(p) := p + n + ˜g((n + p) · b · 2^k+1),

L(k, g)(n) := n +P0(k, F(k, g, n)) + ˜g((n +P0(k, F(k, g, n)))·b·2^k+1), N(k, g) := (L(k, g))^(b²²^k+2⁾(0),

P0(k, f) := ˜f^(b²²^k⁾(0), ˜f(n) := n + f(n), f^M(n) := max

i≤n+1^f(i).

(69)

An application to metric fixed point theory

Let X be a Banach space, C ⊂ X a bounded convex subset and f : C → C a Lipschitzian pseudocontraction (Browder), i.e.

(70)

An application to metric fixed point theory

∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k.

(71)

An application to metric fixed point theory

∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k. Let (x_n) be defined by the Bruck formula:

xn+ 1 := (1 − λn)xn+ λnf(xn) − λnθn(xn− x1), where (λ_n), (θ_n) ⊂ (0, 1] with

(72)

An application to metric fixed point theory

∀u, v ∈ C∀λ > 1 (λ − 1)ku − vk ≤ k(λI − f)(u) − (λI − f)(v)k. Let (x_n) be defined by the Bruck formula:

xn+ 1 := (1 − λn)xn+ λnf(xn) − λnθn(xn− x1), where (λ_n), (θ_n) ⊂ (0, 1] with

(i) lim θn = 0, (ii) P∞ n=1

λnθn= ∞, (iii) lim^λ_θⁿ

n ^{= 0,}

(iv) lim

θn−1

θn ⁻¹

λnθn ^{= 0, (v) λ}ⁿ^{(1 + θ}ⁿ^{) ≤ 1.}

(73)

Convergence of Bruck’s formula for

Lipschitzian pseudocontrations

Theorem (Chidume,Zegeye 2004): lim

n→∞^kxⁿ^{− f(x}ⁿ^{)k = 0.}

(74)

Convergence of Bruck’s formula for

Lipschitzian pseudocontrations

Theorem (Chidume,Zegeye 2004): lim

n→∞^kxⁿ^{− f(x}ⁿ^{)k = 0.}

Let M ≥ diam(C ) and (λ_n), (θ_n) ⊂ (0, 1] with rates of conv./div. R_i : (0, ∞) → N

1 ∀ε > 0∀n ≥ R1(ε) (θ_n≤ ε),

2 ∀x ∈ (0, ∞) ^R

2_(x)

P

n=1

λ_nθ_n≥ x

! ,

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

4 ∀ε > 0∀n ≥ R4(ε)

˛

θn−1 θn ⁻¹

˛

˛ λn^θn ^{≤ ε}

! .

(75)

Polynomial rate of convergenceextracted from Chidume/Zegeye:

(76)

Polynomial rate of convergenceextracted from Chidume/Zegeye: Theorem (D. K¨ornlein/K. Nonlinear Analysis 2011)

∀ε > 0∀n ≥ Ψ (M, L, R1, R2, R3, R4, ε) (kxn− f(xn)k < ε)

(77)

Polynomial rate of convergenceextracted from Chidume/Zegeye: Theorem (D. K¨ornlein/K. Nonlinear Analysis 2011)

∀ε > 0∀n ≥ Ψ (M, L, R1, R2, R3, R4, ε) (kxn− f(xn)k < ε) where

Ψ (M, L, R1, R2, R3, R4, ε) = maxⁿN2(C) + 1, R1

_ε 2M

+ 1^o

and

N1(ε) := max

R3

_ε

4M²(2 + L)

, R4

r _ε

M² ^{+ 1 − 1}

,

N2(x) := R2

_x 2

+ 1,

C := ^{8 (1 + L)}

2M²

ε² ^{+ 2} ^N¹

ε² 8 (1 + L)²

!

− 1

! .