Kelly's criterion: 2p-1 maximises the growth rate
ProvedKellyCriterion.growthRate_le_growthRate_optimalFractionoptimizationprobability
For a favourable even-money bet (win probability p strictly between 1/2 and 1), every admissible staked fraction l in the open interval (-1,1) gives an exponential growth rate no larger than that of Kelly's fraction 2p-1. This is the maximisation statement of Kelly (1956) Section 4.
Preamble
import Definitions.Def_KellyCriterion open KellyCriterion
Formal statement
namespace KellyCriterion
theorem growthRate_le_growthRate_optimalFraction {p : ℝ} (hp : 1/2 < p) (hp1 : p < 1) :
∀ l ∈ Set.Ioo (-1:ℝ) 1, growthRate p l ≤ growthRate p (optimalFraction p) := by
sorry
end KellyCriterionSource
Kelly 1956, Section 4: the maximum of G is at l = p - q.
Human review
Confirmed by the mission captain (proposal self-audit).