InformationTheory

InformationTheory.Shannon.Gambling.Basic

source

Imports 6

Kelly gambling and the doubling rate (Cover–Thomas) #

For a horse race on a finite alphabet α with true win probabilities p : α → ℝ, betting fractions b : α → ℝ, and odds o : α → ℝ (payoff per unit staked on x), the doubling rate of the bet b is the expected log-wealth growth per race,

W(b, o, p) = ∑ x, p x · log (b x · o x).

The main result is that the proportional (Kelly) bet b = p maximizes the doubling rate, and does so uniquely.

Main definitions #

  • doublingRate — the doubling rate ∑ x, p x · log (b x · o x).

Main statements #

Implementation notes #

Everything reduces to the finite-alphabet KL divergence klDivPmf of InformationTheory.Shannon.CsiszarProjection, mirroring the maximum-entropy proof entropy_le_gibbs_of_constraints. The key identity is

W(p, o, p) − W(b, o, p) = ∑ x, p x · (log (p x) − log (b x)) = klDivPmf p b ≥ 0,

where the log (o x) terms cancel. Non-negativity of the gap is klDivPmf_nonneg, and the equality condition is klDivPmf_eq_zero_iff_pmf.

The argument order klDivPmf p b (true distribution first, bet second) is load-bearing: the log-difference and vanishing lemmas require the second argument to be positive, which is provided by the full-support bet hypothesis hb_pos, not by p.

Positivity of b is a genuine correctness precondition, not a bundling of the proof core: since Lean sets Real.log 0 = 0, a zero bet on a live horse (b x = 0, p x > 0) would contribute 0 instead of the true −∞ (ruin), which would make the inequality false. It plays the same role as the full-support reference pmf in the maximum-entropy theorems.

References #

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

InformationTheory.Shannon.Gambling.doublingRate

source
{α : Type u_1} [Fintype α] (b o p : α → ℝ) :
ℝ

The doubling rate of a bet b under odds o when the true win law is p: the expected log growth of wealth per race, ∑ x, p x · log (b x · o x).

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.Gambling.doublingRate_proportional_eq

      source
      {α : Type u_1} [Fintype α] (p o : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (ho : ∀ (x : α), 0 < o x) :
      doublingRate p o p = ∑ x : α, p x * Real.log (o x) - ∑ x : α, (p x).negMulLog

      Closed form for the doubling rate of the proportional (Kelly) bet b = p: W(p, o, p) = ∑ x, p x · log (o x) − H(p), where H(p) = ∑ x, negMulLog (p x).

      Used by
        theorem

        InformationTheory.Shannon.Gambling.doublingRate_gap_eq_klDivPmf

        source
        {α : Type u_1} [Fintype α] (p b o : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (hb : b ∈ stdSimplex ℝ α) (hb_pos : ∀ (x : α), 0 < b x) (ho : ∀ (x : α), 0 < o x) :
        doublingRate p o p - doublingRate b o p = CsiszarProjection.klDivPmf p b

        The gap between the optimal and an arbitrary doubling rate is a KL divergence: W(p, o, p) − W(b, o, p) = klDivPmf p b. The log (o x) terms cancel.

        Used by
          theorem

          InformationTheory.Shannon.Gambling.doublingRate_le_proportional

          source
          {α : Type u_1} [Fintype α] (p b o : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (hb : b ∈ stdSimplex ℝ α) (hb_pos : ∀ (x : α), 0 < b x) (ho : ∀ (x : α), 0 < o x) :
          doublingRate b o p ≤ doublingRate p o p

          Proportional (Kelly) betting maximizes the doubling rate: for any full-support bet b and positive odds o, W(b, o, p) ≤ W(p, o, p). This is Cover–Thomas. @audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]); hb_pos is a genuine correctness precondition (counterexample without it: p=(1/2,1/2), o=(2,2), b=(1,0) gives W(b,o,p)=(1/2)log 2 > 0 = W(p,o,p) since log 0 = 0 erases ruin), not load-bearing; gap = klDivPmf p b ≥ 0.

          Used by
            theorem

            InformationTheory.Shannon.Gambling.doublingRate_eq_proportional_iff

            source
            {α : Type u_1} [Fintype α] (p b o : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (hb : b ∈ stdSimplex ℝ α) (hb_pos : ∀ (x : α), 0 < b x) (ho : ∀ (x : α), 0 < o x) :
            doublingRate b o p = doublingRate p o p ↔ b = p

            The doubling rate is maximized by b iff b is the proportional (Kelly) bet b = p. @audit:ok — sorryAx-free ([propext, Classical.choice, Quot.sound]); equality direction via klDivPmf_eq_zero_iff_pmf hp hb hb_pos (klDivPmf p b = 0 ↔ p = b) flipped by eq_comm, non-circular.

            Used by
              theorem

              InformationTheory.Shannon.Gambling.doublingRate_proportional_add_entropy

              source
              {α : Type u_1} [Fintype α] (p o : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (ho : ∀ (x : α), 0 < o x) :
              doublingRate p o p + ∑ x : α, (p x).negMulLog = ∑ x : α, p x * Real.log (o x)

              Conservation law: the optimal doubling rate plus the entropy of p equals the expected log-odds, W(p, o, p) + H(p) = ∑ x, p x · log (o x).

              Used by