On a relationship between countable functionals and projective trees
On certain decompositions of Gödel numberings.
On changes of input/output coding. I.
On changes of input/output coding. II.
On computable real functions
On L 1 Space Formed by Complex-Valued Partial Functions
In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.
On L 1 Space Formed by Real-Valued Partial Functions
This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a function space, the so-called L1 space and proved that the space turns out to be a normed space. The formalization of a real function space was given in [16]. The set of all function forms additive group. Here addition is defined by point-wise addition of two functions. However it is not true for partial functions. The set of partial functions...
On L p Space Formed by Real-Valued Partial Functions
This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).