Random variable

/-- prob of a sequence of n symbols -/
class rnd_var (n : ℕ) (qₙ : (ℕ → ι) → ℝ) :=
(probs_nonneg  : ∀ s, qₙ s ≥ 0)
(sum_probs_one : ∑ s, qₙ s = 1)

/-- prob of a sequence of 1 symbol -/
class rnd_var_1 (p : ι → ℝ) :=
(probs_nonneg  : ∀ i, p i ≥ 0)
(sum_probs_one : ∑ i, p i = 1)

/-- rnd_var is n_rnd_var for sequences with 1 symbol -/
-- lemma n_rnd_var_to_rnd_var_of_len_1 : ... := sorry

/-- independently and identically distributed -/
def iid (qₙ : (ℕ → ι) → ℝ) [rnd_var n qₙ] (q : ι → ℝ) [rnd_var 1 q] :=
∀ kₙ, qₙ kₙ = ∏ᶠ n, q (kₙ n)

/-- alternative def? -/
def iid' (qₙ : (ℕ → ι) → ℝ) [rnd_var n qₙ] :=
∃ (q : ι → ℝ), qₙ kₙ = Πᶠ i, q (kₙ i)

variables {kₙ : ℕ → ι}
{qₙ : (ℕ → ι) → ℝ} [rnd_var qₙ]
{q : ι → ℝ} [rnd_var_1 q]

lemma iid_rw [iid qₙ q] :
qₙ kₙ = Π n, (q (kₙ n)) := sorry

lemma log_iid_rw [iid qₙ q] :
log(qₙ kₙ) = ∑ n, log(q (kₙ n)) := sorry

write adapter to

Probability measure;

• See generalization to measure theory;

• See generalization to Category theory;