http://hdl.handle.net/11320/3543 Mon, 01 Jun 2026 15:10:24 GMT 2026-06-01T15:10:24Z http://hdl.handle.net/11320/3578 Tytuł: Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables Autorzy: Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article we continue formalizing probability and randomness started in [13], where we formalized some theorems concerning the probability and real-valued random variables. In this paper we formalize the variance of a random variable and prove Chebyshev's inequality. Next we formalize the product probability measure on the Cartesian product of discrete spaces. In the final part of this article we define the algebra of real-valued random variables. Fri, 01 Jan 2010 00:00:00 GMT http://hdl.handle.net/11320/3578 2010-01-01T00:00:00Z http://hdl.handle.net/11320/3574 Tytuł: Sperner's Lemma Autorzy: Pąk, Karol Abstrakt: In this article we introduce and prove properties of simplicial complexes in real linear spaces which are necessary to formulate Sperner's lemma. The lemma states that for a function ƒ, which for an arbitrary vertex υ of the barycentric subdivision B of simplex K assigns some vertex from a face of K which contains υ, we can find a simplex S of B which satisfies ƒ(S) = K (see [10]). Fri, 01 Jan 2010 00:00:00 GMT http://hdl.handle.net/11320/3574 2010-01-01T00:00:00Z http://hdl.handle.net/11320/3575 Tytuł: Counting Derangements, Non Bijective Functions and the Birthday Problem Autorzy: Kaliszyk, Cezary Abstrakt: The article provides counting derangements of finite sets and counting non bijective functions. We provide a recursive formula for the number of derangements of a finite set, together with an explicit formula involving the number e. We count the number of non-one-to-one functions between to finite sets and perform a computation to give explicitely a formalization of the birthday problem. The article is an extension of [10]. Fri, 01 Jan 2010 00:00:00 GMT http://hdl.handle.net/11320/3575 2010-01-01T00:00:00Z http://hdl.handle.net/11320/3576 Tytuł: Riemann Integral of Functions R into C Autorzy: Miyajima, Keiichi; Kato, Takahiro; Shidama, Yasunari Abstrakt: In this article, we define the Riemann Integral on functions R into C and proof the linearity of this operator. Especially, the Riemann integral of complex functions is constituted by the redefinition about the Riemann sum of complex numbers. Our method refers to the [19]. Fri, 01 Jan 2010 00:00:00 GMT http://hdl.handle.net/11320/3576 2010-01-01T00:00:00Z