InformationTheory.Shannon.Gambling.OperationalSequences

Imports 7

Operational gambling over horse-race sequences (Cover–Thomas) #

For an i.i.d. sequence of horse races Xs : ℕ → Ω → α on a finite alphabet α, a gambler reinvesting all wealth with a fixed bet b : α → ℝ and odds o : α → ℝ accumulates wealth whose log grows like ∑ i, log (b (Xs i) · o (Xs i)). The operational (sequence-level) result is that the time-averaged log-wealth growth converges almost surely to the doubling rate W(b, o, p), where p is the law of a single race Xs 0. This is the strong-law counterpart of the single-shot expectation theorem doublingRate_le_proportional, and a near-clone of the asymptotic equipartition property aep_ae.

Main definitions #

betLogReturn — the alphabet-side per-race log return g x = log (b x · o x).
seqLogWealth — the log-wealth after n races, log S_n = ∑ i, betLogReturn b o (Xs i).
lawPmf — the pmf (law) p x = (μ.map X).real {x} of a finite random variable X.

Main statements #

seqLogWealth_div_tendsto_doublingRate — for a general bet, (1/n)·log S_n converges almost surely to doublingRate b o (lawPmf μ (Xs 0)).
seqLogWealth_proportional_asymptotically_optimal — the proportional (Kelly) bet b = p is asymptotically optimal: almost surely both growth rates exist and the arbitrary bet does not beat the Kelly bet.

Implementation notes #

The proof reuses the strong law ProbabilityTheory.strong_law_ae_real applied to the sequence fun i ω ↦ betLogReturn b o (Xs i ω), exactly as aep_ae applies it to the log-likelihood sequence. The only non-mechanical step is identifying the strong-law limit μ[betLogReturn b o ∘ Xs 0] with doublingRate b o (lawPmf μ (Xs 0)), via the discrete-expectation bridge integral_comp_law (push-forward integral_map followed by the finite-sum collapse integral_fintype).

References #

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

noncomputable def

InformationTheory.Shannon.Gambling.betLogReturn

source

{α : Type u_2} (b o : α → ℝ) :

α → ℝ

The alphabet-side per-race log return g x = log (b x · o x): the log growth factor of wealth when the race outcome is x, the bet is b, and the odds are o.

Equations

InformationTheory.Shannon.Gambling.betLogReturn b o x = Real.log (b x * o x)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Gambling.seqLogWealth

source

{Ω : Type u_1} {α : Type u_2} (b o : α → ℝ) (Xs : ℕ → Ω → α) (n : ℕ) :

Ω → ℝ

The log-wealth after n races starting from unit wealth, log S_n = ∑ i < n, betLogReturn b o (Xs i ω).

Equations

InformationTheory.Shannon.Gambling.seqLogWealth b o Xs n ω = ∑ i ∈ Finset.range n, InformationTheory.Shannon.Gambling.betLogReturn b o (Xs i ω)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.Gambling.lawPmf

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : Ω → α) :

α → ℝ

The pmf (law) of a finite random variable X, p x = (μ.map X).real {x}.

Equations

InformationTheory.Shannon.Gambling.lawPmf μ X x = (MeasureTheory.Measure.map X μ).real {x}

Instances For

Used by

theorem

InformationTheory.Shannon.Gambling.measurable_betLogReturn

source

{α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (b o : α → ℝ) :

Measurable (betLogReturn b o)

Used by

theorem

InformationTheory.Shannon.Gambling.integral_comp_law

source

∫ (ω : Ω), g (X ω) ∂μ = ∑ x : α, (MeasureTheory.Measure.map X μ).real {x} * g x

Discrete-expectation bridge: the expectation of g ∘ X collapses to the finite sum against the law of X, ∫ ω, g (X ω) ∂μ = ∑ x, (μ.map X).real {x} · g x.

Used by

theorem

InformationTheory.Shannon.Gambling.integrable_betLogReturn_zero

source

MeasureTheory.Integrable (fun (ω : Ω) => betLogReturn b o (Xs 0 ω)) μ

Used by

theorem

InformationTheory.Shannon.Gambling.identDistrib_betLogReturn

source

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

ProbabilityTheory.IdentDistrib (fun (ω : Ω) => betLogReturn b o (Xs i ω)) (fun (ω : Ω) => betLogReturn b o (Xs 0 ω)) μ μ

Used by

theorem

InformationTheory.Shannon.Gambling.indepFun_betLogReturn

source

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

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (fun (ω : Ω) => betLogReturn b o (Xs i ω)) (fun (ω : Ω) => betLogReturn b o (Xs j ω)) μ

Used by

theorem

InformationTheory.Shannon.Gambling.lawPmf_mem_stdSimplex

source

lawPmf μ X ∈ stdSimplex ℝ α

Used by

theorem

InformationTheory.Shannon.Gambling.seqLogWealth_div_tendsto_doublingRate

source

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

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth b o Xs n ω / ↑n) Filter.atTop (nhds (doublingRate b o (lawPmf μ (Xs 0))))

For an i.i.d. horse-race sequence Xs and a fixed bet b under odds o, the time-averaged log-wealth growth (1/n)·log S_n converges almost surely to the doubling rate doublingRate b o (lawPmf μ (Xs 0)), where lawPmf μ (Xs 0) is the law of a single race (Cover–Thomas). sorryAx-free ([propext, Classical.choice, Quot.sound]). lawPmf μ (Xs 0) is a definitional binding (the pushforward law of Xs 0, computed from the existing μ/Xs), NOT a bundled hypothesis: there is no (h : μ[X 0] = doublingRate …) slot. [IsProbabilityMeasure μ]/hXs/hindep/hident are regularity preconditions of the SLLN. Routes through strong_law_ae_real

the non-trivial expectation→pmf bridge integral_comp_law; not vacuous/circular. @audit:ok

Used by

theorem

InformationTheory.Shannon.Gambling.seqLogWealth_proportional_div_tendsto

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (o : α → ℝ) (ho : ∀ (x : α), 0 < o x) (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth (lawPmf μ (Xs 0)) o Xs n ω / ↑n) Filter.atTop (nhds (∑ x : α, lawPmf μ (Xs 0) x * Real.log (o x) - ∑ x : α, (lawPmf μ (Xs 0) x).negMulLog))

The sequence-level growth rate of the proportional (Kelly) bet b = p in closed form, W(p, o, p) = ∑ x, p x · log (o x) − H(p). sorryAx-free ([propext, Classical.choice, Quot.sound]). lawPmf μ (Xs 0) is a definitional binding; ho (positive odds) is a log 0 = 0-convention correctness precondition, not load-bearing. The closed form is a rewrite of seqLogWealth_div_tendsto_doublingRate's limit via doublingRate_proportional_eq, non-circular. @audit:ok

Used by

theorem

InformationTheory.Shannon.Gambling.seqLogWealth_proportional_asymptotically_optimal

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (b o : α → ℝ) (hb : b ∈ stdSimplex ℝ α) (hb_pos : ∀ (x : α), 0 < b x) (ho : ∀ (x : α), 0 < o x) (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth b o Xs n ω / ↑n) Filter.atTop (nhds (doublingRate b o (lawPmf μ (Xs 0)))) ∧ Filter.Tendsto (fun (n : ℕ) => seqLogWealth (lawPmf μ (Xs 0)) o Xs n ω / ↑n) Filter.atTop (nhds (doublingRate (lawPmf μ (Xs 0)) o (lawPmf μ (Xs 0)))) ∧ doublingRate b o (lawPmf μ (Xs 0)) ≤ doublingRate (lawPmf μ (Xs 0)) o (lawPmf μ (Xs 0))

The proportional (Kelly) bet b = p is asymptotically optimal at the sequence level (Cover–Thomas): almost surely both the arbitrary full-support bet b and the Kelly bet p have a growth rate, and the arbitrary bet does not beat the Kelly bet. sorryAx-free ([propext, Classical.choice, Quot.sound]). lawPmf μ (Xs 0) is a definitional binding; hb/hb_pos/ho (full-support bet + positive odds) are the same correctness preconditions as the parent doublingRate_le_proportional, not load-bearing. The two a.s.-convergence conjuncts come from seqLogWealth_div_tendsto_doublingRate (×2) and the third (deterministic) inequality from doublingRate_le_proportional; no conjunct is smuggled in as a hypothesis. @audit:ok

Used by

theorem

InformationTheory.Shannon.Gambling.seqLogWealth_tendsto_atTop_of_pos_doublingRate

source

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth b o Xs n ω) Filter.atTop Filter.atTop

If the doubling rate is positive, the log-wealth log S_n diverges to +∞ almost surely, i.e. wealth grows exponentially: a positive doubling rate means the gambler gets rich (Cover–Thomas). sorryAx-free ([propext, Classical.choice, Quot.sound]). Pure corollary of seqLogWealth_div_tendsto_doublingRate via log S_n = (log S_n / n)·n + Tendsto.pos_mul_atTop; the limit W* comes from that theorem's conclusion, NOT a bundled (h : Tendsto … (𝓝 W*)) hypothesis. hpos : 0 < W* is a sign precondition (the divergence direction depends on the sign; at W*=0 the direction is indeterminate), not load-bearing. Conclusion Tendsto … atTop is a real claim, not vacuous; the n=0 boundary is handled via eventually_gt_atTop 0. @audit:ok

Used by

theorem

InformationTheory.Shannon.Gambling.seqLogWealth_tendsto_atBot_of_neg_doublingRate

source

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => seqLogWealth b o Xs n ω) Filter.atTop Filter.atBot

If the doubling rate is negative, the log-wealth log S_n diverges to −∞ almost surely, i.e. wealth decays to zero exponentially: a negative doubling rate means the gambler goes broke (Cover–Thomas). sorryAx-free ([propext, Classical.choice, Quot.sound]). Pure corollary of seqLogWealth_div_tendsto_doublingRate via log S_n = (log S_n / n)·n + Tendsto.neg_mul_atTop; the limit W* comes from that theorem's conclusion, NOT a bundled (h : Tendsto … (𝓝 W*)) hypothesis. hneg : W* < 0 is a sign precondition (the divergence direction depends on the sign; at W*=0 the direction is indeterminate), not load-bearing. Conclusion Tendsto … atBot is a real claim, not vacuous; the n=0 boundary is handled via eventually_gt_atTop 0. @audit:ok

Used by