Measurable selection of an argmax of a concave Carathéodory function over the standard simplex. For F measurable in ω (for each fixed portfolio b), continuous and concave in b on the simplex, there is a measurable bstar : Ω → (Fin m → ℝ) picking, for each ω, a point of the simplex that maximizes F ω over the simplex.

The domain-nonemptiness hypothesis [Nonempty (Fin m)] (i.e. m ≥ 1) is a regularity precondition: for m = 0 the simplex is empty and no selection into it exists.

@audit:ok

Per-epoch log return of a causal portfolio bstar (past-measurable, hence ω-dependent) under price relatives X: log (∑ j, bstar ω j · X ω j). For a constant portfolio this specializes to stationaryLogReturn X b.

Expected growth of the stagewise conditional log-optimal portfolio: at stage k, the expected log return ∫ log (bstar k · X) ∂μ of the past-measurable portfolio bstar k. By integral_condExp this equals ∫ μ[log (bstar k · X) | ℱ k] ∂μ, the mean conditional-optimal growth rate.

Infinite-past optimal growth W_∞ := ⨆ k, condOptGrowth k: the supremum of the increasing sequence of conditional-optimal expected growths.

Existence of a stagewise conditional log-optimal portfolio sequence: for each stage k there is a past-ℱ k-measurable simplex portfolio bstar k whose conditional growth dominates, in conditional expectation given ℱ k, that of every ℱ k-measurable simplex competitor c. This is the conditional (past-measurable) form of the measurable-argmax gateway exists_measurable_argmax_on_stdSimplex, applied to the conditional growth objective b ↦ ∫ y, log (b · X y) ∂(condExpKernel μ (ℱ k) ω), the expected log-return against the regular conditional law given ℱ k. The hpos/hint hypotheses are market-regularity preconditions (positivity for the log domain, integrability of simplex log-returns); [StandardBorelSpace Ω] [Nonempty Ω] make the regular conditional distribution condExpKernel available. The gateway is fed a good-set patch of the objective (the true objective where the envelope ∑ⱼ |log Xⱼ| is condExpKernel-integrable, 0 off that co-null set) so that continuity and concavity in b hold for every ω; the conditional dominance then follows from the pull-out identity μ[log (c · X) | ℱ k] ω = ∫ y, log (c ω · X y) ∂(condExpKernel μ (ℱ k) ω), obtained because an ℱ k-measurable c is condExpKernel-a.e. constant.

@audit:ok

Monotonicity of the conditional-optimal expected growth: conditioning on more past information (larger k) can only increase the optimal expected growth. The hdom conditional optimality is a property of the constructed selection bstar (supplied by exists_condLogOptimalSeq), and monotonicity is derived from it via integral_condExp and integral_mono_ae — not assumed.

@audit:ok

Boundedness above of the conditional-optimal expected growth, from a uniform expected-return bound hUB (a market-regularity/integrability precondition: expected simplex log-returns are bounded by a common constant).

@audit:ok

The conditional-optimal expected growth converges monotonically to the infinite-past optimal growth W_∞ (Cover–Thomas). There is a stagewise conditional log-optimal portfolio sequence bstar (past-measurable, dominating all past-measurable competitors) whose expected growth condOptGrowth is monotone, bounded above, and converges to its supremum condOptGrowthInfty = W_∞. The monotone-convergence conclusion is proved, not assumed: monotonicity from the conditional optimality of bstar, boundedness from the regularity envelope hUB, convergence via tendsto_atTop_ciSup. The stagewise conditional log-optimal selection is supplied by exists_condLogOptimalSeq. The Algoet–Cover sandwich consumes bstar/condOptGrowth/condOptGrowthInfty for (1/n) log S*_n → W_∞.

@audit:ok

Gateway identity for the stationary-market W_∞ AEP (Cover–Thomas): the growth-rate integral of the infinite-past (⨆ k, ℱ k) conditional log-optimal portfolio bstarInf equals the increasing limit W_∞ = condOptGrowthInfty of the stagewise conditional-optimal growths. This is the identity that lets the Algoet–Cover sandwich for (1/n) log S*_n → W_∞ reduce to a direct Birkhoff application.

Two inclusions bracket the value. The upper inclusion condOptGrowthInfty ≤ ∫ log (bstarInf · X) uses that each bstar k is ⨆ j, ℱ j-measurable (the filtration is increasing) and hence a legal competitor against bstarInf at the infinite-past level; integrating the conditional dominance collapses both conditional expectations to their integrals. The lower inclusion ∫ log (bstarInf · X) ≤ condOptGrowthInfty approximates bstarInf by its stagewise conditional expectations c_k := μ[bstarInf | ℱ k] (coordinatewise), which are ℱ k-measurable and a.e. simplex-valued (conditional expectation preserves nonnegativity and the unit coordinate sum); patched to be everywhere simplex-valued they are legal stage-k competitors, so ∫ log (c_k · X) ≤ condOptGrowth k ≤ condOptGrowthInfty. Lévy's upward theorem (Integrable.tendsto_ae_condExp) gives c_k → bstarInf a.e., and dominated convergence (envelope ∑ⱼ |log Xⱼ|) passes the bound to the limit.

bstarInf and its ⨆ j, ℱ j-conditional dominance are received as hypotheses (constructed separately, e.g. by instantiating exists_condLogOptimalSeq at the constant filtration fun _ ↦ ⨆ j, ℱ j); this proves only the identity, not the existence. The hpos/hint hypotheses are market-regularity preconditions.

@audit:ok

Existence of an infinite-past (⨆ j, ℱ j) conditional log-optimal portfolio bstarInf: instantiate exists_condLogOptimalSeq at the constant filtration Filtration.const ℕ (⨆ j, ℱ j) (every stage is the infinite past) and read off stage 0.

@audit:ok

A fixed infinite-past conditional log-optimal portfolio bstarInf achieves the optimal growth rate W_∞ = condOptGrowthInfty as the almost-sure Birkhoff time average of its per-epoch log return under a measure-preserving ergodic shift T (Cover–Thomas). The optimal sequence bstar and its infinite-past companion bstarInf are constructed internally (exists_condOptGrowth_tendsto_condOptGrowthInfty and exists_infPast_condLogOptimal) and their conditional-dominance properties are established, so the conclusion carries no optimization hypothesis; hpos/hint/hUB/hT/hT_erg are market-regularity/ergodicity preconditions. The specialization of ℱ to the market-past filtration and T to the shift (giving the verbatim CT 16.5.1 statement) is a downstream framing step.

@audit:ok

Conditional Kuhn–Tucker inequality for the infinite-past (⨆ j, ℱ j) conditional log-optimal portfolio bstarInf (Cover–Thomas). For every ⨆ j, ℱ j-measurable simplex competitor c, the conditional expectation of the one-step wealth ratio (∑ⱼ cⱼ Xⱼ) / (∑ⱼ bstarInfⱼ Xⱼ) given the infinite past is at most 1. This is the multiplicative form of the additive dominance hInf_dom — the one-step supermartingale bound at the heart of the growing-memory wealth-ratio process.

The additive-to-multiplicative passage is the perturbation/first-order argument: for λ ∈ (0, 1] the convex mix bλ := (1 − λ) bstarInf + λ c is a legal ⨆ j, ℱ j-measurable simplex competitor, so hInf_dom bλ gives μ[log ((∑ bλ·X)/(∑ bstarInf·X)) | ⨆ ℱ] ≤ᵐ 0, i.e. μ[log (1 + λ (r − 1)) | ⨆ ℱ] ≤ᵐ 0 where r is the wealth ratio. Dividing by λ and letting λ → 0 (dominated convergence, since log r ≤ log (1 + λ (r − 1))/λ ≤ r − 1) yields μ[r − 1 | ⨆ ℱ] ≤ᵐ 0, hence μ[r | ⨆ ℱ] ≤ᵐ 1. The hint_coord hypothesis (integrability of the coordinate ratios Xᵢ / (∑ bstarInf·X)) is a market-regularity precondition, mirroring the fixed-b Kuhn–Tucker theorem stationaryLogReturn_integral_le_of_kuhnTucker; it makes the wealth ratio r integrable so the conditional expectation is genuine. hpos/hint are the market-regularity positivity/integrability preconditions; [StandardBorelSpace Ω] [Nonempty Ω] are inherited for compatibility with the infinite-past filtration constructions. @audit:ok