Probability Theory: Computer Science & IT Book Chapter | IGI Global

×

Receive a 20% Discount on All Purchases Directly Through IGI Global's Online Bookstore.
Additionally, libraries can receive an extra 5% discount. Learn More

Subscribe to the latest research through IGI Global's new InfoSci-OnDemand Plus

InfoSci®-OnDemand Plus, a subscription-based service, provides researchers the ability to access full-text content from over 100,000 peer-reviewed book chapters and 26,000+ scholarly journal articles covering 11 core subjects. Users can select articles or chapters that meet their interests and gain access to the full content permanently in their personal online InfoSci-OnDemand Plus library.

Purchase the Encyclopedia of Information Science and Technology, Fourth Edition and Receive Complimentary E-Books of Previous Editions

When ordering directly through IGI Global's Online Bookstore, receive the complimentary e-books for the first, second, and third editions with the purchase of the Encyclopedia of Information Science and Technology, Fourth Edition e-book.

Create a Free IGI Global Library Account to Receive a 25% Discount on All Purchases

Exclusive benefits include one-click shopping, flexible payment options, free COUNTER 4 and MARC records, and a 25% discount on all titles as well as the award-winning InfoSci^{®}-Databases.

InfoSci^{®}-Journals Annual Subscription Price for New Customers: As Low As US$ 5,100

This collection of over 175 e-journals offers unlimited access to highly-cited, forward-thinking content in full-text PDF and HTML with no DRM. There are no platform or maintenance fees and a guarantee of no more than 5% increase annually.

Hasan, Osman and Sofiène Tahar. "Probability Theory." Formalized Probability Theory and Applications Using Theorem Proving. IGI Global, 2015. 47-64. Web. 23 Sep. 2018. doi:10.4018/978-1-4666-8315-0.ch005

APA

Hasan, O., & Tahar, S. (2015). Probability Theory. In Formalized Probability Theory and Applications Using Theorem Proving (pp. 47-64). Hershey, PA: IGI Global. doi:10.4018/978-1-4666-8315-0.ch005

Chicago

Hasan, Osman and Sofiène Tahar. "Probability Theory." In Formalized Probability Theory and Applications Using Theorem Proving, 47-64 (2015), accessed September 23, 2018. doi:10.4018/978-1-4666-8315-0.ch005

In this chapter, the authors make use of the formalizations of measure theory and Lebesgue integration in HOL4 to provide a higher-order-logic formalization of probability theory (Mhamdi, 2013). For illustration purposes, they also present the probabilistic analysis of the Heavy Hitter problem using HOL.

The classical approach to define the probability of an event A is p (A) = N_{A} / N, where N_{A} is the number of outcomes favorable to the event A and N is the number of all possible outcomes of the experiment. However, this approach is based on the assumptions that all outcomes are equally likely (equiprobable) and that the number of possible outcomes is finite. These assumptions are not always true and thus the above-mentioned classical definition has a limited scope.

Kolmogorov introduced the axiomatic definition of probability, which overcomes the above-mentioned problem and provides a mathematically consistent way for assigning and deducing probabilities of events. This approach consists in defining a set of all possible outcomes, Ω, called the sample space, a set F of events which are subsets of Ω and a probability measure p such that (Ω, F, p) is a measure space with p (Ω) = 1. Now, (Ω, F, p) is a probability space if it is a measure space and p (Ω) = 1.

Definition 5.1

Ⱶ∀p. prob_space p measure_space p Ʌ (measure p (p_space p) = 1)

A probability measure is a measure function and an event is a measurable set.

Two events A and B are independent iff p (A ∩ B) = p (A) p (B).

Definition 5.2

Ⱶ ∀p a b. indep p a b a events p Ʌb events p Ʌprob p (a b) = prob p a * prob p b
X:Ω → R is a random variable iff X is (F, B (R)) measurable

Definition 5.3

Ⱶ∀ X p s. random_variable X p s prob_space p ɅX measurable (p_space p,events p) s

In this book, we focus on real-valued random variables but the definition can be adapted for random variables having values on any topological space thanks to the general definition of the Borel sigma algebra.

All the properties, presented in the previous chapter, for measurable functions are obviously valid for random variables.

Theorem 5.1

If X and Y are random variables and c ϵ R then the following functions are also random variables: cX, | X |, X^{n,} X + Y, XY and max (X, Y).
Two random variables X and Y are independent iff ∀A, B ϵ B (R), the events { X ϵ A } and { Y ϵ B } are independent. The set { X ϵ A } denotes the set of outcomes ω for which X(ω) ϵ A. In other words{ X ϵ A } = X^{-1}(A).