Basics of finite probability theory

references.bib

@@ -101,6 +101,14 @@ @misc{Awodey22
   keywords      = {Mathematics - Category Theory, Mathematics - Logic},
 }
 
+@misc{Babai00,
+  title         = {Finite Probablity Spaces},
+  author        = {Babai, L\'aszl\'o},
+  year          = 2000,
+  month         = apr,
+  url           = {https://people.cs.uchicago.edu/~laci/reu02/prob.pdf},
+}
+
 @article{BauerTaylor2009,
   title         = {The {{Dedekind}} Reals in Abstract {{Stone}} Duality},
   author        = {Bauer, Andrej and Taylor, Paul},

src/finite-probability-theory.lagda.md

@@ -0,0 +1,11 @@
+# Finite probability theory
+
+```agda
+module finite-probability-theory where
+
+open import finite-probability-theory.expected-value-real-random-variables-finite-probability-spaces public
+open import finite-probability-theory.finite-probability-spaces public
+open import finite-probability-theory.positive-distributions-on-finite-types public
+open import finite-probability-theory.probability-distributions-on-finite-types public
+open import finite-probability-theory.real-random-variables-finite-probability-spaces public
+```

src/finite-probability-theory/expected-value-real-random-variables-finite-probability-spaces.lagda.md

@@ -0,0 +1,80 @@
+# Expected value of real random variables in finite probability spaces
+
+```agda
+module finite-probability-theory.expected-value-real-random-variables-finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.finite-probability-spaces
+open import finite-probability-theory.positive-distributions-on-finite-types
+open import finite-probability-theory.probability-distributions-on-finite-types
+open import finite-probability-theory.real-random-variables-finite-probability-spaces
+
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "expected value" Disambiguation="of a real random variable in a finite probability space" Agda=expected-value-real-random-variable-Finite-Probability-Space}}
+of a
+[real random variable](finite-probability-theory.real-random-variables-finite-probability-spaces.md)
+`X` in a
+[finite probability space](finite-probability-theory.finite-probability-spaces.md)
+`(Ω , Pr)` is the
+[sum](group-theory.sums-of-finite-families-of-elements-abelian-groups.md)
+
+$$
+  ∑_{x ∈ Ω} X(x)\operatorname{Pr}(x).
+$$
+
+Our definition follows Definition 2.2 of {{#cite Babai00}}.
+
+## Definitions
+
+### Expected value of a real random variable in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  (X : real-random-variable-Finite-Probability-Space Ω)
+  where
+
+  expected-value-real-random-variable-Finite-Probability-Space : ℝ lzero
+  expected-value-real-random-variable-Finite-Probability-Space =
+    sum-finite-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( finite-type-Finite-Probability-Space Ω)
+      ( λ x →
+        mul-ℝ
+          ( X x)
+          ( real-distribution-Finite-Probability-Space Ω x))
+```
+
+## References
+
+{{#bibliography}}

src/finite-probability-theory/finite-probability-spaces.lagda.md

@@ -0,0 +1,157 @@
+# Finite probability spaces
+
+```agda
+module finite-probability-theory.finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.positive-distributions-on-finite-types
+open import finite-probability-theory.probability-distributions-on-finite-types
+
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import logic.propositional-double-negation-elimination
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.apartness-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.inhabited-finite-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "finite probability space" Agda=Finite-Probability-Space}} is a
+[finite type](univalent-combinatorics.finite-types.md) equipped with a
+[probability distribution](finite-probability-theory.probability-distributions-on-finite-types.md).
+
+Any finite probability space is [inhabited](foundation.inhabited-types.md).
+
+Our definitions follows {{#cite Babai00}}, except, there it is assumed that the
+underlying type is [nonempty](foundation-core.empty-types.md), but this follows
+from the condition of having
+[total measure](finite-probability-theory.positive-distributions-on-finite-types.md)
+equal to 1.
+
+## Definitions
+
+### Finite probability spaces
+
+```agda
+Finite-Probability-Space : (l : Level) → UU (lsuc l)
+Finite-Probability-Space l =
+  Σ ( Finite-Type l)
+    ( probability-distribution-Finite-Type)
+
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  finite-type-Finite-Probability-Space : Finite-Type l
+  finite-type-Finite-Probability-Space = pr1 Ω
+
+  type-Finite-Probability-Space : UU l
+  type-Finite-Probability-Space =
+    type-Finite-Type finite-type-Finite-Probability-Space
+
+  is-finite-type-Finite-Probability-Space :
+    is-finite type-Finite-Probability-Space
+  is-finite-type-Finite-Probability-Space =
+    is-finite-type-Finite-Type finite-type-Finite-Probability-Space
+
+  distribution-Finite-Probability-Space :
+    positive-distribution-Finite-Type finite-type-Finite-Probability-Space
+  distribution-Finite-Probability-Space = pr1 (pr2 Ω)
+
+  real-distribution-Finite-Probability-Space :
+    type-Finite-Probability-Space → ℝ lzero
+  real-distribution-Finite-Probability-Space =
+    real-positive-distribution-Finite-Type
+      ( finite-type-Finite-Probability-Space)
+      ( distribution-Finite-Probability-Space)
+
+  eq-one-total-measure-distribution-Finite-Probability-Space :
+    ( total-measure-positive-distribution-Finite-Type
+      ( finite-type-Finite-Probability-Space)
+      ( distribution-Finite-Probability-Space)) ＝
+    one-ℝ
+  eq-one-total-measure-distribution-Finite-Probability-Space =
+    pr2 (pr2 Ω)
+```
+
+## Properties
+
+### A finite probability space is nonempty
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  is-nonempty-type-Finite-Probability-Space :
+    is-nonempty (type-Finite-Probability-Space Ω)
+  is-nonempty-type-Finite-Probability-Space =
+    zero-is-not-one-ℝ ∘ absurd-is-empty-Finite-Probability-Space
+    where
+
+    absurd-is-empty-Finite-Probability-Space :
+      is-empty (type-Finite-Probability-Space Ω) →
+      zero-ℝ ＝ one-ℝ
+    absurd-is-empty-Finite-Probability-Space H =
+      ( inv
+        ( is-zero-total-measure-positive-distribution-is-empty-Finite-Type
+          ( finite-type-Finite-Probability-Space Ω)
+          ( distribution-Finite-Probability-Space Ω)
+          ( H))) ∙
+      ( eq-one-total-measure-distribution-Finite-Probability-Space Ω)
+```
+
+### A finite probability space is inhabited
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  is-inhabited-type-Finite-Probability-Space :
+    is-inhabited (type-Finite-Probability-Space Ω)
+  is-inhabited-type-Finite-Probability-Space =
+    prop-double-negation-elim-is-inhabited-or-empty
+      ( is-inhabited-or-empty-is-finite
+        ( is-finite-type-Finite-Probability-Space Ω))
+      ( is-nonempty-type-Finite-Probability-Space Ω)
+
+  inhabited-type-Finite-Probability-Space : Inhabited-Type l
+  inhabited-type-Finite-Probability-Space =
+    ( type-Finite-Probability-Space Ω ,
+      is-inhabited-type-Finite-Probability-Space)
+
+  inhabited-finite-type-Finite-Probability-Space : Inhabited-Finite-Type l
+  inhabited-finite-type-Finite-Probability-Space =
+    ( finite-type-Finite-Probability-Space Ω ,
+      is-inhabited-type-Finite-Probability-Space)
+```
+
+## References
+
+{{#bibliography}}

src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md

@@ -0,0 +1,95 @@
+# Positive distributions on finite types
+
+```agda
+module finite-probability-theory.positive-distributions-on-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "positive distribution" Disambiguation="on a finite type" Agda=positive-distribution-Finite-Type}}
+on a [finite type](univalent-combinatorics.finite-types.md) `Ω` is a function
+into the [positive real numbers](real-numbers.positive-real-numbers.md),
+`Pr : Ω → ℝ⁺`. We interpret the type `Ω` as the collection of _atomic events_,
+and `Pr(x)` as the (unnormalized) _probability_ that the atomic event `x` will
+occur. Note that for positive distributions no atomic event can be _impossible_
+since `Pr(x)` is always strictly greater than `0`. The **total measure** of a
+positive distribution `Pr` on a finite type `Ω` is the
+[sum](group-theory.sums-of-finite-families-of-elements-abelian-groups.md)
+
+$$
+  ∑_{x ∈ Ω}\operatorname{Pr}(x).
+$$
+
+## Definitions
+
+### Positive distributions on finite types
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  where
+
+  positive-distribution-Finite-Type : UU (lsuc lzero ⊔ l)
+  positive-distribution-Finite-Type = type-Finite-Type Ω → ℝ⁺ lzero
+
+  real-positive-distribution-Finite-Type :
+    positive-distribution-Finite-Type → type-Finite-Type Ω → ℝ lzero
+  real-positive-distribution-Finite-Type Pr = real-ℝ⁺ ∘ Pr
+```
+
+### The total measure of a positive distribution on a finite type
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  (Pr : positive-distribution-Finite-Type Ω)
+  where
+
+  total-measure-positive-distribution-Finite-Type : ℝ lzero
+  total-measure-positive-distribution-Finite-Type =
+    sum-finite-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( Ω)
+      ( real-positive-distribution-Finite-Type Ω Pr)
+```
+
+## Properties
+
+### The total measure of a positive distribution on an empty type is zero
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l) (Pr : positive-distribution-Finite-Type Ω)
+  where
+
+  is-zero-total-measure-positive-distribution-is-empty-Finite-Type :
+    is-empty (type-Finite-Type Ω) →
+    total-measure-positive-distribution-Finite-Type Ω Pr ＝ zero-ℝ
+  is-zero-total-measure-positive-distribution-is-empty-Finite-Type H =
+    eq-zero-sum-finite-is-empty-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( Ω)
+      ( H)
+      ( real-positive-distribution-Finite-Type Ω Pr)
+```