InformationTheory.Shannon.Portfolio.OperationalSequences

Imports 7

Operational log-optimal portfolios over i.i.d. markets (Cover–Thomas) #

For an i.i.d. sequence of market outcomes As : ℕ → Ω → α on a finite alphabet α, an investor reinvesting all wealth with a fixed rebalanced portfolio b : Fin m → ℝ and price relatives X : α → (Fin m → ℝ) accumulates wealth whose log grows like ∑ i, log (S_b (As i)). The operational (sequence-level) result is that the time-averaged log-wealth growth converges almost surely to the growth rate W(b) = growthRate p X b, where p is the law of a single outcome As 0. This is the non-diagonal generalization of the horse-race operational theorem InformationTheory.Shannon.Gambling.seqLogWealth_div_tendsto_doublingRate (recovered by the diagonal choice X a i = o i · [a = i]), and the strong-law counterpart of the single-shot log-optimality theorem logOptimal_of_kuhnTucker.

Main definitions #

portfolioLogReturn — the alphabet-side per-period log return g a = log (S_b a).
seqLogWealth — the log-wealth after n periods, log S_n = ∑ i, portfolioLogReturn X b (As i).

Main statements #

seqLogWealth_div_tendsto_growthRate — for a fixed portfolio b, (1/n)·log S_n converges almost surely to growthRate (lawPmf μ (As 0)) X b.
seqLogWealth_asymptotically_optimal — a log-optimal (Kuhn–Tucker) portfolio bs is asymptotically optimal: almost surely both growth rates exist and the arbitrary portfolio b does not beat bs.

Implementation notes #

The proof reuses the strong law ProbabilityTheory.strong_law_ae_real applied to the sequence fun i ω ↦ portfolioLogReturn X b (As i ω), exactly as the gambling mirror applies it to the horse-race log return. The only non-mechanical step is identifying the strong-law limit μ[portfolioLogReturn X b ∘ As 0] with growthRate (lawPmf μ (As 0)) X b, via the bet-independent discrete-expectation bridge InformationTheory.Shannon.Gambling.integral_comp_law. The deterministic dominance W(b) ≤ W(bs) is the IsMaxOn conclusion of the static logOptimal_of_kuhnTucker applied to b. The non-diagonal difficulty (log-optimal portfolios are not proportional) is fully absorbed by that static theorem; the strong-law skeleton is bet-independent.

References #

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

noncomputable def

InformationTheory.Shannon.Portfolio.portfolioLogReturn

source

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

α → ℝ

The alphabet-side per-period log return g a = log (S_b a): the log growth factor of wealth when the outcome is a, the portfolio is b, and the price relatives are X.

Equations

InformationTheory.Shannon.Portfolio.portfolioLogReturn X b a = Real.log (InformationTheory.Shannon.Portfolio.wealthRelative X b a)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.seqLogWealth

source

{Ω : Type u_1} {α : Type u_2} {m : ℕ} (X : α → Fin m → ℝ) (b : Fin m → ℝ) (As : ℕ → Ω → α) (n : ℕ) :

Ω → ℝ

The log-wealth after n periods starting from unit wealth, log S_n = ∑ i < n, portfolioLogReturn X b (As i ω).

Equations

InformationTheory.Shannon.Portfolio.seqLogWealth X b As n ω = ∑ i ∈ Finset.range n, InformationTheory.Shannon.Portfolio.portfolioLogReturn X b (As i ω)

Instances For

Used by

theorem

InformationTheory.Shannon.Portfolio.measurable_portfolioLogReturn

source

{α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {m : ℕ} (X : α → Fin m → ℝ) (b : Fin m → ℝ) :

Measurable (portfolioLogReturn X b)

Used by

theorem

InformationTheory.Shannon.Portfolio.integrable_portfolioLogReturn_zero

source

MeasureTheory.Integrable (fun (ω : Ω) => portfolioLogReturn X b (As 0 ω)) μ

Used by

theorem

InformationTheory.Shannon.Portfolio.identDistrib_portfolioLogReturn

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {m : ℕ} (μ : MeasureTheory.Measure Ω) (X : α → Fin m → ℝ) (b : Fin m → ℝ) (As : ℕ → Ω → α) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (As i) (As 0) μ μ) (i : ℕ) :

ProbabilityTheory.IdentDistrib (fun (ω : Ω) => portfolioLogReturn X b (As i ω)) (fun (ω : Ω) => portfolioLogReturn X b (As 0 ω)) μ μ

Used by

theorem

InformationTheory.Shannon.Portfolio.indepFun_portfolioLogReturn

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {m : ℕ} (μ : MeasureTheory.Measure Ω) (X : α → Fin m → ℝ) (b : Fin m → ℝ) (As : ℕ → Ω → α) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (As i) (As j) μ) :

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (fun (ω : Ω) => portfolioLogReturn X b (As i ω)) (fun (ω : Ω) => portfolioLogReturn X b (As j ω)) μ

Used by

theorem

InformationTheory.Shannon.Portfolio.seqLogWealth_div_tendsto_growthRate

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {m : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : α → Fin m → ℝ) (b : Fin m → ℝ) (As : ℕ → Ω → α) (hAs : ∀ (i : ℕ), Measurable (As i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (As i) (As j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (As i) (As 0) μ μ) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth X b As n ω / ↑n) Filter.atTop (nhds (growthRate (Gambling.lawPmf μ (As 0)) X b))

Operational log-optimal portfolio theorem (Cover–Thomas): for an i.i.d. market sequence As, a fixed rebalanced portfolio b under price relatives X, the time-averaged log-wealth growth (1/n)·log S_n converges almost surely to the growth rate growthRate (lawPmf μ (As 0)) X b, where lawPmf μ (As 0) is the law of a single outcome. @audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). lawPmf μ (As 0) is a genuine definitional binding (pushforward law of As 0), not a bundled (h : μ[…] = growthRate …) slot. hAs/hindep/hident and [IsProbabilityMeasure μ] are the SLLN regularity preconditions. Routes through strong_law_ae_real + the expectation→pmf bridge integral_comp_law; non-circular.

Used by

theorem

InformationTheory.Shannon.Portfolio.seqLogWealth_asymptotically_optimal

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {m : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : α → Fin m → ℝ) (b bs : Fin m → ℝ) (hb : b ∈ stdSimplex ℝ (Fin m)) (hbs : bs ∈ stdSimplex ℝ (Fin m)) (hpos : ∀ (a : α), ∀ c ∈ stdSimplex ℝ (Fin m), 0 < wealthRelative X c a) (As : ℕ → Ω → α) (hAs : ∀ (i : ℕ), Measurable (As i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (As i) (As j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (As i) (As 0) μ μ) (hKT : ∀ (i : Fin m), ∑ a : α, Gambling.lawPmf μ (As 0) a * X a i / wealthRelative X bs a ≤ 1) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth X b As n ω / ↑n) Filter.atTop (nhds (growthRate (Gambling.lawPmf μ (As 0)) X b)) ∧ Filter.Tendsto (fun (n : ℕ) => seqLogWealth X bs As n ω / ↑n) Filter.atTop (nhds (growthRate (Gambling.lawPmf μ (As 0)) X bs)) ∧ growthRate (Gambling.lawPmf μ (As 0)) X b ≤ growthRate (Gambling.lawPmf μ (As 0)) X bs

Operational asymptotic optimality (Cover–Thomas): a log-optimal (Kuhn–Tucker) portfolio bs is asymptotically optimal. Almost surely both the arbitrary portfolio b and bs have a growth rate, and the arbitrary portfolio does not beat bs. @audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). hKT is the first-order Kuhn–Tucker condition on bs alone (gradient inequalities ∀ i, ∑ a, p a · X a i / S_bs(a) ≤ 1), NOT the conclusion W(b) ≤ W(bs): it is bridged to global optimality by the concavity/Jensen content proved sorry-free in logOptimal_of_kuhnTucker (Cover–Thomas). Non-vacuous — a non-log-optimal bs fails hKT (by kuhnTucker_of_logOptimal), so the hypothesis genuinely pins the optimum rather than smuggling the comparison. hb/hbs are simplex membership, hpos is the log-domain positivity precondition; the two a.s. conjuncts come from H1 (×2) and the third deterministic inequality from the static theorem — no conjunct is passed as a hypothesis.

Used by