Classical channel $N(y|x)$ and its action $Np$, $Nq$ (Corollary 10.7.2)

import Definitions.Def_WildeQIT_FinDist

/-!
Wilde, *Quantum Information Theory* (2nd ed.), Corollary 10.7.2 (Monotonicity of relative
entropy): a classical channel is a conditional probability distribution `N(y|x)`; it acts on a
probability distribution `p` by `(Np)(y) = ∑_x N(y|x) p(x)` and on a vector `q` by
`(Nq)(y) = ∑_x N(y|x) q(x)`.
-/

namespace WildeQIT

/-- A classical channel from `α` to `β`: for every input letter `x`, a probability distribution
`N x` over output letters, so that `(N x).prob y` is `N(y|x)`. -/
abbrev Channel (α β : Type) [Fintype β] := α → FinDist β

namespace Channel

variable {α β : Type} [Fintype α] [Fintype β]

/-- The output distribution `Np`, `(Np)(y) = ∑_x N(y|x) p(x)`. -/
noncomputable def apply (N : Channel α β) (p : FinDist α) : FinDist β where
  prob y := ∑ x, (N x).prob y * p.prob x
  nonneg y := Finset.sum_nonneg fun x _ => mul_nonneg ((N x).nonneg y) (p.nonneg x)
  sum_eq_one := by
    rw [Finset.sum_comm]
    simp_rw [← Finset.sum_mul, (N _).sum_eq_one, one_mul]
    exact p.sum_eq_one

/-- The action on an arbitrary vector `q : α → ℝ`: `(Nq)(y) = ∑_x N(y|x) q(x)`. -/
noncomputable def applyFun (N : Channel α β) (q : α → ℝ) : β → ℝ :=
  fun y => ∑ x, (N x).prob y * q x

@[simp] theorem apply_prob (N : Channel α β) (p : FinDist α) (y : β) :
    (N.apply p).prob y = ∑ x, (N x).prob y * p.prob x := rfl

@[simp] theorem applyFun_apply (N : Channel α β) (q : α → ℝ) (y : β) :
    N.applyFun q y = ∑ x, (N x).prob y * q x := rfl

end Channel

end WildeQIT