Skip to content

InformationTheory.Shannon.Portfolio.Universal

Imports 10

Cover's universal portfolio (Cover–Thomas) #

For a market on Fin (d + 1) stocks with a fixed data stream of price relatives xs : ℕ → Fin (d + 1) → ℝ, the wealth of a constant-rebalanced portfolio b on the simplex after n periods is constWealth xs b n = ∏ i < n, (b · xs i). Cover's universal portfolio averages the constant-rebalanced wealth uniformly over the simplex, giving universalWealth xs n = (∫ b, constWealth xs b n) / vol. The main result is that this achieves the same exponential growth rate as the best constant-rebalanced portfolio chosen in hindsight: the per-period regret (1 / n) · (log S*_n − log Ŝ_n) tends to 0.

The simplex is parametrized by its d free coordinates: the corner simplex cornerSimplex d = {y | 0 ≤ y ∧ ∑ y ≤ 1} carries the ambient Lebesgue measure of Fin d → ℝ, and simplexLift sends y to the full portfolio with last coordinate 1 − ∑ y. This makes the uniform measure on the simplex an honest, computable object (the intrinsic (d)-dimensional measure on the affine hyperplane ∑ b = 1 has no Mathlib API, whereas the corner parametrization only needs volume on Fin d → ℝ).

Main definitions #

cornerSimplex — the d-dimensional corner simplex in Fin d → ℝ.
simplexLift — lifts free coordinates y to a portfolio on Fin (d + 1).
constWealth — wealth ∏ i < n, (b · xs i) of a constant-rebalanced portfolio.
universalWealth — Cover's universal wealth, the uniform average over the simplex.
bestConstantWealth — the best constant-rebalanced wealth in hindsight, S*_n.
universalRegret — the per-period regret (log S*_n − log Ŝ_n) / n.

Main statements #

universal_portfolio_regret_tendsto_zero — the per-period regret of the universal portfolio tends to 0.

Implementation notes #

The regret theorem is derived from three analytic facts about the universal wealth — positivity, the average bound Ŝ_n ≤ S*_n, and Cover's shrink bound S*_n ≤ e · (n + 1) ^ d · Ŝ_n. The shrink bound uses MeasureTheory.Measure.addHaar_image_homothety: the homothety b ↦ (1 − λ) b* + λ b scales simplex volume by λ ^ d, and on its image the wealth stays within a factor (1 − λ) ^ n ≥ e⁻¹ of the optimum.

References #

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

def

InformationTheory.Shannon.Portfolio.cornerSimplex

(d : ℕ) :

Set (Fin d → ℝ)

The corner simplex {y : Fin d → ℝ | (∀ i, 0 ≤ y i) ∧ ∑ i, y i ≤ 1}, the domain of the d free coordinates of a portfolio on Fin (d + 1) stocks. It carries the ambient Lebesgue measure of Fin d → ℝ.

Equations

InformationTheory.Shannon.Portfolio.cornerSimplex d = {y : Fin d → ℝ | (∀ (i : Fin d), 0 ≤ y i) ∧ ∑ i : Fin d, y i ≤ 1}

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.simplexLift

{d : ℕ} (y : Fin d → ℝ) :

Fin (d + 1) → ℝ

Lift the free coordinates y : Fin d → ℝ to a full portfolio on Fin (d + 1) stocks by appending the last coordinate 1 − ∑ i, y i.

Equations

InformationTheory.Shannon.Portfolio.simplexLift y = Fin.snoc y (1 - ∑ i : Fin d, y i)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.constWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (b : Fin (d + 1) → ℝ) (n : ℕ) :

Wealth ∏ i < n, (b · xs i) of the constant-rebalanced portfolio b after n periods with price relatives xs.

Equations

InformationTheory.Shannon.Portfolio.constWealth xs b n = ∏ i ∈ Finset.range n, ∑ j : Fin (d + 1), b j * xs i j

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.universalWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (n : ℕ) :

Cover's universal wealth Ŝ_n: the uniform average of the constant-rebalanced wealth over the simplex, computed via the corner parametrization.

Equations

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

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.bestConstantWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (n : ℕ) :

The best constant-rebalanced wealth in hindsight S*_n = ⨆ b, constWealth xs b n, the supremum over the simplex.

Equations

InformationTheory.Shannon.Portfolio.bestConstantWealth xs n = ⨆ (b : ↑(stdSimplex ℝ (Fin (d + 1)))), InformationTheory.Shannon.Portfolio.constWealth xs (⇑b) n

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Portfolio.universalRegret

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (n : ℕ) :

The per-period regret (log S*_n − log Ŝ_n) / n of the universal portfolio.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.Portfolio.simplexLift_mem_stdSimplex

{d : ℕ} {y : Fin d → ℝ} (hy : y ∈ cornerSimplex d) :

simplexLift y ∈ stdSimplex ℝ (Fin (d + 1))

Used by

theorem

InformationTheory.Shannon.Portfolio.wealthFactor_pos

{d : ℕ} {xs : ℕ → Fin (d + 1) → ℝ} (hpos : ∀ (i : ℕ) (j : Fin (d + 1)), 0 < xs i j) {b : Fin (d + 1) → ℝ} (hb : b ∈ stdSimplex ℝ (Fin (d + 1))) (i : ℕ) :

0 < ∑ j : Fin (d + 1), b j * xs i j

Used by

theorem

InformationTheory.Shannon.Portfolio.constWealth_pos

{d : ℕ} {xs : ℕ → Fin (d + 1) → ℝ} (hpos : ∀ (i : ℕ) (j : Fin (d + 1)), 0 < xs i j) {b : Fin (d + 1) → ℝ} (hb : b ∈ stdSimplex ℝ (Fin (d + 1))) (n : ℕ) :

0 < constWealth xs b n

Used by

theorem

InformationTheory.Shannon.Portfolio.isCompact_cornerSimplex

{d : ℕ} :

IsCompact (cornerSimplex d)

Used by

theorem

InformationTheory.Shannon.Portfolio.cornerSimplex_nonempty

{d : ℕ} :

(cornerSimplex d).Nonempty

Used by

theorem

InformationTheory.Shannon.Portfolio.measurableSet_cornerSimplex

{d : ℕ} :

MeasurableSet (cornerSimplex d)

Used by

theorem

InformationTheory.Shannon.Portfolio.volume_cornerSimplex_pos

{d : ℕ} :

0 < MeasureTheory.volume (cornerSimplex d)

Used by

theorem

InformationTheory.Shannon.Portfolio.volume_cornerSimplex_ne_top

{d : ℕ} :

MeasureTheory.volume (cornerSimplex d) ≠ ⊤

Used by

theorem

InformationTheory.Shannon.Portfolio.volume_cornerSimplex_toReal_pos

{d : ℕ} :

0 < (MeasureTheory.volume (cornerSimplex d)).toReal

Used by

theorem

InformationTheory.Shannon.Portfolio.continuous_liftWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (n : ℕ) :

Continuous fun (y : Fin d → ℝ) => constWealth xs (simplexLift y) n

Used by

theorem

InformationTheory.Shannon.Portfolio.integrableOn_liftWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (n : ℕ) :

MeasureTheory.IntegrableOn (fun (y : Fin d → ℝ) => constWealth xs (simplexLift y) n) (cornerSimplex d) MeasureTheory.volume

Used by

theorem

InformationTheory.Shannon.Portfolio.simplexLift_init

{d : ℕ} {b : Fin (d + 1) → ℝ} (hb : b ∈ stdSimplex ℝ (Fin (d + 1))) :

simplexLift (Fin.init b) = b

Used by

theorem

InformationTheory.Shannon.Portfolio.init_mem_cornerSimplex

{d : ℕ} {b : Fin (d + 1) → ℝ} (hb : b ∈ stdSimplex ℝ (Fin (d + 1))) :

Fin.init b ∈ cornerSimplex d

Used by

theorem

InformationTheory.Shannon.Portfolio.bestConstantWealth_attained

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (n : ℕ) :

∃ y ∈ cornerSimplex d, bestConstantWealth xs n = constWealth xs (simplexLift y) n ∧ ∀ z ∈ cornerSimplex d, constWealth xs (simplexLift z) n ≤ bestConstantWealth xs n

The best constant-rebalanced wealth is attained at a maximizer over the corner simplex, and dominates the lifted wealth of every corner point.

Used by

theorem

InformationTheory.Shannon.Portfolio.simplexLift_smul_add

{d : ℕ} (lam : ℝ) (y z : Fin d → ℝ) :

simplexLift ((1 - lam) • y + lam • z) = (1 - lam) • simplexLift y + lam • simplexLift z

Used by

theorem

InformationTheory.Shannon.Portfolio.exp_neg_one_le_shrink

(n : ℕ) :

Real.exp (-1) ≤ (1 - 1 / (↑n + 1)) ^ n

Real inequality behind the shrink constant: (1 - 1/(n+1)) ^ n ≥ e⁻¹.

Used by

theorem

InformationTheory.Shannon.Portfolio.universalWealth_pos

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (hpos : ∀ (i : ℕ) (j : Fin (d + 1)), 0 < xs i j) (n : ℕ) :

0 < universalWealth xs n

Positivity of the universal wealth: with strictly positive price relatives every constant-rebalanced wealth is positive, and the uniform average over the positive-measure corner simplex stays positive.

@audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). hpos regularity.

Used by

theorem

InformationTheory.Shannon.Portfolio.universalWealth_le_bestConstantWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (_hpos : ∀ (i : ℕ) (j : Fin (d + 1)), 0 < xs i j) (n : ℕ) :

universalWealth xs n ≤ bestConstantWealth xs n

The universal wealth never exceeds the best constant-rebalanced wealth: Ŝ_n is a uniform average of values constWealth xs (simplexLift y) n ≤ S*_n.

@audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). _hpos is unused (dominance holds without positivity); underscored to keep the uniform core interface.

Used by

theorem

InformationTheory.Shannon.Portfolio.bestConstantWealth_le_mul_universalWealth

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (hpos : ∀ (i : ℕ) (j : Fin (d + 1)), 0 < xs i j) (n : ℕ) :

bestConstantWealth xs n ≤ Real.exp 1 * (↑n + 1) ^ d * universalWealth xs n

Cover's shrink bound: the best constant-rebalanced wealth exceeds the universal wealth by at most a factor e · (n + 1) ^ d. The homothety b ↦ (1 − 1/(n+1)) b* + (1/(n+1)) b scales simplex volume by (n + 1)⁻ᵈ (MeasureTheory.Measure.addHaar_image_homothety) and keeps the wealth within (1 − 1/(n+1)) ^ n ≥ e⁻¹ of the optimum.

@audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). hpos regularity; the shrink bound is genuine (homothety volume scaling + setIntegral monotonicity).

Used by

theorem

InformationTheory.Shannon.Portfolio.universal_portfolio_regret_tendsto_zero

{d : ℕ} (xs : ℕ → Fin (d + 1) → ℝ) (hpos : ∀ (i : ℕ) (j : Fin (d + 1)), 0 < xs i j) :

Filter.Tendsto (fun (n : ℕ) => universalRegret xs n) Filter.atTop (nhds 0)

(Cover–Thomas): the per-period regret of the universal portfolio relative to the best constant-rebalanced portfolio chosen in hindsight tends to 0.

@audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). hpos (positive price relatives) is a regularity precondition; the squeeze is proven from the three analytic cores, none bundled into a hypothesis.

Used by