Relative entropy

import Random_variable

/-- relative entropy -/
def discrimination (q₁ₙ q₂ₙ : (ℕ → ι) → ℝ) [rnd_var n q₁ₙ] [rnd_var n q₂ₙ] : ℝ :=
∑ k, (q₁ₙ k) * (log(q₁ₙ k) - log(q₂ₙ k))

variables
(q₁ₙ q₂ₙ : (ℕ → ι) → ℝ) (q₁ q₂ : ι → ℝ)
[rnd_var n q₁ₙ] [rnd_var n q₂ₙ] [rnd_var 1 q₁] [rnd_var 1 q₂]

lemma discrimination_additive_of_iid [iid q₁ₙ q₁] [iid q₂ₙ q₂] :
discrimination q₁ₙ q₂ₙ = n * discrimination q₁ q₂ :=
begin
  calc discrimination q₁ₙ q₂ₙ = ∑ kₙ, (qₙ₁ kₙ) * (log(qₙ₁ kₙ) - log(qₙ₂ kₙ)) : by rw discrimination
                         ... = ∑ kₙ, (Π n, (q₁ (kₙ n))) * ∑ n, (log(q₁ (kₙ n)) - log(q₂ (kₙ n))) : by rw log_iid_rw
                         ... = n * discrimination q₁ q₂ : by sorry,
end

-- "The ratio log((q₁ k) / (q₂ k)) is a random variable."

lemma discrimination_zero_of_eq :
q₁ = q₂ → discrimination q₁ q₂ = 0 :=
begin
  intro,
  -- log 1 = 0
  sorry,
end

lemma discrimination_pos_iff_unequal :
discrimination q₁ q₂ > 0 ↔ q₁ ≠ q₂ := sorry

/-- convex with respect to each argument -/
lemma discrimination_convex :
convex discrimination := sorry

References