A proof-theoretic bound extraction theorem for CAT(κ)-spaces

A proof-theoretic bound extraction theorem for CAT(κ)-spaces U. Kohlenbach1, A. Nicolae2,3 1Department of Mathematics, Technische Universit¨at Darmstadt, Schlossgartenstraße 7, 64289 Darmstadt, Germany kohlen[email protected] 2Department of Mathematical Analysis, University of Seville Apdo. 1160, 41080 Sevilla, Spain 3Department of Mathematics, Babe¸s-Bolyai University, Kog˘alniceanu 1, 400084 Cluj-Napoca, Romania [email protected]cluj.ro November 14, 2016 Abstract Starting in 2005, general logical metatheorems have been developed that guarantee the extractability of uniform effective bounds from large classes of proofs of theorems that involve abstract metric structures X. In this paper we adapt this to the class of CAT(κ)-spaces Xfor κ > 0 and establish a new metatheorem that explains specific bound extractions that recently have been achieved in this context as instances of a general logical phenomenon. Keywords: Proof mining, effective bounds, CAT(κ)-spaces. Mathematics Subject Classification (2010): 03F10, 53C22, 58D17 1 Introduction Beginning in 2005, general logical metatheorems have been developed that guarantee the extractability of explicit effective and highly uniform bounds from large classes of proofs in nonlinear analysis that work in the setting of abstract classes of metric spaces that are not assumed to be separable (see [10, 6, 11, 7]). Whereas in the separable context (studied already in [8]) uniformity from input data in general can only be expected to hold in the case of compactness, the abstract setting for sufficiently uniform classes of structures makes this possible as long as metrical bounds are imposed. Metric and normed structures to which this logic-based proof-theoretic approach has been adapted so far are: metric spaces, W-hyperbolic spaces, CAT(0)-spaces, uniformly convex W-hyperbolic spaces, δhyperbolic spaces, R-trees, normed spaces, uniformly convex normed and Hilbert spaces, metric completions of these spaces, Banach lattices, abstract Lpand C(K)-spaces and others. The logic-based approach towards bound extractions from given proofs, also called ‘proof mining’, has resulted in numerous new results obtained for theorems in nonlinear 1 analysis that are formulated in the context of such spaces (see [13] for a survey and for references). In recent years, the class of CAT(κ)-spaces for κ > 0 has received particular attention in fixed point and ergodic theory as well as in convex optimization (see e.g. [1, 5, 14, 15]). These spaces are defined via comparison properties for geodesic triangles and represent a generalization of smooth Riemannian manifolds of sectional curvature bounded above by κ(for a detailed introduction to CAT(κ)-spaces we refer to [3]). It has turned out that ‘proof-mining’-results that previously had been obtained only for CAT(0)-spaces could be generalized to the CAT(κ)-setting (see [14] for a particularly striking instance of this and [12] for an application of proof mining for convex feasibility problems in CAT(κ)-spaces). This raises the natural question on whether these findings can be explained in general logical terms, i.e. whether one can formulate general logical metatheorems on bound extractions also for the class of CAT(κ)-spaces. In this note we give a positive answer to this question. 2 Main Results In this paper, Nalways denotes the set {0,1,2, . . .}.In the following, we make free use of the representation of real numbers (given as fast converging Cauchy sequences of rationals) by names in NNfrom [11] by which every function in NNrepresents a unique real number while every real number has many different names in NNand so actually corresponds to an equivalence class w.r.t. a Π0 1-equivalence relation f=Rgon NN.Noneffectively, though, one can select a unique ‘canonical’ representing function (x)◦∈NNof x∈[0,∞) by (x)◦(n) := j(2k0,2n+1 −1),where k0:= max kk 2n+1 ≤x. Here j:N2→Ndenotes the standard Cantor pairing function. Remark 2.1. Modulo the encoding of rational numbers by natural numbers as used in [11], (x)◦is the Cauchy sequence whose n-th element is the largest dyadic rational number of the form k/2n+1 that is ≤x. To represent quantification over [0,1] we use the operation ˜ (·) : NN→NN, f 7→ ˜ ffrom Definition 4.24 in [11] with the properties (provably in weak fragments of arithmetic in all finite types, see Lemma 4.25 in [11]) (i) 0R≤R˜x≤R1R, (ii) 0R≤Rx≤R1R→˜x=Rx, (iii)x >R1R→˜x=R1R, x <R0R→˜x=R0R. Metric spaces (X, d) are represented as quotients of pseudometric spaces where the latter are given by a constant dXof type X×X→NNsatisfying the axioms (d1) ∀xX(dX(x, x) =R0R), (d2) ∀xX, yX(dX(x, y) =RdX(y, x)), (d3) ∀xX, yX, zX(dX(x, z)≤RdX(x, y) +RdX(y, z)). 2 In order to axiomatize CAT(κ)-spaces (X, d) (for fixed κ > 0) with diam(X)≤π/(2√κ) we first add a constant WXof type X×X×NN→Xrepresenting a convexity operator W:X×X×[0,1] →Xsatisfying the axioms (W1) ∀xX, yX, zX∀λNNdX(z, WX(x, y, λ)) ≤R(1R−R˜ λ)·RdX(z, x) +R˜ λ·RdX(z, y), (W2) ∀xX, yX∀λNN 1, λNN 2dX(WX(x, y, λ1), WX(x, y, λ2)) =R|˜ λ1−R˜ λ2|R·RdX(x, y), (W3) ∀xX, yX∀λNNWX(x, y, λ) =XWX(y, x, 1R−Rλ) (i.e. (X, d, W) is a space of hyperbolic type, see [10]) and - instead of (W4) used in [10] to define the class of (W)-hyperbolic spaces - we now have the axiom (W5) : ∀xX, yX, zX∀λNN(dX(WX(x, z, λ), WX(y, z, λ)) ≤dX(x, y)), which expresses that d(W(x, z, λ), W(y, z, λ)) ≤d(x, y) for all λ∈[0,1] and x, y, z ∈X. Remark 2.2. The reason why in the axioms above we can write λinstead of ˜ λis that (W2) implies that WX(x, y, λ) =XWX(x, y, ˜ λ)since, by the properties (i),(ii)above, ˜ ˜ λ=R˜ λ. So the intended meaning of WX(x, y, λ)is (given a convexity operator W): WX(x, y, λ)is W(x, y, r)for the unique r∈[0,1] that is represented by ˜ λ. In (W3) we do not have to write 1−˜ λinstead of 1−λsince, by the properties (ii),(iii) above, ] 1−λ=R1−˜ λand so WX(x, y, 1−λ) =XWX(x, y, ] 1−λ) =XWX(x, y, 1−˜ λ), where the second equality follows from (W2) since - by (ii),(iii)-λ1=Rλ2→˜ λ1=R˜ λ2. Next we add new constants cκof type N→Nand Nκof type Ntogether with the following axioms (here we write for better readability the real number κrepresented by cκrather than cκitself; note that all the operations used such as √·, π, sin,cos and the field operations on Rcan be explicitly written on the level of representatives of the respective reals and cκby primitive recursive terms, see [9]): (κ1) κ≥R1 Nκ+ 1, i.e. Nκis a witness for the strict positivity of κ > 0, (κ2) ∀xX, yXdX(x, y)≤Rπ 2√κ, which expresses that diam(X)≤π/(2√κ), (κ3)                ∀aX, bX, pX, qX∀nNdX(a, p), dX(b, q)>R1 n+1 → cos(√κdX(p,q))+cos(√κdX(a,p)) cos(√κdX(b,q)) sin(√κdX(a,p)) sin(√κdX(b,q)) −cos(√κdX(a,p))+cos(√κdX(b,p))cos(√κdX(b,q))+cos(√κdX(a,q)) 1+cos(√κdX(a,b)sin(√κdX(a,p)) sin(√κdX(b,q)) ≤R1, 3 which expresses that Xsatisfies the ‘upper four point κ-quadrilateral cos-condition cosqκ’ (see [2]). Let us briefly notice that we can indeed define the quotients used in the axioms (κ2),(κ3) by simple primitive recursive terms in the data: one can easily define a primitive recursive term t:NN×N→NNsuch that t(xNN, n) represents the reciprocal 1/rxof the real number rxrepresented by xprovided that rx≥1 n+1.Such a lower bound on the denominator ‘2√κ’ occurring in (κ2) can easily be obtained from Nκin axiom (κ1),e.g. we may take n:= dNκ/2e.For (κ3) we have to additionally observe that by (κ1),(κ2) the function sin is only applied to arguments x∈[√κ/(n+ 1), π/2] ⊂[√κ/(n+ 1),2] and that sin x≥x/3 for such xso that sin x≥√κ/(3(n+ 1)). Definition 2.3. We define the theory Aω[X, d, W, CAT(κ)] as the theory that results if we add to the theory Aω[X, d]from [10] (p.99) constants WX, cκand Nκof type X×X×NN→ X, N→Nand Nrespectively together with the axioms (W1),(W2),(W3),(W5), (κ1), (κ2) and (κ3). Remark 2.4. The extra constant bXof type Ntogether with the axiom (iv)(4) ∀xX, yX(dX(x, y)≤R(bX)R) used in [10] to express that (X, d)is bounded by bXis now actually redundant (and so officially dropped from Aω[X, d, W, CAT(κ)]) since, by (κ1),(κ2), bXcan be defined in terms of Nκ. Proposition 2.5. Let (X, d)be a metric space, W:X×X×[0,1] →Xbe a mapping, κ∈(0,∞)and Nκ∈N.The full set-theoretic type structure Sω,X is a model of Aω[X, d, W, CAT(κ)] (in the sense of the interpretation as defined in [11] extended - for κ > 0and Nκ∈Nby the interpretation of [cκ]Sω,X := (κ)◦and [Nκ]Sω,X := Nκ) iff (X, d)is a CAT(κ)-space with κ≥1/(Nκ+ 1) and diam(X)≤π/(2√κ)and Wis defined in terms of the unique geodesic segment in Xjoining given points x, y and rλ∈[0,1]. Proof: ‘⇒’: Let (X, d), W, κ, Nκbe such that Sω,X satisfies the axioms listed above. By (W1),(W2), clearly (X, d) is geodesically connected with γ: [0, d(x, y)] →X, γ(α) := W(x, y, α/d(x, y)) for x6=y. Moreover, the axioms (κ1),(κ2) imply that κ≥1/(Nκ+ 1) and diam(X)≤ π/(2√κ).(κ3) implies that (X, d) satisfies the ‘upper four point cosqκcondition’. Hence by Theorem 1.1 in [2], (X, d) is a CAT(κ)-space. ‘⇐’: Let (X, d) be a CAT(κ)-space with κ≥1/(Nκ+ 1) and diam(X)≤π/(2√κ) and let W(x, y, λ) := γ(λ·d(x, y)) for the unique geodesic γ: [0, d(x, y)] →Xjoining x, y. Then the axioms (κ1),(κ2) are satisfied (with the interpretation of the constant cκand Nκ as specified in the proposition) and (X, d) is uniquely geodesic which implies that the WX defined in terms of this unique geodesic satisfies (W2),(W3). Moreover, since for any x0∈X 4 the function x7→ d(x, x0) is convex (see Ex.2.3 in [3], p.176), (W1) also holds. Again by Theorem 1.1 in [2] one has that (X, d) satisfies the ‘upper four point cosqκcondition’ so that axiom (κ3) holds. (W5) follows from Lemma 4.1 in [14] (see also [15]).  One crucial restriction for the logical metatheorems referred to in the introduction to hold is that instead of a full extensionality axiom, which for the type Xwould be ∀fX→X∀xX, yX(x=Xy→f(x) =Xf(y)), one only has a rule which allows one to infer that f(t) =Xf(s) from a proof that t=Xs. Since x=Xyis defined as dX(x, y) =R0,the very conclusion of such a metatheorem when applied to the extensionality of fwould imply a uniform quantitative form of that extensionality which is nothing else but the uniform continuity of f. Note that in the modeltheoretic approach to metric structures as in continuous or positive bounded logic, the uniform continuity of the functions in question is a basic assumption (see, however, the recent paper [4] which relaxes this) while this is not necessary in the proof-theoretic context (see [11, 13] for extensive discussions of this issue). In our current situation, we do have sufficient uniform continuity of WXas a consequence of its axioms to be able to derive full extensionality: Proposition 2.6. Aω[X, d, W, CAT(κ)] proves the extensionality of WX,i.e. ∀λ1 1, λ1 2, xX 1, xX 2, yX 1, yX 2(λ1=Rλ2∧x1=Xx2∧y1=Xy2→WX(x1, y1, λ1) =XW(x2, y2, λ2)). Proof: By Lemma 4.25.6) in [11], λ1=Rλ2implies that ˜ λ1=R˜ λ2and so by (W2) WX(x1, y1, λ1) =XWX(x1, y1, λ2). By (W5), x1=Xx2implies WX(x1, y1, λ2) =XWX(x2, y1, λ2). Using (W3) and again (W5), y1=Xy2yields WX(x2, y1, λ2) =XWX(x2, y2, λ2). The transitivity of =Xnow implies that WX(x1, y1, λ1) =XWX(x2, y2, λ2).  Proposition 2.7. [cκ]Sω,X = (κ)◦is majorized by c∗ κ(n) := j(b·2n+2,2n+1 −1),where b∈N is such that b≥κ. Proof: See Lemma 17.8 in [11].  Remark 2.8. By rescaling one usually can reduce things to the case of κ= 1 in which we may simply interpret cκby (1R)◦and and Nκby 0. 5 Definition 2.9 ([10]).We say that a finite type ρover the base types Nand Xhas degree 1 if ρ=N→. . . →N(including ρ=N). ρhas degree (N, X) if ρ=N→. . . →N→X (including ρ=X). A type ρhas degree (1, X) if it has the form τ1→. . . →τk→X (including ρ=X), where τihas degree 1 or (N, X). Definition 2.10 ([10]).A formula Fis called ∀-formula (resp. ∃-formula) if it has the form F≡ ∀aσFqf (a) (resp. F≡ ∃aσFqf (a)) where Fqf does not contain any quantifier and the types in σare of degree 1 or (1, X). One can now easily adapt the proof of the main logical metatheorem for bounded metric, W-hyperbolic and CAT(0)-spaces from Theorem 3.7 in [10] to the case of CAT(κ)-spaces for κ > 0 : Theorem 2.11. Let σ, ρ be types of degree 1 and τbe a type of degree (1, X). Let sσ→ρbe a closed term of Aω[X, d, W, CAT(κ)] and B∀(xσ, yρ, zτ, uN) (C∃(xσ, yρ, zτ, vN)) be a ∀-formula containing only x, y, z, u free (resp. a ∃-formula containing only x, y, z, v free). If ∀xσ∀y≤ρs(x)∀zτ∀uNB∀(x, y, z, u)→ ∃vNC∃(x, y, z, v) is provable in Aω[X, d, W, CAT(κ)], then one can extract a computable functional Φ : Sσ×N×N→Nsuch that for all x∈ Sσ1all b, N ∈N ∀y≤ρs(x)∀zτ∀u≤Φ(x, b, N)B∀(x, y, z, u)→ ∃v≤Φ(x, b, N)C∃(x, y, z, v) holds in any (non-empty) CAT(κ)-space (X, d) with 1/(N+ 1) ≤κ≤band diam(X)≤ π/(2√κ) (with Nκbeing interpreted by N). The computational complexity of Φ can be estimated in terms of the strength of the Aωprinciple instances actually used in the proof (see Remark 2.12 below). Instead of single variables x, y, z, u, v we may also have finite tuples of variables x, y, z, u, v as long as the elements of the respective tuples satisfy the same type restrictions as x, y, z, u, v. Moreover, instead of a single premise of the form ‘∀uNB∀(x, y, z, u)’ we may have a finite conjunction of such premises. Proof: We only have to augment the proof from Theorem 3.7 in [10] by the following observations (together with Remark 2.4): 1. The new axioms (W5),(κ1),(κ2) and (κ3) are all (logically equivalent to) purely universal sentences, where the quantified variables are of the types N,N→Nor X for which the full set-theoretic model Sω,X and the model of strongly majorizable functionals Mω,X coincide. For (κ3) note that the premise ‘. . . >R1/(n+ 1)’ is purely existential so that the whole expression ‘. . . ’ prenexes into a purely universal formula. 2. [cκ]Mω,X := [cκ]Sω,X := (κ)◦is majorized by the simple function c∗ κwhose definition only uses b. [Nκ]Mω,X := [Nκ]Sω,X := Nis trivially majorized by itself. 1Note that S0=Nand Sσis the set of all functions Nk→Nfor σbeing the type of k-ary number theoretic functions. 6  Remark 2.12. 1. The proof of Theorem 2.11 actually provides an extraction algorithm for Φ. The functional Φcan always be defined in the calculus T+BR of so-called bar recursive functionals, where Trefers to G¨odel’s primitive recursive functionals Tand BR refers to Spector’s schema of bar recursion. However, for concrete proofs usually only small fragments of Aω[X, d, W, CAT (κ)] (corresponding to fragments of Aω) will be needed to formalize the proof guaranteeing bounds of much lower complexity (see Remark 3.8 in [10] and the references given there as well as [11]). 2. It is well-known that any CAT(κ)-space is also a CAT(κ0)-space for all κ0≥κ(see e.g. [3][Theorem 1.12(1)]). So to be CAT(κ) for a κ > 0that is very close to 0(resulting in a large bound Nκ) is a better condition than being CAT(κ)for a κthat is larger while the fact that our bound will depend on Nκdoes not seem to be in line with this. However, one has to note that the condition diam(X)≤π/(2√κ)on the diameter of Xbecomes the more liberal the smaller κis and a uniform bound extraction theorem in the generality of Theorem 2.11 does require (already in the CAT(0)-case) that X is bounded (see [10][Theorem 3.7]; for the unbounded case, treated in [6][Theorem 4.10], one needs extra conditions on zto guarentee the majorizability of z) and the bound has to depend on an upper bound on diam(X).So assume now that we have aB-bounded CAT(κ)-space X. Then Xis also a CAT(κ0)-space for κ0:= (π/2B)2 satisfying diam(X)≤π/(2√κ0)provided that κ≤κ0and we can apply the extracted bound with Nκ0being any natural number such that 1/(Nκ0+ 1) ≤(π/2B)2no matter how small κ > 0was (and with b≥κ0). In the case where κ≥κ0we can take Nκ:= Nκ0in the bound and may use any b≥κ. The most common definition of CAT(κ)-spaces is via an inequality for comparison triangles and so it would be beneficial for the purpose of mining proofs based on this property to have direct access to it (rather than having to go through the proof in [2] that it is implied by the upper four point cosqκcondition). Let us consider one version of such a characterization (given in Proposition 1.7.(2) in [3], p.161): let x1, x2, x3∈Xand consider a comparison triangle ∆(x1, x2, x3) in M2 κ,i.e. x1, x2, x3∈S2(here S2denotes the unit sphere in R3) with (+) d(xi, xj) = dM2 κ(xi, xj),where dM2 κ(xi, xj) = 1 √κarccos(hxi, xji), for i, j ∈ {1,2,3}.Then (++) ∀t∈[0,1] d(x1,(1 −t)x2+tx3)≤dM2 κ(x1,(1 −t)x2+tx3). Unfortunately, due to the universal quantifier hidden in the premise d(xi, xj) = dM2 κ(xi, xj) this characterization ‘(+) →(++)’ is not universal but prenexes into the form ∀∃.So in order to bring it into a purely universal form we have to see that it in fact implies already a seemingly stronger quantitative form where ∀∃-is realized by an explicit function (definable in our system). We will now show that this can be done in a highly uniform way: one 7 can define a function δ:N→Nsuch that any 1/(δ(k) + 1)-comparison triangle, i.e. (for i, j ∈ {1,2,3}) (+)kd(xi, xj)−dM2 κ(xi, xj)<1 δ(k)+1 satisfies (++) up to the error 1/(k+ 1),i.e. (++)k∀t∈[0,1] d(x1,(1 −t)x2+tx3)≤dM2 κ(x1,(1 −t)x2+tx3) + 1 k+ 1. Now (W6) ∀x1, x2, x3∈X∀x1, x2, x3∈S2∀k∈N(+)k→(++)k, where (1 −t)x2+tx3is to be understood as WX(x2, x3, t),is (equivalent to) a purely universal statement and so can be added simply as an axiom to our formal system. Here we wrote things for simplicity in normal mathematical laguage but (W6) can easily be formalized using WX, dXas before while quantification over S2can be reduced to R3(and hence in turn to quantification over triples of objects of type 1) without introducing the purely universal premise ‘hx, xi= 1’ by writing instead of ‘∀x∈S2Φ(x)’ ∀x∈R3(kxkE>1 2→Φ(bx)), where bx:= x/ max{1/2,||x||E}.With Φ also then Φ0(x) := kxkE>1 2→Φ(bx) is (equivalent to) a purely universal formula since >Ris existential. Clearly, the quantitative form (W6) immediately implies back the original characterization from [3]. The existence of such a uniform bound δin fact in itself is an instance of the logical metatheorem on uniform bound extractions when applied to a proof of the characterization given in [3] from the different one due to [2] used further above. Remark 2.13. To have (W6) - and hence the qualitative inequality - stated for the specific geodesic selected by Wimplies already (given the condition on the diameter being ≤π/(2√κ)< π/√κ) that Xis uniquely geodesic so that to state (W6) w.r.t. Wimplies the seemingly stronger version for arbitrary geodesics: suppose x, y are joined by two geodesic segments and let m1and m2be the respective midpoints. Apply the comparison inequality for the triangles ∆(x, m1, m2)and ∆(y, m1, m2)(having a geodesic segment selected by W for each edge in these triangles). Then, if mis a midpoint of m1and m2one gets (if m16=m2) d(x, m)≤d(x, m)< d(x, m1) = d(x, m1). Applying the same argument in ∆(y, m1, m2)gives d(x, y)≤d(x, m) + d(y, m)< d(x, y) and hence a contradiction. 8 Definition 2.14. Let (X, d)be a CAT(κ)-space with κ > 0and diam(X)≤π/(2√κ). Take x1, x2, x3∈X. Having δ > 0, a δ-comparison triangle for ∆(x1, x2, x3)is a triangle ∆(x1, x2, x3)in M2 κsuch that d(xi, xj)−dM2 κ(xi, xj)≤δ √κfor i, j ∈ {1,2,3}. Proposition 2.15. In the setting of Definition 2.14, for every ε∈(0,1) there exists δ:= ε2 108 sin ε2 36 such that for every δ-comparison triangle ∆(x1, x2, x3)we have that ∀t∈[0,1] d(x1,(1 −t)x2+tx3)≤dM2 κ(x1,(1 −t)x2+tx3) + ε √κ. Proof: We give the proof for κ= 1 (the general case follows by a simple rescaling). For ∆(x1, x2, x3), let ∆(x1, x2, x3) and ∆(fx1,fx2,fx3) be a δ-comparison triangle and a comparison triangle, respectively. Fix t∈[0,1] and denote a=dS2(x1, x2), b =dS2(x1, x3), c =dS2(x2, x3), m =dS2(x1,(1 −t)x2+tx3), and ea=dS2(fx1,fx2),e b=dS2(fx1,fx3),ec=dS2(fx2,fx3),em=dS2(fx1,(1 −t)fx2+tfx3). Then |cos a−cos ea|≤|a−ea| ≤ δ,|cos b−cose b|≤|b−e b| ≤ δand |cos c−cos ec| ≤ |c−ec| ≤ δ. Note that if em≤m, then d(x1,(1−t)x2+tx3)≤em≤m. Thus, we assume in the following that em > m, so cos em < cos m. Denote ε0=ε2/18. Then δ= (ε0/6) sin(ε0/2). Suppose first that c≥ε0/2. By Lemma 3.1 in [2], cos m=sin((1 −t)c) sin ccos a+sin(tc) sin ccos b(1) and cos em=sin((1 −t)ec) sin eccos ea+sin(tec) sin eccose b. (2) The function f: (0, π)→R,f(x) = sin(tx)/sin xis increasing. Since c≤ec+δ, we obtain that sin(tc) sin c≤sin(t(ec+δ)) sin(ec+δ)=sin(tec) cos(tδ) + cos(tec) sin(tδ) sin(ec+δ)<sin(tec) sin(ec+δ)+δ sin(ec+δ). Note that ε0/2≤c≤ec+δ≤π/2 + δ < π −ε0/2, so δ sin(ec+δ)<δ sin(ε0/2) =ε0 6. At the same time, sin(ec+δ)≥cos δsin ec≥(1 −δ) sin ecand 1 −δ≥sin(ε0/2), so sin(tec) sin(ec+δ0)≤sin(tec) sin ec 1 1−δ=sin(tec) sin ec1 + δ 1−δ≤sin(tec) sin ec+δ 1−δ ≤sin(tec) sin ec+δ sin(ε0/2) =sin(tec) sin ec+ε0 6. 9