InformationTheory

InformationTheory.Shannon.Portfolio.StationaryMarket

source

Imports 5

Log-optimal portfolios over stationary ergodic markets (Cover–Thomas) #

For a stationary ergodic market driven by a measure-preserving ergodic shift T : Ω → Ω, with the price-relative vector at the first epoch given by an observation X : Ω → (Fin m → ℝ), an investor reinvesting all wealth with a fixed rebalanced portfolio b : Fin m → ℝ accumulates wealth whose log grows like ∑ i, log (b · X (T^[i] ω)). The time-averaged log-wealth growth converges almost surely to the expected log return ∫ ω, log (b · X ω) ∂μ. This is the stationary-ergodic counterpart of the i.i.d. operational theorem InformationTheory.Shannon.Portfolio.seqLogWealth_div_tendsto_growthRate, obtained by replacing the strong law of large numbers with the Birkhoff individual ergodic theorem.

Main definitions #

Main statements #

Implementation notes #

The proof is a direct application of the Birkhoff individual ergodic theorem InformationTheory.Shannon.birkhoff_ergodic_ae to the integrable observable stationaryLogReturn X b, mirroring the template InformationTheory.Shannon.birkhoffAverage_pmfLogCond_tendsto. The normalization matches the in-project birkhoffAverageReal, whose time average uses n + 1 terms (∑_{i=0}^{n}) over the denominator n + 1.

References #

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

InformationTheory.Shannon.Portfolio.stationaryLogReturn

source
{Ω : Type u_1} {m : ℕ} (X : Ω → Fin m → ℝ) (b : Fin m → ℝ) :
Ω → ℝ

The per-epoch log return log (b · X ω) = log (∑ j, b j · X ω j): the log growth factor of wealth when the price-relative vector is X ω and the portfolio is b.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.Portfolio.seqLogWealth_div_tendsto_stationary

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {m : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (hT_erg : Ergodic T μ) (X : Ω → Fin m → ℝ) (b : Fin m → ℝ) (hint : MeasureTheory.Integrable (stationaryLogReturn X b) μ) :
      ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range (n + 1), stationaryLogReturn X b (T^[i] ω)) / (↑n + 1)) Filter.atTop (nhds (∫ (ω : Ω), stationaryLogReturn X b ω ∂μ))

      Stationary ergodic log-optimal portfolio theorem (Cover–Thomas): for a measure-preserving ergodic shift T on a probability space, a fixed rebalanced portfolio b, and an integrable per-epoch log return, the Birkhoff time average of the log-wealth growth converges almost surely to the expected log return ∫ ω, log (b · X ω) ∂μ. @audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). Direct application of birkhoff_ergodic_ae; hT/hT_erg/hint are its ergodic-system and integrability preconditions, ∫ ω, stationaryLogReturn X b ω is a genuine definitional binding (the spatial mean), and the spelled-out range (n+1) / (n+1) average matches birkhoffAverageReal. Non-circular, no load-bearing hypothesis.

      Used by
        theorem

        InformationTheory.Shannon.Portfolio.stationaryLogReturn_integral_le_of_kuhnTucker

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {m : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → Fin m → ℝ) (b bs : Fin m → ℝ) (hb : b ∈ stdSimplex ℝ (Fin m)) (hpos_b : ∀ (ω : Ω), 0 < ∑ j : Fin m, b j * X ω j) (hpos_bs : ∀ (ω : Ω), 0 < ∑ j : Fin m, bs j * X ω j) (hint_b : MeasureTheory.Integrable (stationaryLogReturn X b) μ) (hint_bs : MeasureTheory.Integrable (stationaryLogReturn X bs) μ) (hint_coord : ∀ (i : Fin m), MeasureTheory.Integrable (fun (ω : Ω) => X ω i / ∑ j : Fin m, bs j * X ω j) μ) (hKT : ∀ (i : Fin m), ∫ (ω : Ω), X ω i / ∑ j : Fin m, bs j * X ω j ∂μ ≤ 1) :
        ∫ (ω : Ω), stationaryLogReturn X b ω ∂μ ≤ ∫ (ω : Ω), stationaryLogReturn X bs ω ∂μ

        Stationary asymptotic optimality (Cover–Thomas): a log-optimal portfolio bs satisfying the integral Kuhn–Tucker condition ∀ i, ∫ X_i / (bs · X) ∂μ ≤ 1 maximizes the expected log return: every simplex portfolio b has ∫ log (b · X) ≤ ∫ log (bs · X).

        Together with seqLogWealth_div_tendsto_stationary this gives the asymptotic dominance of bs over any fixed b: the almost-sure limits of the time-averaged log-wealth satisfy the same inequality. @audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]). hKT constrains only bs (per-coordinate integral stationarity, b-free), so it is the honest hypothesis of the Kuhn–Tucker sufficiency theorem, not the conclusion in disguise: the dominance is proved genuinely via the tangent bound log t ≤ t − 1 integrated against the wealth ratio, then ∫ R = ∑ i, b i · ∫ X_i/(bs·X) ≤ 1. Simplex/positivity/integrability hypotheses are regularity preconditions; non-circular, no load-bearing hypothesis.

        Used by