http://hdl.handle.net/11320/3543 2026-06-01T19:13:54Z 2026-06-01T19:13:54Z Okazaki, Hiroyuki Shidama, Yasunari http://hdl.handle.net/11320/3578 2017-10-05T22:54:23Z 2010-01-01T00:00:00Z

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.

2010-01-01T00:00:00Z Pąk, Karol http://hdl.handle.net/11320/3574 2017-10-05T22:57:04Z 2010-01-01T00:00:00Z

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]).

2010-01-01T00:00:00Z Kaliszyk, Cezary http://hdl.handle.net/11320/3575 2017-10-05T22:57:23Z 2010-01-01T00:00:00Z

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].

2010-01-01T00:00:00Z Miyajima, Keiichi Kato, Takahiro Shidama, Yasunari http://hdl.handle.net/11320/3576 2017-10-05T22:54:22Z 2010-01-01T00:00:00Z

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].

2010-01-01T00:00:00Z