Joint sample entropy and the jointly typical set (Definitions 14.5.1–14.5.3)
DefinitionWildeQIT_weakJointTypicalSetConsider independent realizations and of random variables and with joint distribution on , i.i.d. across positions: . A pair of sequences is represented as one sequence of pairs (Fin n → α × β), with component sequences seqFst, seqSnd.
Definition 14.5.1 (Joint sample entropy). .
Definition 14.5.2 (Jointly typical sequence). are -jointly typical if their joint sample entropy is -close to and both and are marginally -typical.
Definition 14.5.3 (Jointly typical set).
Formalization Note. jointSampleEntropy p z abbreviates sampleEntropy p z for the joint distribution p : FinDist (α × β); weakJointTypicalSet p n δ filters sequences of pairs by the three conditions, the marginal ones using weakTypicalSet p.fst and weakTypicalSet p.snd.
RETIRED (deprecated) 2026-09-07 03:35. Built on the retired WildeQIT_weakTypicalSet; replaced by WildeQIT_jointTypicalSet (WildeQIT.jointTypicalSet), which requires positive joint probability.
import Definitions.Def_WildeQIT_weakTypicalSet
/-!
Wilde, *Quantum Information Theory* (2nd ed.), Definitions 14.5.1–14.5.3 (Joint sample entropy,
jointly typical sequence, jointly typical set). For `n` independent realizations of the pair
`(X,Y)` with i.i.d. joint distribution `p_{XⁿYⁿ}(xⁿ,yⁿ) = ∏ᵢ p_{XY}(xᵢ,yᵢ)`, the joint sample
entropy is `H̄(xⁿ,yⁿ) = -(1/n) log p_{XⁿYⁿ}(xⁿ,yⁿ)`, and
`T_δ^{XⁿYⁿ} ≡ { (xⁿ,yⁿ) : |H̄(xⁿ,yⁿ) − H(X,Y)| ≤ δ, xⁿ ∈ T_δ^{Xⁿ}, yⁿ ∈ T_δ^{Yⁿ} }`.
A pair of sequences is represented as one sequence of pairs, `Fin n → α × β`.
-/
namespace WildeQIT
variable {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
/-- The sequence of first components `xⁿ` of a sequence of pairs. -/
def seqFst {n : ℕ} (z : Fin n → α × β) : Fin n → α := fun i => (z i).1
/-- The sequence of second components `yⁿ` of a sequence of pairs. -/
def seqSnd {n : ℕ} (z : Fin n → α × β) : Fin n → β := fun i => (z i).2
/-- Definition 14.5.1. The joint sample entropy `H̄(xⁿ,yⁿ) = -(1/n) log₂ ∏ᵢ p_{XY}(xᵢ,yᵢ)`,
i.e. the sample entropy of the pair sequence with respect to the joint distribution. -/
noncomputable abbrev jointSampleEntropy (p : FinDist (α × β)) {n : ℕ} (z : Fin n → α × β) : ℝ :=
sampleEntropy p z
/-- Definitions 14.5.2–14.5.3. The `δ`-jointly typical set `T_δ^{XⁿYⁿ}`: pairs of sequences whose
joint sample entropy is `δ`-close to `H(X,Y)` and whose components are each `δ`-typical. -/
noncomputable def weakJointTypicalSet (p : FinDist (α × β)) (n : ℕ) (δ : ℝ) : Finset (Fin n → α × β) :=
Finset.univ.filter fun z =>
|sampleEntropy p z - entropy p| ≤ δ ∧ seqFst z ∈ weakTypicalSet p.fst n δ ∧ seqSnd z ∈ weakTypicalSet p.snd n δ
theorem mem_weakJointTypicalSet {p : FinDist (α × β)} {n : ℕ} {δ : ℝ} {z : Fin n → α × β} :
z ∈ weakJointTypicalSet p n δ ↔
|sampleEntropy p z - entropy p| ≤ δ ∧ seqFst z ∈ weakTypicalSet p.fst n δ ∧ seqSnd z ∈ weakTypicalSet p.snd n δ := by
simp [weakJointTypicalSet]
end WildeQIT