Kelly's information-rate identity (in nats)
ProvedKellyCriterion.growthRate_optimalFraction_eqinformation-theoryprobability
The growth rate attained at Kelly's fraction equals log 2 + p log p + (1-p) log(1-p). Dividing by log 2 gives Kelly's bit-valued maximum 1 + p log2 p + q log2 q, which is one minus the binary entropy of p -- the identity between capital growth rate and information rate.
Preamble
import Definitions.Def_KellyCriterion open KellyCriterion
Formal statement
namespace KellyCriterion
theorem growthRate_optimalFraction_eq {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
growthRate p (optimalFraction p)
= Real.log 2 + p * Real.log p + (1 - p) * Real.log (1 - p) := by
sorry
end KellyCriterionSource
Kelly 1956, Section 4: G_max = 1 + p log p + q log q, in bits.
Human review
Confirmed by the mission captain (proposal self-audit).