InformationTheory.Shannon.Portfolio.SideInformation

Imports 4

Log-optimal portfolios with side information (Cover–Thomas) #

An investor allocating wealth across m stocks with price relatives X : α → (Fin m → ℝ) observes side information Y on a finite alphabet γ. The joint law is presented in factored form (pY, pXgivenY). Using a portfolio bcond y that may depend on the observed side information gives the conditional growth rate W(bcond | Y) = ∑ y, pY y · W(pXgivenY y, X, bcond y). The increment of the growth rate obtained from Y over the marginal log-optimal growth is bounded above by the mutual information I(X; Y).

This is the non-diagonal mirror of the horse-race theorem InformationTheory.Shannon.Gambling.sideInfo_doublingRate_increment_eq_mutualInfo. In the diagonal (horse-race) case Kelly betting is proportional and the increment equals I(X; Y); for a general market the log-optimal portfolio is not proportional, the per-term log cancellation of the gambling proof fails, and the identity weakens to the inequality ΔW ≤ I(X; Y) obtained from Gibbs' inequality and competitive optimality of the marginal log-optimal portfolio.

Main definitions #

condGrowthRate — the conditional growth rate W(bcond | Y) = ∑ y, pY y · W(pXgivenY y, X, bcond y).

Main statements #

sideInfo_growthRate_increment_le_mutualInfo — the increment of the growth rate due to side information Y is at most the mutual information I(X; Y).

References #

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

noncomputable def

InformationTheory.Shannon.Portfolio.condGrowthRate

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] {m : ℕ} (X : α → Fin m → ℝ) (bcond : γ → Fin m → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

ℝ

The conditional (side-information) growth rate of a portfolio bcond that may depend on the observed side information y: W(bcond | Y) = ∑ y, pY y · W(pXgivenY y, X, bcond y).

Equations

InformationTheory.Shannon.Portfolio.condGrowthRate X bcond pY pXgivenY = ∑ y : γ, pY y * InformationTheory.Shannon.Portfolio.growthRate (pXgivenY y) X (bcond y)

Instances For

Used by

theorem

InformationTheory.Shannon.Portfolio.gibbs_core

source

(a b c d : ℝ) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) (ha : 0 ≤ a) (hpos : 0 < a → 0 < b ∧ 0 < c ∧ 0 < d) :

a - b * c / d ≤ a * (Real.log a - Real.log b - Real.log c + Real.log d)

Used by

theorem

InformationTheory.Shannon.Portfolio.sideInfoMutualInfo_eq_condKL

source

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

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

Used by

theorem

InformationTheory.Shannon.Portfolio.increment_eq

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] {m : ℕ} (X : α → Fin m → ℝ) (bs : Fin m → ℝ) (bcond : γ → Fin m → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) :

condGrowthRate X bcond pY pXgivenY - growthRate (Gambling.sideMarginalX pY pXgivenY) X bs = ∑ y : γ, pY y * ∑ x : α, pXgivenY y x * (Real.log (wealthRelative X (bcond y) x) - Real.log (wealthRelative X bs x))

Used by

theorem

InformationTheory.Shannon.Portfolio.sideInfo_growthRate_increment_le_mutualInfo

source

{α : Type u_1} [Fintype α] {γ : Type u_2} [Fintype γ] {m : ℕ} (X : α → Fin m → ℝ) (bs : Fin m → ℝ) (bcond : γ → Fin m → ℝ) (pY : γ → ℝ) (pXgivenY : γ → α → ℝ) (hpY : pY ∈ stdSimplex ℝ γ) (hcond : ∀ (y : γ), pXgivenY y ∈ stdSimplex ℝ α) (hpos : ∀ (a : α), ∀ c ∈ stdSimplex ℝ (Fin m), 0 < wealthRelative X c a) (hbs : bs ∈ stdSimplex ℝ (Fin m)) (hbcond : ∀ (y : γ), bcond y ∈ stdSimplex ℝ (Fin m)) (hKT : ∀ (i : Fin m), ∑ a : α, Gambling.sideMarginalX pY pXgivenY a * X a i / wealthRelative X bs a ≤ 1) :

condGrowthRate X bcond pY pXgivenY - growthRate (Gambling.sideMarginalX pY pXgivenY) X bs ≤ Gambling.sideInfoMutualInfo pY pXgivenY

(Cover–Thomas, portfolio with side information): the increment of the growth rate obtained from the side information Y is bounded above by the mutual information I(X; Y). Here bs is a marginal log-optimal (Kuhn–Tucker) portfolio and bcond y an arbitrary portfolio on the simplex for each observed y, so W(bcond | Y) − W*(X) ≤ I(X; Y).

Unlike the horse-race mirror sideInfo_doublingRate_increment_eq_mutualInfo (an equality), the non-proportional log-optimal portfolio yields only an inequality.

@audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). hbs/hbcond are simplex-membership regularity (portfolio validity); without them the statement is false as framed (an off-simplex bcond gives ΔW = log 100 > 0 = I under X ⊥ Y). hpos is log-domain positivity and hKT the Kuhn–Tucker characterization of the marginal log-optimal baseline bs, consumed via the proven competitive_optimality — none is the conclusion. The ΔW ≤ I bound is genuinely derived from per-outcome Gibbs plus competitive optimality; the dropped hKTcond (optimality of bcond) is not needed for the upper bound. No load-bearing hypothesis.

Used by