InformationTheory.Shannon.Portfolio.StationaryWinftyConcrete

Imports 3

Concrete two-sided market instantiation of the growing-memory `W_∞` AEP (Cover–Thomas) #

The abstract headline growingMemory_logWealth_tendsto_condOptGrowthInfty is stated for an arbitrary increasing filtration ℱ and measure-preserving map T, conditional on two measurability-only shift/past coherence hypotheses (hcoh, hcoh_inf) linking the filtration to the shift orbit. This file discharges both coherences for the concrete two-sided market — sequence space Ω = ∀ _ : ℤ, Fin m → ℝ, shift T = shiftZ, coordinate-0 price relative X = coord0, and the finite-past filtration ℱ = pastFiltration — and produces the concrete headline growingMemory_logWealth_tendsto_condOptGrowthInfty_concrete with the two coherences removed (every remaining hypothesis is a market-regularity/ergodicity precondition).

The discharge is bounded plumbing: each coherence component is a finite-window function pulled back through a shift, so it factors as g ∘ shiftZ^[k+1] with g measurable w.r.t. the negative-past σ-algebra, using the generic comap-through-shift factorization.

Local shift-iterate helpers #

Replicated from the (privately scoped) engine in SMB/AlgoetCover/TwoSidedRatio.lean to keep the import surface light (shiftZ_iterate_apply is public in Core, so it is used directly).

Coordinate measurability in the past σ-algebras #

Generic comap-through-shift factorization #

The two coherence discharges #

Concrete headline #

theorem

InformationTheory.Shannon.Portfolio.growingMemory_logWealth_tendsto_condOptGrowthInfty_concrete

source

{m : ℕ} (μ : MeasureTheory.Measure (ℤ → Fin m → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hT : MeasureTheory.MeasurePreserving TwoSided.shiftZ μ μ) (hT_erg : Ergodic TwoSided.shiftZ μ) [Nonempty (Fin m)] (hpos : ∀ (ω : ℤ → Fin m → ℝ), ∀ b ∈ stdSimplex ℝ (Fin m), 0 < ∑ j : Fin m, b j * TwoSided.coord0 ω j) (hint : ∀ (c : (ℤ → Fin m → ℝ) → Fin m → ℝ), Measurable c → (∀ (ω : ℤ → Fin m → ℝ), c ω ∈ stdSimplex ℝ (Fin m)) → MeasureTheory.Integrable (causalLogReturn TwoSided.coord0 c) μ) (bstar : ℕ → (ℤ → Fin m → ℝ) → Fin m → ℝ) (hbstar_meas : ∀ (k : ℕ), MeasureTheory.StronglyMeasurable (bstar k)) (hbstar_simplex : ∀ (k : ℕ) (ω : ℤ → Fin m → ℝ), bstar k ω ∈ stdSimplex ℝ (Fin m)) (hbstar_dom : ∀ (k : ℕ) (c : (ℤ → Fin m → ℝ) → Fin m → ℝ), MeasureTheory.StronglyMeasurable c → (∀ (ω : ℤ → Fin m → ℝ), c ω ∈ stdSimplex ℝ (Fin m)) → μ[causalLogReturn TwoSided.coord0 c | ↑TwoSided.pastFiltration k] ≤ᵐ[μ] μ[causalLogReturn TwoSided.coord0 (bstar k) | ↑TwoSided.pastFiltration k]) (hint_coord : ∀ (i : ℕ) (coord : Fin m), MeasureTheory.Integrable (fun (ω : ℤ → Fin m → ℝ) => TwoSided.coord0 ω coord / ∑ j : Fin m, bstar i ω j * TwoSided.coord0 ω j) μ) (hUB : ∃ (C : ℝ), ∀ (c : (ℤ → Fin m → ℝ) → Fin m → ℝ), (∀ (ω : ℤ → Fin m → ℝ), c ω ∈ stdSimplex ℝ (Fin m)) → MeasureTheory.Integrable (causalLogReturn TwoSided.coord0 c) μ → ∫ (ω : ℤ → Fin m → ℝ), causalLogReturn TwoSided.coord0 c ω ∂μ ≤ C) (bstarInf : (ℤ → Fin m → ℝ) → Fin m → ℝ) (hInf_meas : MeasureTheory.StronglyMeasurable bstarInf) (hInf_simplex : ∀ (ω : ℤ → Fin m → ℝ), bstarInf ω ∈ stdSimplex ℝ (Fin m)) (hint_coord_inf : ∀ (i : Fin m), MeasureTheory.Integrable (fun (ω : ℤ → Fin m → ℝ) => TwoSided.coord0 ω i / ∑ j : Fin m, bstarInf ω j * TwoSided.coord0 ω j) μ) (hInf_dom : ∀ (c : (ℤ → Fin m → ℝ) → Fin m → ℝ), MeasureTheory.StronglyMeasurable c → (∀ (ω : ℤ → Fin m → ℝ), c ω ∈ stdSimplex ℝ (Fin m)) → μ[causalLogReturn TwoSided.coord0 c | ⨆ (j : ℕ), ↑TwoSided.pastFiltration j] ≤ᵐ[μ] μ[causalLogReturn TwoSided.coord0 bstarInf | ⨆ (j : ℕ), ↑TwoSided.pastFiltration j]) :

∀ᵐ (ω : ℤ → Fin m → ℝ) ∂μ, Filter.Tendsto (fun (n : ℕ) => growingMemoryLogAvg TwoSided.coord0 bstar TwoSided.shiftZ n ω) Filter.atTop (nhds (condOptGrowthInfty μ TwoSided.coord0 bstar))

Growing-memory W_∞ AEP (Cover–Thomas) for the concrete two-sided market: the growing-memory log-wealth average converges almost surely to the infinite-past optimal growth rate W_∞ = condOptGrowthInfty. The sequence space is Ω = ∀ _ : ℤ, Fin m → ℝ, the dynamics is the two-sided shift shiftZ, the per-epoch price relative is the coordinate-0 projection coord0, and the filtration is the finite-past pastFiltration. The two shift/past coherences of the abstract statement are discharged internally; all remaining hypotheses are market-regularity/ergodicity preconditions (measure preservation, ergodicity, simplex membership, positivity, integrability, conditional dominance). @audit:ok

Used by