The Hahn-Banach theorem in type theory

1998 ◽  
Author(s):  
Jan Cederquist ◽  
Thierry Coquand
Keyword(s):  
Linear Functional ◽  
Constructive Proof ◽  
Normed Vector Space ◽  
Deductive Systems ◽  
Banach Theorem ◽  
Cover Relation ◽  
The Right ◽  
Proof By Induction ◽  
Normed Vector ◽  
Formal Topology

We present the basic concepts and definitions needed in a pointfree approach to functional analysis via formal topology. Our main results are the constructive proofs of localic formulations of the Alaoglu and Helly-Hahn-Banach theorems. Earlier pointfree formulations of the Hahn-Banach theorem, in a topos-theoretic setting, were presented by Mulvey and Pelletier (1987, 1991) and by Vermeulen (1986). A constructive proof based on points was given by Bishop (1967). In the formulation of his proof, the norm of the linear functional is preserved to an arbitrary degree by the extension and a counterexample shows that the norm, in general, is not preserved exactly. As usual in pointfree topology, our guideline is to define the objects under analysis as formal points of a suitable formal space. After this has been accomplished for the reals, we consider the formal topology ℒ(A) obtained as follows. To the formal space of mappings from a normed vector space A to the reals, we add the linearity and norm conditions in the form of covering axioms. The linear functional of norm ≤1 from A to the reals then correspond to the formal points of this formal topology. Given a subspace M of A, the classical Helly-Hahn-Banach theorem states that the restriction mapping from the linear functionals on A of norm ≤1 to those on M is surjective. In terms of covers, conceived as deductive systems, it becomes a conservativity statement (cf. Mulvey and Pelletier 1991): whenever a is an element and U is a subset of the base of the formal space ℒ(M) and we have a derivation in ℒ(A) of a ⊲ U, then we can find a derivation in ℒ(M) with the same conclusion. With this formulation it is quite natural to look for a proof by induction on covers. Moreover, as already pointed out by Mulvey and Pelletier (1991), it is possible to simplify the problem greatly, since it is enough to prove it for coherent spaces of which ℒ(A) and ℒ(M) are retracts. Then, in a derivation of a cover, we can assume that only finite subsets occur on the right-hand side of the cover relation.

The M-Space Theory of Tolerances

1990 ◽  
Author(s):  
Joshua U. Turner ◽  
Michael J. Wozny
Keyword(s):  
Vector Space ◽  
Mathematical Theory ◽  
Solid Modeling ◽  
Normed Vector Space ◽  
Space Theory ◽  
Modeling Technology ◽  
Geometric Tolerances ◽  
Normed Vector

Abstract A rigorous mathematical theory of tolerances is an important step toward the automated solution of tolerancing problems. This paper develops a mathematical theory of tolerances in which tolerance specifications are interpreted as constraints on a normed vector space of model variations (M-space). This M-space provides concise representations for both dimensional and geometric tolerances, without deviating from the established tolerancing standards. This paper extends the authors’ previous work to include examples of geometric orientation and form tolerances. We show that the M-space theory supports the development of effective algorithms for the solution of tolerancing problems. Through the use of solid modeling technology, it is possible to automate the solution of such problems.

scholarly journals On the stability of radical septic functional equations

Mathematics ◽  
2020 ◽  
Vol 8 (12) ◽  
pp. 2229
Author(s):  
Emanuel Guariglia ◽  
Kandhasamy Tamilvanan
Keyword(s):  
Functional Equation ◽  
Approximate Solution ◽  
Vector Space ◽  
Banach Spaces ◽  
Functional Equations ◽  
Normed Vector Space ◽  
Relevant Case ◽  
The Stability ◽  
Normed Vector ◽  
Stability Results

This paper deals with the approximate solution of the following functional equation fx7+y77=f(x)+f(y), where f is a mapping from R into a normed vector space. We show stability results of this equation in quasi-β-Banach spaces and (β,p)-Banach spaces. We also prove the nonstability of the previous functional equation in a relevant case.

scholarly journals Two fixed point theorems and invariant integrals

1974 ◽  
Vol 11 (1) ◽  
pp. 15-30 ◽  
Author(s):  
T.J. Cooper ◽  
J.H. Michael
Keyword(s):  
Fixed Point ◽  
Vector Space ◽  
Fixed Point Theorems ◽  
Normed Vector Space ◽  
Invariant Integrals ◽  
Lower Semi ◽  
Normed Vector

Two fixed point theorems for a subset C of a normed vector space X are established by using the concept of centre. These results differ from previous fixed point theorems in that X is assumed to have a topology T as well as a norm. The norm is required to be lower semi-continuous with respect to T and C is required to be convex, bounded with respect to the norm and compact with respect to T.

Uniform Domains and Uniform Domain Decomposition Property in Real Normed Vector Spaces

2013 ◽  
Vol 113 (1) ◽  
pp. 128 ◽  
Author(s):  
M. Huang ◽  
X. Wang
Keyword(s):  
Vector Space ◽  
Domain Decomposition ◽  
Vector Spaces ◽  
Uniform Domain ◽  
Normed Vector Space ◽  
Decomposition Property ◽  
Uniform Domains ◽  
Normed Vector

Let $E$ be a real normed vector space with $\dim(E)\geq 2$, $D$ a proper subdomain of $E$. In this paper we characterize uniform domains in $E$ in terms of the uniform domain decomposition property. In addition, we discuss the relation between quasiballs and domains with the quasiball decomposition property in $\mathsf{R}^n$.

A Hahn-Banach theorem for complex semifields

1970 ◽  
Vol 2 (1) ◽  
pp. 129-133
Author(s):  
Howard Anton ◽  
W.J. Pervin
Keyword(s):  
Linear Space ◽  
Linear Functional ◽  
Linear Extension ◽  
Banach Theorem

The following form of the Hahn-Banach theorem is proved: Let X be a linear space over the complex semifield E and let f: S → E be a linear functional defined on a subspace S of X. If p: X → RΔ is a seminorm with the property that ∣f(s)∣ ≪ p(s) for all s in S, then f has a linear extension F to X with the property that ∣F(x)∣ ≪ p(x) for all x in X.

Tychonoff's theorem in the framework of formal topologies

1997 ◽  
Vol 62 (4) ◽  
pp. 1315-1332 ◽  
Author(s):  
Sara Negri ◽  
Silvio Valentini
Keyword(s):  
Type Theory ◽  
Constructive Proof ◽  
Topological Product ◽  
Essential Difference ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Definition Of ◽  
The Axiom Of Choice ◽  
Inductive Property ◽  
Formal Topology

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.

Measures under the flat norm as ordered normed vector space

Positivity ◽  
2017 ◽  
Vol 22 (1) ◽  
pp. 105-138
Author(s):  
Piotr Gwiazda ◽  
Anna Marciniak-Czochra ◽  
Horst R. Thieme
Keyword(s):  
Vector Space ◽  
Normed Vector Space ◽  
Flat Norm ◽  
Normed Vector

scholarly journals Order-Lipschitz mappings restricted with linear bounded mappings in normed vector spaces without normalities of involving cones via methods of upper and lower solutions

Filomat ◽  
2018 ◽  
Vol 32 (19) ◽  
pp. 6691-6698
Author(s):  
Shujun Jiang ◽  
Zhilong Li
Keyword(s):  
Fixed Point ◽  
Existence Result ◽  
Fixed Point Theorems ◽  
Upper And Lower Solutions ◽  
Vector Spaces ◽  
Normed Vector Space ◽  
Unique Existence ◽  
Lipschitz Mappings ◽  
Normed Vector

In this paper, without assuming the normalities of cones, we prove some new fixed point theorems of order-Lipschitz mappings restricted with linear bounded mappings in normed vector space in the framework of w-convergence via the method of upper and lower solutions. It is worth mentioning that the unique existence result of fixed points in this paper, presents a characterization of Picard-completeness of order-Lipschitz mappings.

scholarly journals The Joly topology and the Mosco-Beer topology revisited

1993 ◽  
Vol 48 (3) ◽  
pp. 353-363 ◽  
Author(s):  
Dominique Azé ◽  
Jean-Paul Penot
Keyword(s):  
Vector Space ◽  
Convex Functions ◽  
Normed Vector Space ◽  
Fenchel Transform ◽  
Proper Convex ◽  
Normed Vector

Some extensions to the non reflexive case of continuity results for the Legendre-Fenchel transform are presented following an approach due to J.-L. Joly. We compare the topology introduced by J.-L. Joly and the Mosco-Beer topology introduced by G. Beer. In particular, in the case of the space of closed proper convex functions defined on the dual of a normed vector space they coincide.

scholarly journals A remark on continuous bilinear mappings

1971 ◽  
Vol 17 (3) ◽  
pp. 245-248 ◽  
Author(s):  
J. W. Baker ◽  
J. S. Pym
Keyword(s):  
Vector Space ◽  
Banach Algebra ◽  
Dimensional Subspace ◽  
Real Field ◽  
Normed Vector Space ◽  
Normed Algebra ◽  
One Dimensional ◽  
Bilinear Mapping ◽  
Second Dual ◽  
Normed Vector

The main theorem of this paper is a little involved (though the proof is straightforward using a well-known idea) but the immediate corollaries are interesting. For example, take a complex normed vector space A which is also a normed algebra with identity under each of two multiplications * and ∘. Then these multiplications coincide if and only if there exists α such that ‖a ∘ b ‖ ≦ α ‖ a * b ‖ for a, b in A. This is a condition for the two Arens multiplications on the second dual of a Banach algebra to be identical. By taking * to be the multiplication of a Banach algebra and ∘ to be its opposite, we obtain the condition for commutativity given in (3). Other applications are concerned with conditions under which a bilinear mapping between two algebras is a homomorphism, when an element lies in the centre of an algebra, and a one-dimensional subspace of an algebra is a right ideal. An example shows that the theorem is false for algebras over the real field, but Theorem 2 gives the parallel result in this case.

Sign in / Sign up

Export Citation Format

Share Document