Basics of finite probability theory

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-random-real-variables-finite-probability-spaces public
+open import finite-probability-theory.finite-probability-spaces public
+open import finite-probability-theory.measures-on-finite-types public
+open import finite-probability-theory.probability-measures-on-finite-types public
+open import finite-probability-theory.random-real-variables-finite-probability-spaces public
+```

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

@@ -0,0 +1,72 @@
+# Expected value of random real variables in finite probability spaces
+
+```agda
+module finite-probability-theory.expected-value-random-real-variables-finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.finite-probability-spaces
+open import finite-probability-theory.measures-on-finite-types
+open import finite-probability-theory.probability-measures-on-finite-types
+open import finite-probability-theory.random-real-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 random real variable in a finite probability space" Agda=expected-value-random-real-variable-Finite-Probability-Space}}
+of a
+[random real variable](finite-probability-theory.random-real-variables-finite-probability-spaces.md)
+`X` in a
+[finite probability space](finite-probability-theory.finite-probability-spaces.md)
+`(Ω , μ)` is the
+[sum](group-theory.sums-of-finite-families-of-elements-abelian-groups.md)
+
+\[ ∑\_{x ∈ Ω} X(x)μ(x). \]
+
+## Definitions
+
+### Expected value of a random real variable in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  (X : random-real-variable-Finite-Probability-Space Ω)
+  where
+
+  expected-value-random-real-variable-Finite-Probability-Space : ℝ lzero
+  expected-value-random-real-variable-Finite-Probability-Space =
+    sum-finite-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( finite-type-Finite-Probability-Space Ω)
+      ( λ x →
+        mul-ℝ
+          ( X x)
+          ( real-measure-Finite-Probability-Space Ω x))
+```

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

@@ -0,0 +1,123 @@
+# Finite probability spaces
+
+```agda
+module finite-probability-theory.finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.measures-on-finite-types
+open import finite-probability-theory.probability-measures-on-finite-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 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 real-numbers.strict-inequality-real-numbers
+
+open import univalent-combinatorics.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 measure](finite-probability-theory.probability-measures-on-finite-types.md).
+
+## Definitions
+
+### Finite probability spaces
+
+```agda
+Finite-Probability-Space : (l : Level) → UU (lsuc l)
+Finite-Probability-Space l =
+  Σ ( Finite-Type l)
+    ( probability-measure-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
+
+  measure-Finite-Probability-Space :
+    measure-Finite-Type finite-type-Finite-Probability-Space
+  measure-Finite-Probability-Space = pr1 (pr2 Ω)
+
+  real-measure-Finite-Probability-Space :
+    type-Finite-Probability-Space → ℝ lzero
+  real-measure-Finite-Probability-Space =
+    real-measure-Finite-Type
+      ( finite-type-Finite-Probability-Space)
+      ( measure-Finite-Probability-Space)
+
+  eq-one-total-measure-Finite-Probability-Space :
+    ( total-measure-Finite-Type
+      ( finite-type-Finite-Probability-Space)
+      ( measure-Finite-Probability-Space)) ＝
+    one-ℝ
+  eq-one-total-measure-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 =
+    not-0＝1 ∘ 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-is-empty-Finite-Type
+          ( finite-type-Finite-Probability-Space Ω)
+          ( measure-Finite-Probability-Space Ω)
+          ( H))) ∙
+      ( eq-one-total-measure-Finite-Probability-Space Ω)
+
+    not-0＝1 : is-empty (zero-ℝ ＝ one-ℝ)
+    not-0＝1 H =
+      irreflexive-le-ℝ
+        ( zero-ℝ)
+        ( inv-tr
+          ( le-ℝ zero-ℝ)
+          ( H)
+          ( is-positive-real-ℝ⁺ one-ℝ⁺))
+```

src/finite-probability-theory/measures-on-finite-types.lagda.md

@@ -0,0 +1,81 @@
+# Measures on finite types
+
+```agda
+module finite-probability-theory.measures-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 "measure" Disambiguation="on a finite type" Agda=measure-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).
+
+The **total measure** of a measure `μ` on a finite type `Ω` is the
+[sum](group-theory.sums-of-finite-families-of-elements-abelian-groups.md)
+
+\[ ∑\_{x ∈ Ω} μ(x). \]
+
+## Definition
+
+### Measures on finite types
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  where
+
+  measure-Finite-Type : UU (lsuc lzero ⊔ l)
+  measure-Finite-Type = type-Finite-Type Ω → ℝ⁺ lzero
+
+  real-measure-Finite-Type :
+    measure-Finite-Type → type-Finite-Type Ω → ℝ lzero
+  real-measure-Finite-Type μ = real-ℝ⁺ ∘ μ
+
+  total-measure-Finite-Type : measure-Finite-Type → ℝ lzero
+  total-measure-Finite-Type μ =
+    sum-finite-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( Ω)
+      ( real-ℝ⁺ ∘ μ)
+```
+
+## Properties
+
+### The total measure of an empty type is zero
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l) (μ : measure-Finite-Type Ω)
+  where
+
+  is-zero-total-measure-is-empty-Finite-Type :
+    is-empty (type-Finite-Type Ω) →
+    total-measure-Finite-Type Ω μ ＝ zero-ℝ
+  is-zero-total-measure-is-empty-Finite-Type H =
+    eq-zero-sum-finite-is-empty-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( Ω)
+      ( H)
+      ( real-ℝ⁺ ∘ μ)
+```

src/finite-probability-theory/probability-measures-on-finite-types.lagda.md

@@ -0,0 +1,77 @@
+# Probability measures on finite types
+
+```agda
+module finite-probability-theory.probability-measures-on-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.measures-on-finite-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.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 "probability measure" Disambiguation="on a finite type" Agda=probability-measure-Finite-Type}}
+on a [finite type](univalent-combinatorics.finite-types.md) is a
+[measure](finite-probability-theory.measures-on-finite-types.md) with **total
+measure** equal to 1.
+
+## Definition
+
+### The property of being a probability measure on a finite type
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l) (μ : measure-Finite-Type Ω)
+  where
+
+  is-probability-measure-prop-measure-Finite-Type : Prop (lsuc lzero)
+  is-probability-measure-prop-measure-Finite-Type =
+    Id-Prop
+      ( ℝ-Set lzero)
+      ( total-measure-Finite-Type Ω μ)
+      ( one-ℝ)
+
+  is-probability-measure-Finite-Type : UU (lsuc lzero)
+  is-probability-measure-Finite-Type =
+    type-Prop is-probability-measure-prop-measure-Finite-Type
+
+  is-prop-is-probability-measure-Finite-Type :
+    is-prop is-probability-measure-Finite-Type
+  is-prop-is-probability-measure-Finite-Type =
+    is-prop-type-Prop is-probability-measure-prop-measure-Finite-Type
+```
+
+### Probability measures on finite types
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  where
+
+  probability-measure-Finite-Type : UU (lsuc lzero ⊔ l)
+  probability-measure-Finite-Type =
+    type-subtype (is-probability-measure-prop-measure-Finite-Type Ω)
+```