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,13 @@
+# Finite probability theory
+
+```agda
+module finite-probability-theory where
+
+open import finite-probability-theory.atomic-real-random-variables-finite-probability-spaces public
+open import finite-probability-theory.constant-real-random-variables-finite-probability-spaces public
+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/atomic-real-random-variables-finite-probability-spaces.lagda.md

@@ -0,0 +1,59 @@
+# Atomic real random variables in finite probability spaces
+
+```agda
+module finite-probability-theory.atomic-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.real-random-variables-finite-probability-spaces
+
+open import foundation.coproduct-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.rational-real-numbers
+
+open import univalent-combinatorics.equality-finite-types
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "atomic real random variable" Disambiguation="in a finite probability space" Agda=atomic-real-random-variable-Finite-Probability-Space}}
+in a
+[finite probability space](finite-probability-theory.finite-probability-spaces.md)
+`(Ω , Pr)` at `e : Ω` is the
+[real random variable](finite-probability-theory.real-random-variables-finite-probability-spaces.md)
+`X : Ω → ℝ` such that:
+
+- `X e ＝ 1`;
+- `∀ (e' : Ω) (e' ≠ e) → X e ＝ 0`.
+
+## Definition
+
+### Atomic real random variables in a finite probability space
+
+```agda
+module _
+  {l1 l2 : Level} (Ω : Finite-Probability-Space l1 l2)
+  (e : type-Finite-Probability-Space Ω)
+  where
+
+  atomic-real-random-variable-Finite-Probability-Space :
+    real-random-variable-Finite-Probability-Space lzero Ω
+  atomic-real-random-variable-Finite-Probability-Space e' =
+    rec-coproduct
+      ( λ _ → one-ℝ)
+      ( λ _ → zero-ℝ)
+      ( has-decidable-equality-is-finite
+        ( is-finite-type-Finite-Probability-Space Ω)
+        ( e)
+        ( e'))
+```

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

@@ -0,0 +1,44 @@
+# Constnant real random variables in finite probability spaces
+
+```agda
+module finite-probability-theory.constant-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.real-random-variables-finite-probability-spaces
+
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+Any [real number](real-numbers.dedekind-real-numbers.md) `x` defines a
+{{#concept "constant real random variable" Disambiguation="in a finite probability space" Agda=const-real-random-variable-Finite-Probability-Space}}
+on any
+[finite probability space](finite-probability-theory.finite-probability-spaces.md)
+`Ω`: the
+[real random variable](finite-probability-theory.real-random-variables-finite-probability-spaces.md)
+`X : (e : Ω) ↦ x`.
+
+## Definitions
+
+### Constant random variables in a finite probability space
+
+```agda
+module _
+  {l1 l2 : Level} (Ω : Finite-Probability-Space l1 l2)
+  where
+
+  const-real-random-variable-Finite-Probability-Space :
+    (x : ℝ l2) → real-random-variable-Finite-Probability-Space l2 Ω
+  const-real-random-variable-Finite-Probability-Space x _ = x
+```

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

@@ -0,0 +1,81 @@
+# 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 commutative-algebra.sums-of-finite-families-of-elements-commutative-rings
+
+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 real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.large-ring-of-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](commutative-algebra.sums-of-finite-families-of-elements-commutative-rings.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 _
+  {l1 l2 l3 : Level} (Ω : Finite-Probability-Space l1 l2)
+  (X : real-random-variable-Finite-Probability-Space l3 Ω)
+  where
+
+  expected-value-real-random-variable-Finite-Probability-Space : ℝ (l2 ⊔ l3)
+  expected-value-real-random-variable-Finite-Probability-Space =
+    sum-finite-Commutative-Ring
+      ( commutative-ring-ℝ (l2 ⊔ l3))
+      ( 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,150 @@
+# 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 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Finite-Probability-Space l1 l2 =
+  Σ ( Finite-Type l1)
+    ( probability-distribution-Finite-Type l2)
+
+module _
+  {l1 l2 : Level} (Ω : Finite-Probability-Space l1 l2)
+  where
+
+  finite-type-Finite-Probability-Space : Finite-Type l1
+  finite-type-Finite-Probability-Space = pr1 Ω
+
+  type-Finite-Probability-Space : UU l1
+  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 l2 finite-type-Finite-Probability-Space
+  distribution-Finite-Probability-Space = pr1 (pr2 Ω)
+
+  real-distribution-Finite-Probability-Space :
+    type-Finite-Probability-Space → ℝ l2
+  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)) ＝
+    ( raise-one-ℝ l2)
+  eq-one-total-measure-distribution-Finite-Probability-Space = pr2 (pr2 Ω)
+```
+
+## Properties
+
+### A finite probability space is nonempty
+
+```agda
+module _
+  {l1 l2 : Level} (Ω : Finite-Probability-Space l1 l2)
+  where
+
+  is-nonempty-type-Finite-Probability-Space :
+    is-nonempty (type-Finite-Probability-Space Ω)
+  is-nonempty-type-Finite-Probability-Space H =
+    neq-raise-zero-one-ℝ l2
+      ( ( 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 _
+  {l1 l2 : Level} (Ω : Finite-Probability-Space l1 l2)
+  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 l1
+  inhabited-type-Finite-Probability-Space =
+    ( type-Finite-Probability-Space Ω ,
+      is-inhabited-type-Finite-Probability-Space)
+
+  inhabited-finite-type-Finite-Probability-Space : Inhabited-Finite-Type l1
+  inhabited-finite-type-Finite-Probability-Space =
+    ( finite-type-Finite-Probability-Space Ω ,
+      is-inhabited-type-Finite-Probability-Space)
+```
+
+## References
+
+{{#bibliography}}