×

Events of Borel sets, construction of Borel sets and random variables for stochastic finance. (English) Zbl 1311.28001

Summary: We consider special events of Borel sets with the aim to prove, that the set of the irrational numbers is an event of the Borel sets. The set of the natural numbers, the set of the integer numbers and the set of the rational numbers are countable, so we can use the literature [O. Forster, Analysis 1. Differential- und Integralrechnung einer Veränderlichen. 6., verb. Aufl. Braunschweig: Vieweg. 78–81 (2001; Zbl 1043.26500)] as a basis for the similar construction of the proof. Next we prove, that different sets can construct the Borel sets [A. Klenke, Wahrscheinlichkeitstheorie. Berlin: Springer. 9–10 (2006; Zbl 1103.60001)]. Literature [Klenke, loc. cit.] and [H.-O. Georgii, Stochastik. Einführung in die Wahrscheinlichkeitstheorie und Statistik. 2nd revised edition. Berlin: de Gruyter. 11–12 (2004; Zbl 1082.62002)] gives an overview, that there exists some other sets for this construction. Last we define special functions as random variables for stochastic finance in discrete time. The relevant functions are implemented in the article [P. Jaeger, Formaliz. Math. 20, No. 1, 1–5 (2012; Zbl 1276.91103), see [H. Föllmer and A. Schied, Stochastic finance. An introduction in discrete time. 2nd revised and extended ed. Berlin: de Gruyter. p. 4 (2004; Zbl 1126.91028)]. The aim is to construct events and random variables, which can easily be used with a probability measure. See as an example theorems (10) and (14) in [H. Okazaki and Y. Shidama, Formaliz. Math. 21, No. 1, 33–39 (2013; Zbl 1281.60006)]. Then the formalization is more similar to the presentation used in the book [Föllmer and Schied, loc. cit.]. As a background, further literatures is [S. Bosch, Lineare Algebra. 4th revised ed. Berlin: Springer. 9–12 (2008; Zbl 1141.15300)], [H. Heuser, Lehrbuch der Analysis. Teil 1. 15., durchgesehene Aufl. Stuttgart: Teubner. 17–20 (2003; Zbl 1011.26001)], and [G. Fischer, Lineare Algebra, 13th ed. Braunschweig, Wiesbaden: Vieweg. 32–35 (2002)].

MSC:

28A05 Classes of sets (Borel fields, \(\sigma\)-rings, etc.), measurable sets, Suslin sets, analytic sets
60A05 Axioms; other general questions in probability
91G99 Actuarial science and mathematical finance
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.; · Zbl 1364.68157
[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.;
[3] Siegfried Bosch. Lineare Algebra. Springer, Berlin, Heidelberg, 4 edition, 2008.; · Zbl 1141.15300
[4] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.;
[5] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.;
[6] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.;
[7] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.;
[8] Gerd Fischer. Lineare Algebra. Vieweg, Braunschweig, Wiesbaden, 13 edition, 2002.; · Zbl 0421.15002
[9] Hans F¨ollmer and Alexander Schied. Stochastic Finance: An Introduction in Discrete Time, volume 27 of Studies in Mathematics. de Gruyter, Berlin, 2nd edition, 2004.; · Zbl 1126.91028
[10] Otto Forster. Analysis 1. Vieweg-Verlag, Braunschweig/Wiesbaden, 6th edition, 2001.; · Zbl 1043.26500
[11] Hans-Otto Georgii. Stochastik, Einf¨uhrung in die Wahrscheinlichkeitstheorie und Statistik. deGruyter, Berlin, 2nd edition, 2004.; · Zbl 1082.62002
[12] Adam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3): 313-322, 2003.;
[13] Harro Heuser. Lehrbuch der Analysis. Teil 1. Teubner, Stuttgart, Leipzig, Wiesbaden, 15 edition, 2003.; · Zbl 1011.26001
[14] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1): 35-40, 1990.;
[15] Peter Jaeger. Elementary introduction to stochastic finance in discrete time. Formalized Mathematics, 20(1):1-5, 2012. doi:10.2478/v10037-012-0001-5.; · Zbl 1276.91103
[16] Achim Klenke. Wahrscheinlichkeitstheorie. Springer-Verlag, Berlin, Heidelberg, 2006.;
[17] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990.;
[18] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477-481, 1990.;
[19] Andrzej Nedzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401-407, 1990.;
[20] Hiroyuki Okazaki and Yasunari Shidama. Random variables and product of probability spaces. Formalized Mathematics, 21(1):33-39, 2013. doi:10.2478/forma-2013-0003.; · Zbl 1281.60006
[21] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.;
[22] Konrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213-216, 1991.;
[23] Konrad Raczkowski and Andrzej Nedzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991.;
[24] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777-780, 1990.;
[25] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003.;
[26] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1 (1):187-190, 1990.;
[27] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.;
[28] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.;
[29] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.;
[30] Bo Zhang, Hiroshi Yamazaki, and Yatsuka Nakamura. Set sequences and monotone class. Formalized Mathematics, 13(4):435-441, 2005.;
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.