InformationTheory.Shannon.Gambling.SideInformation

Imports 4

Gambling with side information (Cover–Thomas) #

A horse race on a finite alphabet α (the outcome X) is run while a gambler observes side information Y on a finite alphabet γ. The joint law is presented in factored form (pY, pXgivenY): pY is the law of Y and pXgivenY y is the conditional law of X given Y = y. Betting a proportional (Kelly) strategy that depends on the observed side information, the increment of the doubling rate obtained from Y equals the mutual information I(X; Y).

Main definitions #

sideMarginalX — the X-marginal pmf pX x = ∑ y, pY y · pXgivenY y x.
sideInfoJoint — the joint pmf q (x, y) = pY y · pXgivenY y x on α × γ.
condDoublingRate — the conditional doubling rate W(b | Y) = ∑ y, pY y · W(b y, o, pXgivenY y).
sideInfoMutualInfo — the mutual information in symmetric form I(X; Y) = H(X) + H(Y) − H(X, Y).

Main statements #

condDoublingRate_le_proportional — conditional Kelly optimality: proportional betting on each observed y maximizes the conditional doubling rate.
sideInfo_doublingRate_increment_eq_mutualInfo — the increment of the optimal doubling rate due to the side information Y equals I(X; Y).

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

noncomputable def

InformationTheory.Shannon.Gambling.sideMarginalX

source

{α : Type u_1} {γ : Type u_2} [Fintype γ] (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

α → ℝ

The X-marginal pmf obtained from the side-information factored law: pX x = ∑ y, pY y · pXgivenY y x.

Equations

InformationTheory.Shannon.Gambling.sideMarginalX pY pXgivenY x = ∑ y : γ, pY y * pXgivenY y x

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Gambling.sideInfoJoint

source

{α : Type u_1} {γ : Type u_2} (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

α × γ → ℝ

The joint pmf on α × γ of the outcome and the side information: q (x, y) = pY y · pXgivenY y x.

Equations

InformationTheory.Shannon.Gambling.sideInfoJoint pY pXgivenY p = pY p.2 * pXgivenY p.2 p.1

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Gambling.condDoublingRate

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (b : γ → α → ℝ) (o : α → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

ℝ

The conditional (side-information) doubling rate of a strategy b that may depend on the observed side information y: W(b | Y) = ∑ y, pY y · W(b y, o, pXgivenY y).

Equations

InformationTheory.Shannon.Gambling.condDoublingRate b o pY pXgivenY = ∑ y : γ, pY y * InformationTheory.Shannon.Gambling.doublingRate (b y) o (pXgivenY y)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Gambling.sideInfoMutualInfo

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

ℝ

The mutual information I(X; Y) in symmetric pmf form I(X; Y) = H(X) + H(Y) − H(X, Y), where the entropies are the finite-alphabet Shannon entropies of the marginals and the joint. The symmetric form carries the joint entropy H(X, Y) as an independent term, so it is not crafted to match the doubling-rate increment H(X) − H(X|Y); recognizing it as that increment forces a detour through the chain-rule bridge (sideInfoJointEntropy_eq_chain). Not trivial-circular. @audit:ok

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.Gambling.sideMarginalX_mem_stdSimplex

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] {pY : γ → ℝ} {pXgivenY : γ → α → ℝ} (hpY : pY ∈ stdSimplex ℝ γ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) :

sideMarginalX pY pXgivenY ∈ stdSimplex ℝ α

Used by

theorem

InformationTheory.Shannon.Gambling.sideInfoJoint_mem_stdSimplex

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] {pY : γ → ℝ} {pXgivenY : γ → α → ℝ} (hpY : pY ∈ stdSimplex ℝ γ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) :

sideInfoJoint pY pXgivenY ∈ stdSimplex ℝ (α × γ)

Used by

theorem

InformationTheory.Shannon.Gambling.sideInfo_logOdds_cancel

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (o : α → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

∑ y : γ, pY y * ∑ x : α, pXgivenY y x * Real.log (o x) = ∑ x : α, sideMarginalX pY pXgivenY x * Real.log (o x)

Used by

theorem

InformationTheory.Shannon.Gambling.condDoublingRate_proportional_eq

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (o : α → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) (ho : ∀ (x : α), 0 < o x) :

condDoublingRate pXgivenY o pY pXgivenY = ∑ x : α, sideMarginalX pY pXgivenY x * Real.log (o x) - ∑ y : γ, pY y * ∑ x : α, (pXgivenY y x).negMulLog

Used by

theorem

InformationTheory.Shannon.Gambling.sideInfoJointEntropy_eq_chain

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) :

∑ p : α × γ, (sideInfoJoint pY pXgivenY p).negMulLog = ∑ y : γ, (pY y).negMulLog + ∑ y : γ, pY y * ∑ x : α, (pXgivenY y x).negMulLog

Chain rule bridge H(X, Y) = H(Y) + H(X | Y) in pmf form (the honesty linchpin of the theorem: it lets the symmetric sideInfoMutualInfo be recognized as the doubling-rate increment without defining the latter to match). sorryAx-free ([propext, Classical.choice, Quot.sound]); an independent identity via the unconditional Real.negMulLog_mul plus each row sum ∑ x, pXgivenY y x = 1, and does not assume the conclusion. @audit:ok

Used by

theorem

InformationTheory.Shannon.Gambling.condDoublingRate_le_proportional

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (b : γ → α → ℝ) (o : α → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) (hpY : pY ∈ stdSimplex ℝ γ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) (hb : ∀ (y : γ), b y ∈ stdSimplex ℝ α) (hb_pos : ∀ (y : γ) (x : α), 0 < b y x) (ho : ∀ (x : α), 0 < o x) :

condDoublingRate b o pY pXgivenY ≤ condDoublingRate pXgivenY o pY pXgivenY

Proportional (Kelly) betting on each observed value of the side information maximizes the conditional doubling rate: for any full-support strategy b and positive odds o, W(b | Y) ≤ W(pXgivenY | Y). This is the conditional step towards Cover–Thomas. sorryAx-free ([propext, Classical.choice, Quot.sound]); per-y reuse of doublingRate_le_proportional weighted by pY y ≥ 0, no bundling. All hypotheses are regularity preconditions (hpY/hcond pmf, hb/hb_pos full-support bet, ho positive odds), none load-bearing. @audit:ok

Used by

theorem

InformationTheory.Shannon.Gambling.sideInfo_doublingRate_increment_eq_mutualInfo

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] (o : α → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) (hpY : pY ∈ stdSimplex ℝ γ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) (ho : ∀ (x : α), 0 < o x) :

condDoublingRate pXgivenY o pY pXgivenY - doublingRate (sideMarginalX pY pXgivenY) o (sideMarginalX pY pXgivenY) = sideInfoMutualInfo pY pXgivenY

The increment of the optimal doubling rate obtained from the side information Y equals the mutual information I(X; Y). Writing W*(X | Y) for the optimal conditional doubling rate and W*(X) for the optimal doubling rate of the X-marginal, W*(X | Y) − W*(X) = I(X; Y). This is Cover–Thomas (gambling with side information). sorryAx-free ([propext, Classical.choice, Quot.sound]). Not trivial-circular: the increment reduces to H(X) − H(X|Y), but the RHS sideInfoMutualInfo is the symmetric H(X) + H(Y) − H(X, Y), so the closing linarith consumes the chain-rule bridge sideInfoJointEntropy_eq_chain to cancel the joint entropy term (dropping it leaves the goal underdetermined). All hypotheses (hpY/hcond pmf, ho positive odds) are regularity preconditions, none load-bearing. @audit:ok

Used by