One-shot channel simulation

StructureFinite joint law#✓fully proved

A finite joint law consists of positive integers \(n_X\) and \(n_Y\) and a probability distribution on \(\{0, \dots, n_X - 1\} \times \{0, \dots, n_Y - 1\}\).

structure FiniteJointLaw where
  nx : ℕ
  ny : ℕ
  nx_pos : 0 < nx
  ny_pos : 0 < ny
  law : PMF (Fin nx × Fin ny)

Used by 26

Used byMutual information between the input and the auxiliary · Auxiliary marginal of an extension · Conditional entropy of the output given the auxiliary · Conditional entropy vanishes for a one-letter output · Conditional-prefix optimum of a joint law · The conditional-prefix optimum vanishes for a one-letter output · Each admissible extension bounds the conditional-prefix optimum · The worst-case optimum dominates each conditional-prefix optimum · Finite extension of a joint law · Uniform outer constant for channel simulation · Input-auxiliary law · Input marginal of the input-auxiliary law · Auxiliary marginal of the input-auxiliary law · Input law · Mutual information · Output-auxiliary law · Output marginal of the output-auxiliary law · Auxiliary marginal of the output-auxiliary law · Conditional entropy of the output given the input and the auxiliary · Zero output entropy given input and auxiliary for a one-letter output · Output law · Trivial extension · The trivial extension has zero auxiliary information · Auxiliary law of the trivial extension · Conditional entropy in the trivial extension · Worst-case conditional-prefix optimum

DefinitionInput law#✓fully proved

The input law of a finite joint law \(p\) on \(\{0, \dots, n_X - 1\} \times \{0, \dots, n_Y - 1\}\) is its first marginal: the law on \(\{0, \dots, n_X - 1\}\) that is the image of \(p\) under \((x, y) \mapsto x\).

noncomputable def FiniteJointLaw.inputLaw (p : FiniteJointLaw) : PMF (Fin p.nx) :=
  p.law.map Prod.fst

Uses 1 · Used by 4

Statement usesFinite joint law

Used byMutual information between the input and the auxiliary · Input marginal of the input-auxiliary law · Mutual information · The trivial extension has zero auxiliary information

DefinitionOutput law#✓fully proved

The output law of a finite joint law \(p\) of an input \(X\) and an output \(Y\) is the law of \(Y\): the marginal of \(p\) on the output alphabet, obtained by pushing \(p\) forward along the projection onto the second coordinate.

noncomputable def FiniteJointLaw.outputLaw (p : FiniteJointLaw) : PMF (Fin p.ny) :=
  p.law.map Prod.snd

Uses 1 · Used by 3

Statement usesFinite joint law

Used byMutual information · Output marginal of the output-auxiliary law · Conditional entropy in the trivial extension

DefinitionMutual information#✓fully proved

The mutual information of a finite joint law \(p\) of \((X, Y)\) is \(I(X; Y) = H(X) + H(Y) - H(X, Y)\), where \(H(X)\) and \(H(Y)\) are the Shannon entropies in bits of the input and output laws of \(p\), and \(H(X, Y)\) is the Shannon entropy in bits of \(p\).

noncomputable def FiniteJointLaw.mutualInformation (p : FiniteJointLaw) : ℝ :=
  shannonEntropy p.inputLaw + shannonEntropy p.outputLaw - shannonEntropy p.law

Uses 4 · Used by 3

Statement usesFinite joint law · Input law · Output law · Shannon entropy

Used byThe worst-case optimum dominates each conditional-prefix optimum · Uniform outer constant for channel simulation · Worst-case conditional-prefix optimum

StructureFinite extension of a joint law#✓fully proved

A finite extension of a finite joint law \(p\) on \(\{0, \dots, n_X - 1\} \times \{0, \dots, n_Y - 1\}\) consists of a positive integer \(n_S\) and a probability law on triples \((x, y, s)\) with \(s \in \{0, \dots, n_S - 1\}\) whose marginal on the pairs \((x, y)\) is exactly \(p\).

structure FiniteExtension (p : FiniteJointLaw) where
  ns : ℕ
  ns_pos : 0 < ns
  law : PMF ((Fin p.nx × Fin p.ny) × Fin ns)
  marginal_eq : law.map Prod.fst = p.law

Uses 1 · Used by 18

Statement usesFinite joint law

Used byMutual information between the input and the auxiliary · Auxiliary marginal of an extension · Conditional entropy of the output given the auxiliary · Conditional entropy vanishes for a one-letter output · Conditional-prefix optimum of a joint law · The conditional-prefix optimum vanishes for a one-letter output · Each admissible extension bounds the conditional-prefix optimum · Uniform outer constant for channel simulation · Input-auxiliary law · Input marginal of the input-auxiliary law · Auxiliary marginal of the input-auxiliary law · Output-auxiliary law · Output marginal of the output-auxiliary law · Auxiliary marginal of the output-auxiliary law · Conditional entropy of the output given the input and the auxiliary · Zero output entropy given input and auxiliary for a one-letter output · Trivial extension · Auxiliary law of the trivial extension

DefinitionTrivial extension#✓fully proved

The trivial extension of a finite joint law \(p\) of an input \(X\) and an output \(Y\) has the one-letter auxiliary alphabet \(\{0\}\) and, as its law, the law of \(((X, Y), 0)\) for \((X, Y)\) distributed according to \(p\); its \((X, Y)\) marginal is \(p\).

noncomputable def FiniteExtension.trivial (p : FiniteJointLaw) : FiniteExtension p where
  ns := 1
  ns_pos := Nat.zero_lt_succ 0
  law := p.law.map (fun z => (z, (0 : Fin 1)))
  marginal_eq := by
    rw [PMF.map_comp]
    exact PMF.map_id p.law

Uses 2 · Used by 4

Statement usesFinite extension of a joint law · Finite joint law

Used byThe conditional-prefix optimum vanishes for a one-letter output · The trivial extension has zero auxiliary information · Auxiliary law of the trivial extension · Conditional entropy in the trivial extension

DefinitionAuxiliary marginal of an extension#✓fully proved

For a finite extension \(q\) of a finite joint law \(p\), viewed as the law of a triple \((X, Y, S)\) with \(S\) taking values in \(\{0, \dots, n_S - 1\}\), the auxiliary law is the marginal law of \(S\) under \(q\).

noncomputable def FiniteExtension.auxiliaryLaw {p : FiniteJointLaw}
    (q : FiniteExtension p) : PMF (Fin q.ns) :=
  q.law.map Prod.snd

Uses 2 · Used by 6

Statement usesFinite extension of a joint law · Finite joint law

Used byMutual information between the input and the auxiliary · Conditional entropy of the output given the auxiliary · Conditional entropy vanishes for a one-letter output · Auxiliary marginal of the input-auxiliary law · Auxiliary marginal of the output-auxiliary law · Auxiliary law of the trivial extension

DefinitionInput-auxiliary law#✓fully proved

Let \(q\) be a finite extension of a finite joint law of \((X, Y)\), that is, a law of \(((X, Y), S)\) with an auxiliary variable \(S\). Its input-auxiliary law is the joint law of \((X, S)\): the image of the law of \(q\) under \(((x, y), s) \mapsto (x, s)\).

noncomputable def FiniteExtension.inputAuxiliaryLaw {p : FiniteJointLaw}
    (q : FiniteExtension p) : PMF (Fin p.nx × Fin q.ns) :=
  q.law.map (fun z => (z.1.1, z.2))

Uses 2 · Used by 5

Statement usesFinite extension of a joint law · Finite joint law

Used byMutual information between the input and the auxiliary · Input marginal of the input-auxiliary law · Auxiliary marginal of the input-auxiliary law · Conditional entropy of the output given the input and the auxiliary · Zero output entropy given input and auxiliary for a one-letter output

DefinitionOutput-auxiliary law#✓fully proved

Let \(q\) be a finite extension of a finite joint law of \((X, Y)\), that is, a law of \(((X, Y), S)\) with an auxiliary variable \(S\). Its output-auxiliary law is the joint law of \((Y, S)\): the image of the law of \(q\) under \(((x, y), s) \mapsto (y, s)\).

noncomputable def FiniteExtension.outputAuxiliaryLaw {p : FiniteJointLaw}
    (q : FiniteExtension p) : PMF (Fin p.ny × Fin q.ns) :=
  q.law.map (fun z => (z.1.2, z.2))

Uses 2 · Used by 4

Statement usesFinite extension of a joint law · Finite joint law

Used byConditional entropy of the output given the auxiliary · Conditional entropy vanishes for a one-letter output · Output marginal of the output-auxiliary law · Auxiliary marginal of the output-auxiliary law

DefinitionMutual information between the input and the auxiliary#✓fully proved

For a finite extension \(q\) of a finite joint law \(p\), viewed as the law of a triple \((X, Y, S)\) whose \((X, Y)\) marginal is \(p\), this is \(I(X; S) = H(X) + H(S) - H(X, S)\), where \(H(X)\) is the Shannon entropy in bits of the \(X\) marginal of \(p\), and \(H(S)\) and \(H(X, S)\) are the Shannon entropies in bits of the \(S\) and \((X, S)\) marginals of \(q\).

noncomputable def FiniteExtension.auxiliaryInformation {p : FiniteJointLaw}
    (q : FiniteExtension p) : ℝ :=
  shannonEntropy p.inputLaw + shannonEntropy q.auxiliaryLaw -
    shannonEntropy q.inputAuxiliaryLaw

Uses 6 · Used by 5

Statement usesFinite extension of a joint law · Auxiliary marginal of an extension · Input-auxiliary law · Finite joint law · Input law · Shannon entropy

Used byConditional-prefix optimum of a joint law · The conditional-prefix optimum vanishes for a one-letter output · Each admissible extension bounds the conditional-prefix optimum · Uniform outer constant for channel simulation · The trivial extension has zero auxiliary information

DefinitionConditional entropy of the output given the auxiliary#✓fully proved

For a finite extension \(q\) of a finite joint law \(p\), viewed as the law of a triple \((X, Y, S)\) whose \((X, Y)\) marginal is \(p\), this is \(H(Y \mid S) = H(Y, S) - H(S)\), where \(H(Y, S)\) and \(H(S)\) are the Shannon entropies in bits of the \((Y, S)\) and \(S\) marginals of \(q\).

noncomputable def FiniteExtension.conditionalEntropy {p : FiniteJointLaw}
    (q : FiniteExtension p) : ℝ :=
  shannonEntropy q.outputAuxiliaryLaw - shannonEntropy q.auxiliaryLaw

Uses 5 · Used by 6

Statement usesFinite extension of a joint law · Auxiliary marginal of an extension · Output-auxiliary law · Finite joint law · Shannon entropy

Used byConditional entropy vanishes for a one-letter output · Conditional-prefix optimum of a joint law · The conditional-prefix optimum vanishes for a one-letter output · Each admissible extension bounds the conditional-prefix optimum · Uniform outer constant for channel simulation · Conditional entropy in the trivial extension

DefinitionConditional entropy of the output given the input and the auxiliary#✓fully proved

For a finite extension of a finite joint law, with input \(X\), output \(Y\) and auxiliary \(S\), the conditional entropy of \(Y\) given \((X, S)\) is \(H(Y \mid X, S) = H(X, Y, S) - H(X, S)\), where \(H\) denotes Shannon entropy in bits, \(H(X, Y, S)\) is the entropy of the law of the extension and \(H(X, S)\) is the entropy of its \((X, S)\) marginal.

It vanishes exactly when \(Y\) is almost surely a deterministic function of \((X, S)\).

noncomputable def FiniteExtension.outputGivenInputAuxiliaryEntropy {p : FiniteJointLaw}
    (q : FiniteExtension p) : ℝ :=
  shannonEntropy q.law - shannonEntropy q.inputAuxiliaryLaw

Uses 4 · Used by 5

Statement usesFinite extension of a joint law · Input-auxiliary law · Finite joint law · Shannon entropy

Used byConditional-prefix optimum of a joint law · The conditional-prefix optimum vanishes for a one-letter output · Each admissible extension bounds the conditional-prefix optimum · Uniform outer constant for channel simulation · Zero output entropy given input and auxiliary for a one-letter output

TheoremZero output entropy given input and auxiliary for a one-letter output#✓fully proved

Let \(p\) be a finite joint law of an input \(X\) and an output \(Y\) whose output alphabet has exactly one letter. Then for every finite extension of \(p\) by an auxiliary \(S\), the conditional entropy \(H(Y \mid X, S)\) of the output given the input and the auxiliary is \(0\).

theorem FiniteExtension.outputGivenInputAuxiliaryEntropy_eq_zero_of_output_subsingleton
    {p : FiniteJointLaw} [Subsingleton (Fin p.ny)] (q : FiniteExtension p) :
    q.outputGivenInputAuxiliaryEntropy = 0

Uses 6 · Used by 1

Statement usesFinite extension of a joint law · Conditional entropy of the output given the input and the auxiliary · Finite joint law

Proof usesInput-auxiliary law · Shannon entropy · Entropy is invariant under relabeling

Used byThe conditional-prefix optimum vanishes for a one-letter output

TheoremAuxiliary law of the trivial extension#✓fully proved

For every finite joint law \(p\), the auxiliary law of the trivial extension of \(p\) is the point mass at \(0\), the only letter of its one-letter auxiliary alphabet \(\{0\}\).

@[simp] theorem FiniteExtension.trivial_auxiliaryLaw (p : FiniteJointLaw) :
    (FiniteExtension.trivial p).auxiliaryLaw = PMF.pure (0 : Fin 1)

Uses 4

Statement usesFinite extension of a joint law · Auxiliary marginal of an extension · Trivial extension · Finite joint law

TheoremThe trivial extension has zero auxiliary information#✓fully proved

For every finite joint law \(p\), the mutual information \(I(X; S)\) between the input \(X\) and the auxiliary \(S\) in the trivial extension of \(p\), whose auxiliary alphabet has a single letter, is \(0\).

@[simp] theorem FiniteExtension.trivial_auxiliaryInformation (p : FiniteJointLaw) :
    (FiniteExtension.trivial p).auxiliaryInformation = 0

Uses 7 · Used by 1

Statement usesMutual information between the input and the auxiliary · Trivial extension · Finite joint law

Proof usesInput law · Shannon entropy · A constant observation has zero entropy · Appending a singleton coordinate preserves entropy

Used byThe conditional-prefix optimum vanishes for a one-letter output

TheoremConditional entropy in the trivial extension#✓fully proved

For every finite joint law \(p\) of an input \(X\) and an output \(Y\), the conditional entropy \(H(Y \mid S)\) of the output given the auxiliary \(S\) in the trivial extension of \(p\) equals the Shannon entropy \(H(Y)\) of the output law of \(p\).

@[simp] theorem FiniteExtension.trivial_conditionalEntropy (p : FiniteJointLaw) :
    (FiniteExtension.trivial p).conditionalEntropy = shannonEntropy p.outputLaw

Uses 7

Statement usesConditional entropy of the output given the auxiliary · Trivial extension · Finite joint law · Output law · Shannon entropy

Proof usesA constant observation has zero entropy · Appending a singleton coordinate preserves entropy

TheoremInput marginal of the input-auxiliary law#✓fully proved

Let \(q\) be a finite extension of a finite joint law \(p\) of \((X, Y)\) by an auxiliary variable \(S\). Then the marginal of \(X\) under the joint law of \((X, S)\) in \(q\) equals the law of \(X\) under \(p\).

@[simp] theorem FiniteExtension.inputAuxiliaryLaw_map_fst {p : FiniteJointLaw}
    (q : FiniteExtension p) : q.inputAuxiliaryLaw.map Prod.fst = p.inputLaw

Uses 4

Statement usesFinite extension of a joint law · Input-auxiliary law · Finite joint law · Input law

TheoremOutput marginal of the output-auxiliary law#✓fully proved

Let \(q\) be a finite extension of a finite joint law \(p\) of \((X, Y)\) by an auxiliary variable \(S\). Then the marginal of \(Y\) under the joint law of \((Y, S)\) in \(q\) equals the law of \(Y\) under \(p\).

@[simp] theorem FiniteExtension.outputAuxiliaryLaw_map_fst {p : FiniteJointLaw}
    (q : FiniteExtension p) : q.outputAuxiliaryLaw.map Prod.fst = p.outputLaw

Uses 4

Statement usesFinite extension of a joint law · Output-auxiliary law · Finite joint law · Output law

TheoremAuxiliary marginal of the input-auxiliary law#✓fully proved

Let \(q\) be a finite extension of a finite joint law of \((X, Y)\) by an auxiliary variable \(S\). Then the marginal of \(S\) under the joint law of \((X, S)\) in \(q\) equals the law of \(S\) in \(q\).

@[simp] theorem FiniteExtension.inputAuxiliaryLaw_map_snd {p : FiniteJointLaw}
    (q : FiniteExtension p) : q.inputAuxiliaryLaw.map Prod.snd = q.auxiliaryLaw

Uses 4

Statement usesFinite extension of a joint law · Auxiliary marginal of an extension · Input-auxiliary law · Finite joint law

TheoremAuxiliary marginal of the output-auxiliary law#✓fully proved

Let \(q\) be a finite extension of a finite joint law of \((X, Y)\) by an auxiliary variable \(S\). Then the marginal of \(S\) under the joint law of \((Y, S)\) in \(q\) equals the law of \(S\) in \(q\).

@[simp] theorem FiniteExtension.outputAuxiliaryLaw_map_snd {p : FiniteJointLaw}
    (q : FiniteExtension p) : q.outputAuxiliaryLaw.map Prod.snd = q.auxiliaryLaw

Uses 4

Statement usesFinite extension of a joint law · Auxiliary marginal of an extension · Output-auxiliary law · Finite joint law

TheoremConditional entropy vanishes for a one-letter output#✓fully proved

If the output alphabet of a finite joint law \(p\) of \((X, Y)\) has exactly one element, then for every finite extension of \(p\) by an auxiliary variable \(S\), the conditional entropy \(H(Y \mid S)\) is \(0\).

theorem FiniteExtension.conditionalEntropy_eq_zero_of_output_subsingleton
    {p : FiniteJointLaw} [Subsingleton (Fin p.ny)] (q : FiniteExtension p) :
    q.conditionalEntropy = 0

Uses 7 · Used by 1

Statement usesFinite extension of a joint law · Conditional entropy of the output given the auxiliary · Finite joint law

Proof usesAuxiliary marginal of an extension · Output-auxiliary law · Shannon entropy · Entropy is invariant under relabeling

Used byThe conditional-prefix optimum vanishes for a one-letter output

DefinitionConditional-prefix optimum of a joint law#✓fully proved

For a finite joint law \(p\) of \((X, Y)\), this is the infimum in the extended reals of the conditional entropy \(H(Y \mid S)\) in bits over all finite extensions of \(p\) by an auxiliary variable \(S\) such that \(I(X; S) = 0\) and \(H(Y \mid X, S) = 0\). The infimum of the empty set is \(+\infty\).

noncomputable def conditionalPrefixOptimum (p : FiniteJointLaw) : EReal :=
  sInf {h | ∃ q : FiniteExtension p, q.auxiliaryInformation = 0 ∧
    q.outputGivenInputAuxiliaryEntropy = 0 ∧
    h = (q.conditionalEntropy : EReal)}

Sources

• Li, arXiv:2501.13736v4, equation cs_h_c.

Uses 5 · Used by 4

Statement usesFinite extension of a joint law · Mutual information between the input and the auxiliary · Conditional entropy of the output given the auxiliary · Conditional entropy of the output given the input and the auxiliary · Finite joint law

Used byThe conditional-prefix optimum vanishes for a one-letter output · Each admissible extension bounds the conditional-prefix optimum · The worst-case optimum dominates each conditional-prefix optimum · Worst-case conditional-prefix optimum

DefinitionWorst-case conditional-prefix optimum#✓fully proved

For a real number \(t\), the worst-case optimum at \(t\) is the supremum, taken in the extended reals, of the conditional-prefix optimum of \(p\) over all finite joint laws \(p\) of an input \(X\) and an output \(Y\) whose mutual information \(I(X; Y)\), in bits, equals \(t\); it is \(-\infty\) when no such law exists.

noncomputable def worstCaseOptimum (t : ℝ) : EReal :=
  sSup {h | ∃ p : FiniteJointLaw, p.mutualInformation = t ∧ h = conditionalPrefixOptimum p}

Uses 3 · Used by 2

Statement usesFinite joint law · Mutual information · Conditional-prefix optimum of a joint law

Used byChannel simulation constant · The worst-case optimum dominates each conditional-prefix optimum

DefinitionChannel simulation constant#✓fully proved

The constant \(c_c^*\) is the limit superior in the extended reals, as the real number \(t\) tends to \(+\infty\), of \(W(t) - t - \log_2 t\), where \(W(t)\) is the worst-case optimum at \(t\): the supremum of the conditional-prefix optimum over all finite joint laws whose mutual information in bits is exactly \(t\).

noncomputable def channelSimulationConstant : EReal :=
  Filter.limsup (fun t : ℝ => worstCaseOptimum t - (t : EReal) -
    (Real.log t / Real.log 2 : EReal)) Filter.atTop

Sources

• Li, arXiv:2501.13736v4, definition of c_c*.

Uses 1

Statement usesWorst-case conditional-prefix optimum

DefinitionUniform outer constant for channel simulation#✓fully proved

A real number \(\alpha\) is a uniform outer constant when there is a real \(\beta > 0\) such that for every finite joint law \(p\) of \((X, Y)\) there is a finite extension of \(p\) by an auxiliary variable \(S\) with \(I(X; S) = 0\) and \(H(Y \mid X, S) = 0\) and

\[H(Y \mid S) \le I(X; Y) + \log_2\bigl(I(X; Y) + \beta\bigr) + \alpha,\]

where all entropies and mutual informations are in bits and are computed from the law of \((X, Y, S)\) in the extension.

def HasUniformOuterConstant (α : ℝ) : Prop :=
  ∃ β : ℝ, 0 < β ∧ ∀ p : FiniteJointLaw, ∃ q : FiniteExtension p,
    q.auxiliaryInformation = 0 ∧ q.outputGivenInputAuxiliaryEntropy = 0 ∧
    q.conditionalEntropy ≤ p.mutualInformation +
      Real.log (p.mutualInformation + β) / Real.log 2 + α

Uses 6 · Used by 1

Statement usesFinite extension of a joint law · Mutual information between the input and the auxiliary · Conditional entropy of the output given the auxiliary · Conditional entropy of the output given the input and the auxiliary · Finite joint law · Mutual information

Used byInfimum of the uniform outer constants

DefinitionInfimum of the uniform outer constants#✓fully proved

Call a real number \(\alpha\) a uniform outer constant when there is a real \(\beta > 0\) such that every finite joint law \(p\) of an input \(X\) and an output \(Y\) has a finite extension by an auxiliary \(S\) with \(I(X; S) = 0\), \(H(Y \mid X, S) = 0\) and \(H(Y \mid S) \le I(X; Y) + \log_2(I(X; Y) + \beta) + \alpha\), where entropies and mutual informations are in bits. This is the infimum of the set of uniform outer constants, taken in the extended reals, so it is \(+\infty\) when there is none.

noncomputable def uniformOuterConstantInfimum : EReal :=
  sInf {h | ∃ α : ℝ, HasUniformOuterConstant α ∧ h = (α : EReal)}

Uses 1

Statement usesUniform outer constant for channel simulation

TheoremEach admissible extension bounds the conditional-prefix optimum#✓fully proved

Let \(p\) be a finite joint law of \((X, Y)\) and let \(q\) be a finite extension of \(p\) by an auxiliary variable \(S\) with \(I(X; S) = 0\) and \(H(Y \mid X, S) = 0\). Then the conditional-prefix optimum of \(p\) is at most the conditional entropy \(H(Y \mid S)\) of \(q\).

theorem conditionalPrefixOptimum_le {p : FiniteJointLaw} (q : FiniteExtension p)
    (hq : q.auxiliaryInformation = 0)
    (hqrec : q.outputGivenInputAuxiliaryEntropy = 0) :
    conditionalPrefixOptimum p ≤ (q.conditionalEntropy : EReal)

Uses 6 · Used by 1

Statement usesFinite extension of a joint law · Mutual information between the input and the auxiliary · Conditional entropy of the output given the auxiliary · Conditional entropy of the output given the input and the auxiliary · Finite joint law · Conditional-prefix optimum of a joint law

Used byThe conditional-prefix optimum vanishes for a one-letter output

TheoremThe conditional-prefix optimum vanishes for a one-letter output#✓fully proved

If the output alphabet of a finite joint law \(p\) has exactly one element, then the conditional-prefix optimum of \(p\) equals \(0\).

theorem conditionalPrefixOptimum_eq_zero_of_output_subsingleton
    (p : FiniteJointLaw) [Subsingleton (Fin p.ny)] :
    conditionalPrefixOptimum p = 0

Uses 11

Statement usesFinite joint law · Conditional-prefix optimum of a joint law

Proof usesFinite extension of a joint law · Mutual information between the input and the auxiliary · Conditional entropy of the output given the auxiliary · Conditional entropy vanishes for a one-letter output · Conditional entropy of the output given the input and the auxiliary · Zero output entropy given input and auxiliary for a one-letter output · Trivial extension · The trivial extension has zero auxiliary information · Each admissible extension bounds the conditional-prefix optimum

TheoremThe worst-case optimum dominates each conditional-prefix optimum#✓fully proved

For every finite joint law \(p\) of \((X, Y)\), the conditional-prefix optimum of \(p\) is at most the worst-case optimum at \(t = I(X; Y)\), the mutual information of \(p\) in bits.

theorem conditionalPrefixOptimum_le_worstCaseOptimum (p : FiniteJointLaw) :
    conditionalPrefixOptimum p ≤ worstCaseOptimum p.mutualInformation

Uses 4

Statement usesFinite joint law · Mutual information · Conditional-prefix optimum of a joint law · Worst-case conditional-prefix optimum

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.