The optimal fraction is an admissible stake
ProvedKellyCriterion.optimalFraction_mem_Iooprobability
For a favourable bet, Kelly's fraction 2p-1 lies strictly between 0 and 1: the gambler stakes a positive proportion of wealth but never all of it. This is what makes the logarithms in the growth rate finite and the strategy survivable.
Preamble
import Definitions.Def_KellyCriterion open KellyCriterion
Formal statement
namespace KellyCriterion
theorem optimalFraction_mem_Ioo {p : ℝ} (hp : 1/2 < p) (hp1 : p < 1) :
optimalFraction p ∈ Set.Ioo (0:ℝ) 1 := by
sorry
end KellyCriterionSource
Kelly 1956, Section 4 (implicit admissibility of l = p - q for p > 1/2).
Human review
Confirmed by the mission captain (proposal self-audit).