Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions

Pischke, Nicholas

doi:10.1090/tran/9226

Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions
HTML articles powered by AMS MathViewer

by Nicholas Pischke;

Trans. Amer. Math. Soc. 377 (2024), 7475-7517

DOI: https://doi.org/10.1090/tran/9226

Published electronically: August 16, 2024

HTML | PDF | Request permission

Abstract:

We present a proof-theoretically tame approach for treating the dual space of an abstract Banach space in systems amenable to proof mining metatheorems which quantify and allow for the extraction of the computational content of large classes of theorems about the dual of a Banach space and its corresponding norm, unlocking a major branch of functional analysis as a new area of applications for these methods. The approach relies on using intensional methods to deal with the high quantifier complexity of the predicate defining the dual space as well as on a proof-theoretically tame treatment of suprema over (certain) bounded sets in normed spaces to deal with the norm of the dual. Beyond this, we discuss further possible extensions of this system to deal with convex functions and corresponding Fréchet derivatives and their duality theory through Fenchel conjugates, together with the associated Bregman distances, which provide the logical basis for a range of recent applications of proof mining methods to these branches of nonlinear analysis.

References

Y. I. Alber, Metric and generalized projection operators in Banach spaces: properties and applications, Theory and applications of nonlinear operators of accretive and monotone type, Lecture Notes in Pure and Appl. Math., vol. 178, Dekker, New York, 1996, pp. 15–50. MR 1386667
Heinz H. Bauschke and Jonathan M. Borwein, Legendre functions and the method of random Bregman projections, J. Convex Anal. 4 (1997), no. 1, 27–67. MR 1459881
Heinz H. Bauschke, Jonathan M. Borwein, and Patrick L. Combettes, Essential smoothness, essential strict convexity, and Legendre functions in Banach spaces, Commun. Contemp. Math. 3 (2001), no. 4, 615–647. MR 1869107, DOI 10.1142/S0219199701000524
Heinz H. Bauschke, Jonathan M. Borwein, and Patrick L. Combettes, Bregman monotone optimization algorithms, SIAM J. Control Optim. 42 (2003), no. 2, 596–636. MR 1982285, DOI 10.1137/S0363012902407120
Heinz H. Bauschke and Patrick L. Combettes, Convex analysis and monotone operator theory in Hilbert spaces, 2nd ed., CMS Books in Mathematics/Ouvrages de Mathématiques de la SMC, Springer, Cham, 2017. With a foreword by Hédy Attouch. MR 3616647, DOI 10.1007/978-3-319-48311-5
Heinz H. Bauschke and Adrian S. Lewis, Dykstra’s algorithm with Bregman projections: a convergence proof, Optimization 48 (2000), no. 4, 409–427. MR 1811866, DOI 10.1080/02331930008844513
Marc Bezem, Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, J. Symbolic Logic 50 (1985), no. 3, 652–660. MR 805674, DOI 10.2307/2274319
J. Borwein, A. J. Guirao, P. Hájek, and J. Vanderwerff, Uniformly convex functions on Banach spaces, Proc. Amer. Math. Soc. 137 (2009), no. 3, 1081–1091. MR 2457450, DOI 10.1090/S0002-9939-08-09630-5
Jonathan M. Borwein and Jon Vanderwerff, Fréchet-Legendre functions and reflexive Banach spaces, J. Convex Anal. 17 (2010), no. 3-4, 915–924. MR 2731284
L. M. Bregman, The relaxation method for finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics, 7:200–217, 1967.
A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat. Fys. Medd. Danske Vid. Selsk. 34 (1964).
A. Brøndsted and R. T. Rockafellar, On the subdifferentiability of convex functions, Proc. Amer. Math. Soc. 16 (1965), 605–611. MR 178103, DOI 10.1090/S0002-9939-1965-0178103-8
Felix E. Browder, Nonlinear monotone operators and convex sets in Banach spaces, Bull. Amer. Math. Soc. 71 (1965), 780–785. MR 180882, DOI 10.1090/S0002-9904-1965-11391-X
Felix E. Browder, Nonlinear maximal monotone operators in Banach space, Math. Ann. 175 (1968), 89–113. MR 223942, DOI 10.1007/BF01418765
Regina S. Burachik, Minh N. Dao, and Scott B. Lindstrom, The generalized Bregman distance, SIAM J. Optim. 31 (2021), no. 1, 404–424. MR 4207185, DOI 10.1137/19M1288140
D. Butnariu and A. N. Iusem, Totally Convex Functions for Fixed Points Computation and Infinite Dimensional Optimization, volume 40 of Applied Optimization. Springer Dordrecht, 2000.
Dan Butnariu, Alfredo N. Iusem, and Constantin Zălinescu, On uniform convexity, total convexity and convergence of the proximal point and outer Bregman projection algorithms in Banach spaces, J. Convex Anal. 10 (2003), no. 1, 35–61. MR 1999901
Dan Butnariu and Elena Resmerita, Bregman distances, totally convex functions, and a method for solving operator equations in Banach spaces, Abstr. Appl. Anal. , posted on (2006), Art. ID 84919, 39. MR 2211675, DOI 10.1155/AAA/2006/84919
Yair Censor and Tommy Elfving, A multiprojection algorithm using Bregman projections in a product space, Numer. Algorithms 8 (1994), no. 2-4, 221–239. MR 1309222, DOI 10.1007/BF02142692
Yair Censor and Simeon Reich, The Dykstra algorithm with Bregman projections, Commun. Appl. Anal. 2 (1998), no. 3, 407–419. MR 1626725
Joseph Diestel, Geometry of Banach spaces—selected topics, Lecture Notes in Mathematics, Vol. 485, Springer-Verlag, Berlin-New York, 1975. MR 461094, DOI 10.1007/BFb0082079
W. Fenchel, On conjugate convex functions, Canad. J. Math. 1 (1949), 73–77. MR 28365, DOI 10.4153/cjm-1949-007-x
Fernando Ferreira, Laurenţiu Leuştean, and Pedro Pinto, On the removal of weak compactness arguments in proof mining, Adv. Math. 354 (2019), 106728, 55. MR 3985505, DOI 10.1016/j.aim.2019.106728
Fernando Ferreira and Paulo Oliva, Bounded functional interpretation, Ann. Pure Appl. Logic 135 (2005), no. 1-3, 73–112. MR 2156133, DOI 10.1016/j.apal.2004.11.001
Philipp Gerhardy and Ulrich Kohlenbach, General logical metatheorems for functional analysis, Trans. Amer. Math. Soc. 360 (2008), no. 5, 2615–2660. MR 2373327, DOI 10.1090/S0002-9947-07-04429-7
Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12 (1958), 280–287 (German, with English summary). MR 102482, DOI 10.1111/j.1746-8361.1958.tb01464.x
Daniel Günzel and Ulrich Kohlenbach, Logical metatheorems for abstract spaces axiomatized in positive bounded logic, Adv. Math. 290 (2016), 503–551. MR 3451931, DOI 10.1016/j.aim.2015.12.007
David Hilbert, Über das Unendliche, Math. Ann. 95 (1926), no. 1, 161–190 (German). MR 1512272, DOI 10.1007/BF01206605
W. A. Howard, Appendix: Hereditarily majorizable function of finite type, Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Math., Vol. 344, Springer, Berlin-New York, 1973, pp. 454–461. MR 469712
Robert C. James, Reflexivity and the supremum of linear functionals, Ann. of Math. (2) 66 (1957), 159–169. MR 90019, DOI 10.2307/1970122
Shoji Kamimura, Fumiaki Kohsaka, and Wataru Takahashi, Weak and strong convergence theorems for maximal monotone operators in a Banach space, Set-Valued Anal. 12 (2004), no. 4, 417–429. MR 2112848, DOI 10.1007/s11228-004-8196-4
Ulrich Kohlenbach, Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization, J. Symbolic Logic 57 (1992), no. 4, 1239–1273. MR 1195271, DOI 10.2307/2275367
Ulrich Kohlenbach, Pointwise hereditary majorization and some applications, Arch. Math. Logic 31 (1992), no. 4, 227–241. MR 1155034, DOI 10.1007/BF01794980
Ulrich Kohlenbach, Analysing proofs in analysis, Logic: from foundations to applications (Staffordshire, 1993) Oxford Sci. Publ., Oxford Univ. Press, New York, 1996, pp. 225–260. MR 1428007
Ulrich Kohlenbach, Arithmetizing proofs in analysis, Logic Colloquium ’96 (San Sebastián), Lecture Notes Logic, vol. 12, Springer, Berlin, 1998, pp. 115–158. MR 1674949, DOI 10.1007/978-3-662-22110-5_{5}
Ulrich Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 (2005), no. 1, 89–128. MR 2098088, DOI 10.1090/S0002-9947-04-03515-9
U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008. MR 2445721
Ulrich Kohlenbach, Proof-theoretic methods in nonlinear analysis, Proceedings of the International Congress of Mathematicians—Rio de Janeiro 2018. Vol. II. Invited lectures, World Sci. Publ., Hackensack, NJ, 2018, pp. 61–82. MR 3966757
Ulrich Kohlenbach, Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness, Kreisel’s interests—on the foundations of logic and mathematics, Tributes, vol. 41, Coll. Publ., [London], [2020] ©2020, pp. 45–61. MR 4241040
U. Kohlenbach and L. Leuştean, On the computational content of convergence proofs via Banach limits, Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci. 370 (2012), no. 1971, 3449–3463. MR 2943215, DOI 10.1098/rsta.2011.0329
U. Kohlenbach and A. Nicolae, A proof-theoretic bound extraction theorem for CAT$(\kappa )$-spaces, Studia Logica 105 (2017), no. 3, 611–624. MR 3650519, DOI 10.1007/s11225-016-9702-z
U. Kohlenbach and P. Oliva, Proof mining: a systematic way of analyzing proofs in mathematics, Tr. Mat. Inst. Steklova 242 (2003), no. Mat. Logika i Algebra, 147–175; English transl., Proc. Steklov Inst. Math. 3(242) (2003), 136–164. MR 2054493
Ulrich Kohlenbach and Nicholas Pischke, Proof theory and non-smooth analysis, Philos. Trans. Roy. Soc. A 381 (2023), no. 2248, Paper No. 20220015 , 21. MR 4590513
Fumiaki Kohsaka and Wataru Takahashi, Strong convergence of an iterative sequence for maximal monotone operators in a Banach space, Abstr. Appl. Anal. 3 (2004), 239–249. MR 2058504, DOI 10.1155/S1085337504309036
G. Kreisel, On the interpretation of non-finitist proofs. I, J. Symbolic Logic 16 (1951), 241–267. MR 49135, DOI 10.2307/2267908
G. Kreisel, On the interpretation of non-finitist proofs. II. Interpretation of number theory. Applications, J. Symbolic Logic 17 (1952), 43–58. MR 51193, DOI 10.2307/2267457
Georg Kreisel, Interpretation of analysis by means of constructive functionals of finite types, Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam, 1957 (edited by A. Heyting), Stud. Logic Found. Math., North-Holland, Amsterdam, 1959, pp. 101–128. MR 106838
Sigekatu Kuroda, Intuitionistische Untersuchungen der formalistischen Logik, Nagoya Math. J. 2 (1951), 35–47 (German). MR 41801, DOI 10.1017/S0027763000010023
Laurenţiu Leuştean, Proof mining in $\Bbb R$-trees and hyperbolic spaces, Proceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006), Electron. Notes Theor. Comput. Sci., vol. 165, Elsevier Sci. B. V., Amsterdam, 2006, pp. 95–106. MR 2321766, DOI 10.1016/j.entcs.2006.05.039
Laurenţiu Leuştean, An application of proof mining to nonlinear iterations, Ann. Pure Appl. Logic 165 (2014), no. 9, 1484–1500. MR 3210080, DOI 10.1016/j.apal.2014.04.015
Angus Macintyre, The mathematical significance of proof theory, Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci. 363 (2005), no. 1835, 2419–2435. MR 2197658, DOI 10.1098/rsta.2005.1656
Angus Macintyre, The impact of Gödel’s incompleteness theorems on mathematics, Kurt Gödel and the foundations of mathematics, Cambridge Univ. Press, Cambridge, 2011, pp. 3–25. MR 2866863
V. Martín-Márquez, S. Reich, and S. Sabach, Iterative methods for approximating fixed points of Bregman nonexpansive operators, Discrete and Continuous Dynamical Systems-Series S, 6(4):1043–1063, 2013.
Victoria Martín-Márquez, Simeon Reich, and Shoham Sabach, Bregman strongly nonexpansive operators in reflexive Banach spaces, J. Math. Anal. Appl. 400 (2013), no. 2, 597–614. MR 3004990, DOI 10.1016/j.jmaa.2012.11.059
Liviu Păunescu and Andrei Sipoş, A proof-theoretic metatheorem for tracial von Neumann algebras, MLQ Math. Log. Q. 69 (2023), no. 1, 63–76. MR 4606448, DOI 10.1002/malq.202200048
N. Pischke, A proof-theoretic metatheorem for nonlinear semigroups generated by an accretive operator and applications, E-print, arXiv:2304.01723 [math.LO], 2023.
N. Pischke, Generalized Fejér monotone sequences and their finitary content, Optimization, to appear. DOI 10.1080/02331934.2024.2390114
Nicholas Pischke, Logical metatheorems for accretive and (generalized) monotone set-valued operators, J. Math. Log. 24 (2024), no. 2, Paper No. 2350008, 59. MR 4741735, DOI 10.1142/S0219061323500083
N. Pischke, Proof-theoretical aspects of nonlinear and set-valued analysis, Ph.D. Thesis, TU Darmstadt, 2024, https://tuprints.ulb.tu-darmstadt.de/26584/.
N. Pischke and U. Kohlenbach, Effective rates for iterations involving Bregman strongly nonexpansive operators, 2024, Submitted, https://sites.google.com/view/nicholaspischke/notes-and-papers.
Simeon Reich and Shoham Sabach, A strong convergence theorem for a proximal-type algorithm in reflexive Banach spaces, J. Nonlinear Convex Anal. 10 (2009), no. 3, 471–485. MR 2588944
R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966), 497–510. MR 193549, DOI 10.2140/pjm.1966.17.497
R. T. Rockafellar, Level sets and continuity of conjugate convex functions, Trans. Amer. Math. Soc. 123 (1966), 46–63. MR 192318, DOI 10.1090/S0002-9947-1966-0192318-X
R. Tyrrell Rockafellar, Convex analysis, Princeton Mathematical Series, No. 28, Princeton University Press, Princeton, NJ, 1970. MR 274683, DOI 10.1515/9781400873173
R. Tyrrell Rockafellar and Roger J.-B. Wets, Variational analysis, Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 317, Springer-Verlag, Berlin, 1998. MR 1491362, DOI 10.1007/978-3-642-02431-3
Walter Rudin, Functional analysis, 2nd ed., International Series in Pure and Applied Mathematics, McGraw-Hill, Inc., New York, 1991. MR 1157815
H. H. Schaefer and M. P. Wolff, Topological vector spaces, 2nd ed., Graduate Texts in Mathematics, vol. 3, Springer-Verlag, New York, 1999. MR 1741419, DOI 10.1007/978-1-4612-1468-7
Yekini Shehu, Convergence results of forward-backward algorithms for sum of monotone operators in Banach spaces, Results Math. 74 (2019), no. 4, Paper No. 138, 24. MR 3978049, DOI 10.1007/s00025-019-1061-4
Andrei Sipoş, Proof mining in $L^p$ spaces, J. Symb. Log. 84 (2019), no. 4, 1612–1629. MR 4045991, DOI 10.1017/jsl.2019.55
Clifford Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Proc. Sympos. Pure Math., Vol. V, Amer. Math. Soc., Providence, RI, 1962, pp. 1–27. MR 154801
Wataru Takahashi, Nonlinear functional analysis, Yokohama Publishers, Yokohama, 2000. Fixed point theory and its applications. MR 1864294
A.S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer, Berlin, 1973.
C. Zălinescu, Convex analysis in general vector spaces, World Scientific Publishing Co., Inc., River Edge, NJ, 2002. MR 1921556, DOI 10.1142/9789812777096
Habtu Zegeye, Strong convergence theorems for maximal monotone mappings in Banach spaces, J. Math. Anal. Appl. 343 (2008), no. 2, 663–671. MR 2401524, DOI 10.1016/j.jmaa.2008.01.076