linearUtilityPartial

formal source

 131
 132/-- The partial sum of the linear-utility expected payout from
 133`n = 1` to `n = N` (inclusive). -/
 134def linearUtilityPartial (N : ℕ) : ℝ :=
 135  ∑ n ∈ Finset.Ico 1 (N + 1), prob n * payout n
 136
 137/-- **CLOSED FORM (linear utility).** The partial sum is exactly `N`. -/
 138theorem linearUtilityPartial_eq (N : ℕ) :
 139    linearUtilityPartial N = N := by
 140  unfold linearUtilityPartial
 141  -- Each term equals 1, so the sum equals the cardinality of the index set.
 142  rw [Finset.sum_congr rfl (fun n _ => linear_term n)]
 143  rw [Finset.sum_const]
 144  rw [Nat.card_Ico]
 145  simp
 146
 147/-- **DIVERGENCE OF LINEAR UTILITY.** The linear expected payout is
 148unbounded: for every `M`, there is an `N` such that the partial sum
 149exceeds `M`. -/
 150theorem linearUtility_diverges :
 151    ∀ M : ℝ, ∃ N : ℕ, M < linearUtilityPartial N := by
 152  intro M
 153  obtain ⟨N, hN⟩ := exists_nat_gt M
 154  exact ⟨N, by rw [linearUtilityPartial_eq]; exact hN⟩
 155
 156/-- The linear partial sum is non-decreasing. -/
 157theorem linearUtilityPartial_mono : Monotone linearUtilityPartial := by
 158  intro N₁ N₂ h
 159  rw [linearUtilityPartial_eq, linearUtilityPartial_eq]
 160  exact_mod_cast h
 161
 162/-! ## §3. Log utility: the closed-form identity `S_N = 2 - (N+2)/2^N`
 163
 164The fundamental identity: