InformationTheory.Shannon.Portfolio.Basic

Imports 12

Log-optimal portfolios (Cover–Thomas) #

For a market on a finite outcome space α with true law p : α → ℝ and price relatives X : α → (Fin m → ℝ) (the factor by which stock i multiplies wealth in outcome a), a portfolio b : Fin m → ℝ on the simplex distributes wealth across the m stocks. Its wealth relative in outcome a is S_b(a) = ∑ i, b i · X a i, and its growth (doubling) rate is W(b) = ∑ a, p a · log (S_b(a)).

This is the non-diagonal generalization of the horse-race doubling rate InformationTheory.Shannon.Gambling.doublingRate (recovered by the diagonal choice X a i = o i · [a = i]).

Main definitions #

wealthRelative — the wealth relative S_b(a) = ∑ i, b i · X a i.
growthRate — the growth rate W(b) = ∑ a, p a · log (S_b(a)).

Main statements #

competitive_optimality — for a Kuhn–Tucker portfolio bs, every portfolio b satisfies E[S_b / S_bs] ≤ 1.
growthRate_concaveOn — the growth rate is concave on the simplex.
logOptimal_of_kuhnTucker — reverse: the Kuhn–Tucker condition implies log-optimality.
kuhnTucker_of_logOptimal — forward: log-optimality implies the Kuhn–Tucker condition.

References #

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

noncomputable def

InformationTheory.Shannon.Portfolio.wealthRelative

source

{α : Type u_1} {m : ℕ} (X : α → Fin m → ℝ) (b : Fin m → ℝ) (a : α) :

ℝ

Wealth relative S_b(a) = ∑ i, b i · X a i of portfolio b under price relatives X.

Equations

InformationTheory.Shannon.Portfolio.wealthRelative X b a = ∑ i : Fin m, b i * X a i

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.growthRate

source

{α : Type u_1} [Fintype α] {m : ℕ} (p : α → ℝ) (X : α → Fin m → ℝ) (b : Fin m → ℝ) :

ℝ

Growth (doubling) rate W(b) = ∑ a, p a · log (S_b(a)) of portfolio b.

Equations

InformationTheory.Shannon.Portfolio.growthRate p X b = ∑ a : α, p a * Real.log (InformationTheory.Shannon.Portfolio.wealthRelative X b a)

Instances For

Used by

theorem

InformationTheory.Shannon.Portfolio.competitive_optimality

source

{α : Type u_1} [Fintype α] {m : ℕ} (p : α → ℝ) (X : α → Fin m → ℝ) (bs b : Fin m → ℝ) (hb : b ∈ stdSimplex ℝ (Fin m)) (hKT : ∀ (i : Fin m), ∑ a : α, p a * X a i / wealthRelative X bs a ≤ 1) :

∑ a : α, p a * (wealthRelative X b a / wealthRelative X bs a) ≤ 1

(Cover–Thomas): competitive optimality of a Kuhn–Tucker portfolio bs. If bs satisfies the Kuhn–Tucker condition ∀ i, ∑ a, p a · X a i / S_bs(a) ≤ 1, then every portfolio b on the simplex has expected wealth ratio at most one, ∑ a, p a · (S_b(a) / S_bs(a)) ≤ 1.

@audit:ok

Used by

theorem

InformationTheory.Shannon.Portfolio.concaveOn_finset_sum

source

{E : Type u_2} [AddCommMonoid E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) {ι : Type u_3} (f : ι → E → ℝ) (t : Finset ι) :

(∀ i ∈ t, ConcaveOn ℝ s (f i)) → ConcaveOn ℝ s fun (x : E) => ∑ i ∈ t, f i x

Used by

theorem

InformationTheory.Shannon.Portfolio.growthTerm_concaveOn

source

{α : Type u_1} {m : ℕ} (p : α → ℝ) (X : α → Fin m → ℝ) (a : α) (hpa : 0 ≤ p a) (hpos : ∀ b ∈ stdSimplex ℝ (Fin m), 0 < wealthRelative X b a) :

ConcaveOn ℝ (stdSimplex ℝ (Fin m)) fun (b : Fin m → ℝ) => p a * Real.log (wealthRelative X b a)

Used by

theorem

InformationTheory.Shannon.Portfolio.growthRate_concaveOn

source

{α : Type u_1} [Fintype α] {m : ℕ} (p : α → ℝ) (X : α → Fin m → ℝ) (hp : p ∈ stdSimplex ℝ α) (hpos : ∀ (a : α), ∀ b ∈ stdSimplex ℝ (Fin m), 0 < wealthRelative X b a) :

ConcaveOn ℝ (stdSimplex ℝ (Fin m)) (growthRate p X)

(Cover–Thomas): the growth rate is concave in the portfolio.

@audit:ok

Used by

theorem

InformationTheory.Shannon.Portfolio.logOptimal_of_kuhnTucker

source

{α : Type u_1} [Fintype α] {m : ℕ} (p : α → ℝ) (X : α → Fin m → ℝ) (bs : Fin m → ℝ) (hp : p ∈ stdSimplex ℝ α) (hbs : bs ∈ stdSimplex ℝ (Fin m)) (hpos : ∀ (a : α), ∀ b ∈ stdSimplex ℝ (Fin m), 0 < wealthRelative X b a) (hKT : ∀ (i : Fin m), ∑ a : α, p a * X a i / wealthRelative X bs a ≤ 1) :

IsMaxOn (growthRate p X) (stdSimplex ℝ (Fin m)) bs

(Cover–Thomas), reverse direction: a portfolio bs satisfying the Kuhn–Tucker condition is log-optimal (maximizes the growth rate on the simplex).

@audit:ok

Used by

theorem

InformationTheory.Shannon.Portfolio.kuhnTucker_of_logOptimal

source

{α : Type u_1} [Fintype α] {m : ℕ} (p : α → ℝ) (X : α → Fin m → ℝ) (bs : Fin m → ℝ) (hp : p ∈ stdSimplex ℝ α) (hbs : bs ∈ stdSimplex ℝ (Fin m)) (hpos : ∀ (a : α), 0 < wealthRelative X bs a) (hmax : IsMaxOn (growthRate p X) (stdSimplex ℝ (Fin m)) bs) (i : Fin m) :

∑ a : α, p a * X a i / wealthRelative X bs a ≤ 1

(Cover–Thomas), forward direction: a log-optimal portfolio bs satisfies the Kuhn–Tucker condition ∀ i, ∑ a, p a · X a i / S_bs(a) ≤ 1.

@audit:ok

Used by