KellyCriterion

import Mathlib

/-!
The Kelly criterion for an even-money binary bet.

Source: J. L. Kelly Jr., *A New Interpretation of Information Rate*, Bell System Technical
Journal **35** (1956) 917-926, the "simplest case" of Section 4 (even-money bet, no track
take): a gambler with win probability `p` stakes a fixed fraction `ℓ` of current wealth on
each of a sequence of independent bets.

Kelly writes the exponential rate of growth as `G = p log(1+ℓ) + q log(1-ℓ)` with `q = 1-p`,
maximised at `ℓ = p - q`, giving `G_max = 1 + p log p + q log q` in BITS. We state `G` with
the NATURAL logarithm, so our maximum carries an additive `log 2`; dividing by `log 2`
recovers Kelly's bit-valued form exactly. The maximiser `ℓ = p - q = 2p - 1` is unaffected by
the choice of base.
-/

namespace KellyCriterion

/-- Kelly's exponential rate of growth `G(ℓ)` for an even-money bet with win probability `p`
and staked fraction `ℓ`, in nats (Kelly 1956, §4).

TOTALITY. Like every Lean definition this is total: `p` and `ℓ` range over all of `ℝ`, and
Mathlib's `Real.log` is itself total, with `Real.log 0 = 0` and `Real.log x = Real.log |x|`
for `x < 0`. So this expression evaluates to a real number for EVERY input, and outside
`ℓ ∈ (-1, 1)` those junk conventions are load-bearing rather than the intended mathematics —
e.g. at `ℓ = 1` it returns `p * Real.log 2`. Kelly's setting is `ℓ ∈ [0, 1)` with
`0 < p < 1`; the hypotheses live on the THEOREMS, which restrict to the range where both
logarithm arguments are strictly positive. Read no meaning into values outside it. -/
noncomputable def growthRate (p l : ℝ) : ℝ :=
  p * Real.log (1 + l) + (1 - p) * Real.log (1 - l)

/-- Kelly's optimal staked fraction `ℓ = p - q = 2p - 1` (Kelly 1956, §4). -/
noncomputable def optimalFraction (p : ℝ) : ℝ := 2 * p - 1

end KellyCriterion

• Endorsed by Shuze Chen · Sep 6, 2026

• Endorsed by viratkota · Sep 6, 2026

  Confirmed by the mission captain (proposal self-audit).