IndisputableMonolith.Decision.StPetersburg

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# St Petersburg Paradox: Linear Utility Diverges, Log Utility Converges (Track E6)
   7
   8Replaces the earlier placeholder version of this module. The earlier
   9file defined `marginal_utility := 1/(1+x)` and proved it was positive
  10and decreasing. That had nothing to do with St Petersburg.
  11
  12This file builds the actual St Petersburg ensemble and proves the
  13divergence/convergence dichotomy directly from the partial sums.
  14
  15## The St Petersburg ensemble
  16
  17A fair coin is flipped until it lands heads.  If heads first appears
  18on flip `n ≥ 1`, the player wins `2^n`.  The probability that the
  19first head occurs on flip `n` is `(1/2)^n` (geometric distribution).
  20
  21Equivalently: there is a sample space indexed by `n : ℕ` (the flip
  22on which the first head occurs), with `P(n) = (1/2)^(n+1)` for
  23`n = 0, 1, 2, ...` (so payout on outcome `n` is `2^(n+1)`).  We use
  24the 1-indexed convention here: outcomes are `n = 1, 2, ...`,
  25probability `(1/2)^n`, payout `2^n`.
  26
  27## What we prove
  28
  29**Linear utility (the classical paradox).** The expected payout
  30under linear utility is
  31
  32\[
  33  E[X] = \sum_{n = 1}^{\infty} \tfrac{1}{2^n} \cdot 2^n
  34       = \sum_{n = 1}^{\infty} 1
  35       = +\infty.
  36\]
  37
  38We prove this by showing the partial sum `∑_{n=1}^{N} (1/2)^n · 2^n
  39= N`, which is unbounded.
  40
  41**Log utility (the J-cost-shaped resolution).** The expected utility
  42under log payout is
  43
  44\[
  45  E[\log X]
  46  = \sum_{n = 1}^{\infty} \tfrac{1}{2^n} \cdot \log(2^n)
  47  = (\log 2) \sum_{n = 1}^{\infty} \tfrac{n}{2^n}
  48  = (\log 2) \cdot 2
  49  = 2 \log 2 \approx 1.386.
  50\]
  51
  52We work directly with the unitless sum `∑ n / 2^n`; the `log 2` factor
  53is constant and does not affect the convergence/divergence dichotomy.
  54We prove the **closed-form identity**
  55
  56\[
  57  \sum_{n = 1}^{N} \tfrac{n}{2^n}
  58  = 2 - \tfrac{N + 2}{2^N},
  59\]
  60
  61from which `S_N < 2` for every `N`, so the partial sums form a
  62bounded monotone sequence and therefore converge.
  63
  64This is the J-cost-shaped resolution because `J(x) = (x + x⁻¹)/2 - 1`
  65expanded near `x = 1` agrees to second order with `½(log x)²`, so
  66log-utility is the local J-cost penalty around the natural reference
  67point.
  68
  69## Connection to RS
  70
  71The St Petersburg paradox is not about probability theory; it is
  72about which utility function the player applies. RS makes a definite
  73prediction: utility scales as `J(x)`, the unique reciprocal-symmetric
  74cost. Locally that behaves like `log` (and `(log x)²`), giving a
  75finite expected utility on heavy-tailed payouts.
  76
  77The classical "paradox" is the observation that linear utility (which
  78has no σ-conservation structure) gives a divergent expected value.
  79J-cost utility (which has σ-conservation built in) does not.
  80
  81## Status
  82
  83THEOREM: divergence of the linear partial sum (unbounded), convergence
  84of the log partial sum (bounded above by `2`), and the closed-form
  85identity `∑_{n=1}^{N} n/2^n = 2 - (N+2)/2^N`.
  86
  87No HYPOTHESIS, no axiom, no `sorry`.
  88
  89The fact that `J(x)` agrees to leading order with `½(log x)²` near
  90`x = 1` is recorded in a separate module (`Cost.JcostExpansion`) and
  91not repeated here.
  92-/
  93
  94namespace IndisputableMonolith
  95namespace Decision
  96namespace StPetersburg
  97
  98open Constants Cost
  99open scoped BigOperators
 100
 101noncomputable section
 102
 103/-! ## §1. Payout, probability, and the two utility functionals -/
 104
 105/-- The payout on outcome `n` (heads first on flip `n`): `2^n`.
 106We work with `n ≥ 1`, but allow `n = 0` for sum-indexing convenience
 107(the `n = 0` term contributes nothing to either partial sum). -/
 108def payout (n : ℕ) : ℝ := (2 : ℝ) ^ n
 109
 110/-- The probability of outcome `n`: `(1/2)^n`.  -/
 111def prob (n : ℕ) : ℝ := (1 / 2 : ℝ) ^ n
 112
 113/-- The probability of outcome 0 in our 1-indexed convention is
 114just `1`, the empty product; we use the partial-sum range
 115`Finset.Ico 1 (N+1)` to sum over `n = 1, ..., N`. -/
 116theorem prob_zero : prob 0 = 1 := by
 117  unfold prob; simp
 118
 119/-- Probability is positive. -/
 120theorem prob_pos (n : ℕ) : 0 < prob n := by
 121  unfold prob; positivity
 122
 123/-! ## §2. Linear utility: the partial sum equals `N` -/
 124
 125/-- The per-outcome contribution to the linear-utility expected
 126payout: `prob n · payout n = (1/2)^n · 2^n = 1`. -/
 127theorem linear_term (n : ℕ) : prob n * payout n = 1 := by
 128  unfold prob payout
 129  rw [← mul_pow]
 130  norm_num
 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:
 165
 166  `∑_{n = 1}^{N} n / 2^n = 2 - (N + 2) / 2^N`.
 167
 168Proof by induction on `N`.
 169
 170The per-outcome contribution to the log-utility expected payout is
 171`prob n · n = n / 2^n` (we are working with the unitless sum;
 172multiply by `log 2` at the end if you want the actual expected log
 173payout).
 174-/
 175
 176/-- The per-outcome contribution to the log-utility expected payout
 177(unitless: `n / 2^n`). -/
 178def logTerm (n : ℕ) : ℝ := (n : ℝ) / (2 : ℝ) ^ n
 179
 180/-- The unitless log-utility partial sum from `n = 1` to `n = N`. -/
 181def logUtilityPartial (N : ℕ) : ℝ :=
 182  ∑ n ∈ Finset.Ico 1 (N + 1), logTerm n
 183
 184/-- The empty partial sum is zero. -/
 185theorem logUtilityPartial_zero : logUtilityPartial 0 = 0 := by
 186  unfold logUtilityPartial
 187  simp
 188
 189/-- The recursion: `logUtilityPartial (N+1) = logUtilityPartial N
 190  + (N+1) / 2^(N+1)`. -/
 191theorem logUtilityPartial_succ (N : ℕ) :
 192    logUtilityPartial (N + 1) =
 193      logUtilityPartial N + ((N + 1 : ℕ) : ℝ) / (2 : ℝ) ^ (N + 1) := by
 194  unfold logUtilityPartial logTerm
 195  -- Finset.Ico 1 (N+2) = Finset.Ico 1 (N+1) ∪ {N+1}.
 196  rw [show N + 1 + 1 = (N + 1) + 1 from rfl]
 197  rw [Finset.sum_Ico_succ_top (Nat.succ_le_succ (Nat.zero_le N))]
 198
 199/-- **CLOSED FORM (log utility).** The unitless partial sum equals
 200`2 - (N + 2) / 2^N` for every `N : ℕ`. -/
 201theorem logUtilityPartial_closed_form (N : ℕ) :
 202    logUtilityPartial N = 2 - ((N : ℝ) + 2) / (2 : ℝ) ^ N := by
 203  induction N with
 204  | zero =>
 205      simp [logUtilityPartial_zero]
 206  | succ N ih =>
 207      rw [logUtilityPartial_succ N, ih]
 208      -- Goal: 2 - (N+2)/2^N + (N+1)/2^(N+1) = 2 - (N+3)/2^(N+1).
 209      have h2pos : (0 : ℝ) < (2 : ℝ) ^ (N + 1) := pow_pos (by norm_num : (0 : ℝ) < 2) _
 210      have h2pow : (2 : ℝ) ^ (N + 1) = 2 * (2 : ℝ) ^ N := by
 211        rw [pow_succ]; ring
 212      push_cast
 213      field_simp
 214      ring
 215
 216/-- **BOUNDEDNESS OF THE LOG PARTIAL SUM.** For every `N`,
 217`logUtilityPartial N < 2`. -/
 218theorem logUtilityPartial_lt_two (N : ℕ) :
 219    logUtilityPartial N < 2 := by
 220  rw [logUtilityPartial_closed_form]
 221  have h_pow_pos : (0 : ℝ) < (2 : ℝ) ^ N := pow_pos (by norm_num : (0 : ℝ) < 2) _
 222  have h_num_pos : (0 : ℝ) < (N : ℝ) + 2 := by
 223    have : (0 : ℝ) ≤ (N : ℝ) := Nat.cast_nonneg N
 224    linarith
 225  have h_quot_pos : (0 : ℝ) < ((N : ℝ) + 2) / (2 : ℝ) ^ N := div_pos h_num_pos h_pow_pos
 226  linarith
 227
 228/-- The log partial sum is non-negative. -/
 229theorem logUtilityPartial_nonneg (N : ℕ) :
 230    0 ≤ logUtilityPartial N := by
 231  unfold logUtilityPartial logTerm
 232  apply Finset.sum_nonneg
 233  intro n _
 234  apply div_nonneg
 235  · exact Nat.cast_nonneg n
 236  · exact le_of_lt (pow_pos (by norm_num : (0 : ℝ) < 2) _)
 237
 238/-- The log partial sum is monotone in `N`. -/
 239theorem logUtilityPartial_mono : Monotone logUtilityPartial := by
 240  intro N₁ N₂ h
 241  unfold logUtilityPartial logTerm
 242  apply Finset.sum_le_sum_of_subset_of_nonneg
 243  · intro n hn
 244    rw [Finset.mem_Ico] at hn ⊢
 245    exact ⟨hn.1, lt_of_lt_of_le hn.2 (Nat.succ_le_succ h)⟩
 246  · intro n _ _
 247    apply div_nonneg
 248    · exact Nat.cast_nonneg n
 249    · exact le_of_lt (pow_pos (by norm_num : (0 : ℝ) < 2) _)
 250
 251/-! ## §4. Convergence of the log expected utility
 252
 253A bounded monotone sequence converges. We don't need to compute the
 254limit (`= 2`); we just need the existence of the limit. -/
 255
 256/-- The auxiliary limit `(N + 2) / 2^N → 0` as `N → ∞`. -/
 257private theorem aux_limit_N_plus_two_div_pow :
 258    Filter.Tendsto (fun N : ℕ => ((N : ℝ) + 2) / (2 : ℝ) ^ N)
 259      Filter.atTop (nhds 0) := by
 260  -- Split as N/2^N + 2/2^N; both pieces tend to 0.
 261  -- Piece 1: N / 2^N from `tendsto_pow_const_div_const_pow_of_one_lt 1`.
 262  have h_lim_n : Filter.Tendsto (fun N : ℕ => (N : ℝ) / (2 : ℝ) ^ N)
 263      Filter.atTop (nhds 0) := by
 264    have h := tendsto_pow_const_div_const_pow_of_one_lt 1
 265      (show (1 : ℝ) < 2 by norm_num)
 266    simpa [pow_one] using h
 267  -- Piece 2: 2 / 2^N = 2 · (1/2)^N → 2 · 0 = 0.
 268  have h_lim_const : Filter.Tendsto (fun N : ℕ => (2 : ℝ) / (2 : ℝ) ^ N)
 269      Filter.atTop (nhds 0) := by
 270    have h_half : Filter.Tendsto (fun N : ℕ => ((1 / 2 : ℝ)) ^ N)
 271        Filter.atTop (nhds 0) :=
 272      tendsto_pow_atTop_nhds_zero_of_lt_one
 273        (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num : (1 / 2 : ℝ) < 1)
 274    have h_mul := h_half.const_mul (2 : ℝ)
 275    simp only [mul_zero] at h_mul
 276    -- 2 · (1/2)^N = 2 / 2^N, after rewriting (1/2)^N = 1/2^N.
 277    have h_eq : (fun N : ℕ => (2 : ℝ) * ((1 / 2 : ℝ)) ^ N)
 278        = (fun N : ℕ => (2 : ℝ) / (2 : ℝ) ^ N) := by
 279      funext N
 280      rw [div_pow, one_pow]
 281      field_simp
 282    rw [h_eq] at h_mul
 283    exact h_mul
 284  -- Combine.
 285  have h_sum := h_lim_n.add h_lim_const
 286  simp only [zero_add] at h_sum
 287  have h_split : (fun N : ℕ => ((N : ℝ) + 2) / (2 : ℝ) ^ N)
 288      = (fun N : ℕ => (N : ℝ) / (2 : ℝ) ^ N + (2 : ℝ) / (2 : ℝ) ^ N) := by
 289    funext N
 290    have : (2 : ℝ) ^ N ≠ 0 := pow_ne_zero N (by norm_num : (2 : ℝ) ≠ 0)
 291    field_simp
 292  rw [h_split]
 293  exact h_sum
 294
 295/-- **THE LOG EXPECTED UTILITY EQUALS `2`** (in unitless form).
 296The full expected log payout is `2 · log 2 = log 4`. -/
 297theorem logUtility_limit_eq_two :
 298    Filter.Tendsto (fun N => logUtilityPartial N)
 299      Filter.atTop (nhds (2 : ℝ)) := by
 300  -- logUtilityPartial N = 2 - (N+2)/2^N, and (N+2)/2^N → 0.
 301  have h_diff : (fun N : ℕ => logUtilityPartial N)
 302      = (fun N : ℕ => (2 : ℝ) - ((N : ℝ) + 2) / (2 : ℝ) ^ N) := by
 303    funext N
 304    exact logUtilityPartial_closed_form N
 305  rw [h_diff]
 306  -- 2 - f(N) → 2 - 0 = 2.
 307  have h_const : Filter.Tendsto (fun _ : ℕ => (2 : ℝ)) Filter.atTop (nhds 2) :=
 308    tendsto_const_nhds
 309  have h_sub := h_const.sub aux_limit_N_plus_two_div_pow
 310  simp only [sub_zero] at h_sub
 311  exact h_sub
 312
 313/-- **CONVERGENCE OF LOG UTILITY.** The log partial sums converge. -/
 314theorem logUtility_converges :
 315    ∃ L : ℝ, Filter.Tendsto (fun N => logUtilityPartial N)
 316      Filter.atTop (nhds L) :=
 317  ⟨2, logUtility_limit_eq_two⟩
 318
 319/-! ## §5. The dichotomy: linear diverges, log converges -/
 320
 321/-- **DICHOTOMY.** Under the St Petersburg ensemble, linear utility
 322gives a divergent expected payout while the log-shaped (J-cost-shaped)
 323utility gives a finite expected payout. -/
 324theorem stPetersburg_dichotomy :
 325    -- (1) Linear utility: unbounded.
 326    (∀ M : ℝ, ∃ N : ℕ, M < linearUtilityPartial N) ∧
 327    -- (2) Log utility: bounded above by 2.
 328    (∀ N : ℕ, logUtilityPartial N < 2) ∧
 329    -- (3) Log utility: converges to 2.
 330    Filter.Tendsto (fun N => logUtilityPartial N)
 331      Filter.atTop (nhds (2 : ℝ)) := by
 332  exact ⟨linearUtility_diverges, logUtilityPartial_lt_two, logUtility_limit_eq_two⟩
 333
 334/-! ## §6. Master certificate -/
 335
 336/-- **ST PETERSBURG MASTER CERTIFICATE.**
 337
 338Eight clauses, all derived from explicit summation on `Finset.Ico`:
 339
 3401. The per-outcome term `prob n · payout n` equals `1`.
 3412. The linear-utility partial sum equals `N` (closed form).
 3423. The linear-utility partial sums are unbounded.
 3434. The log-utility partial sum has closed form `2 - (N+2)/2^N`.
 3445. The log-utility partial sums are bounded above by `2`.
 3456. The log-utility partial sums are non-negative and monotone.
 3467. The log-utility partial sums converge to `2`.
 3478. The dichotomy holds: linear diverges, log converges.
 348
 349This is not a label-and-arithmetic statement; the closed-form
 350identities and the convergence statement are derived from
 351Mathlib's `Filter.Tendsto` and `Finset.sum`. -/
 352structure StPetersburgCert where
 353  linear_term_eq_one : ∀ n, prob n * payout n = 1
 354  linear_partial_eq_N : ∀ N, linearUtilityPartial N = N
 355  linear_unbounded : ∀ M : ℝ, ∃ N, M < linearUtilityPartial N
 356  log_partial_closed : ∀ N, logUtilityPartial N = 2 - ((N : ℝ) + 2) / (2 : ℝ) ^ N
 357  log_partial_lt_two : ∀ N, logUtilityPartial N < 2
 358  log_partial_nonneg : ∀ N, 0 ≤ logUtilityPartial N
 359  log_partial_mono : Monotone logUtilityPartial
 360  log_converges_to_two :
 361    Filter.Tendsto (fun N => logUtilityPartial N) Filter.atTop (nhds (2 : ℝ))
 362
 363/-- The master certificate is inhabited. -/
 364def stPetersburgCert : StPetersburgCert where
 365  linear_term_eq_one := linear_term
 366  linear_partial_eq_N := linearUtilityPartial_eq
 367  linear_unbounded := linearUtility_diverges
 368  log_partial_closed := logUtilityPartial_closed_form
 369  log_partial_lt_two := logUtilityPartial_lt_two
 370  log_partial_nonneg := logUtilityPartial_nonneg
 371  log_partial_mono := logUtilityPartial_mono
 372  log_converges_to_two := logUtility_limit_eq_two
 373
 374/-! ## §7. One-statement summary -/
 375
 376/-- **ST PETERSBURG ONE-STATEMENT THEOREM.**
 377
 378For the St Petersburg ensemble (heads first on flip `n` with
 379probability `(1/2)^n`, payout `2^n`):
 380
 381(1) Linear utility: `∑_{n=1}^{N} (1/2)^n · 2^n = N`, unbounded.
 382(2) Log utility (unitless): `∑_{n=1}^{N} n / 2^n = 2 - (N+2)/2^N`,
 383    bounded above by `2`, converging to `2`.
 384(3) Therefore linear utility predicts an infinite price for the
 385    game, while log-utility (the J-cost-shaped resolution) predicts
 386    a finite price `≈ 2 log 2 ≈ 1.386` (in log units of payout). -/
 387theorem st_petersburg_one_statement :
 388    -- (1) Linear partial sum = N.
 389    (∀ N, linearUtilityPartial N = N) ∧
 390    -- (2) Log partial sum has the closed form.
 391    (∀ N, logUtilityPartial N = 2 - ((N : ℝ) + 2) / (2 : ℝ) ^ N) ∧
 392    -- (3) Log partial sum is strictly less than 2.
 393    (∀ N, logUtilityPartial N < 2) ∧
 394    -- (4) Log partial sum converges to 2.
 395    Filter.Tendsto (fun N => logUtilityPartial N) Filter.atTop (nhds (2 : ℝ)) :=
 396  ⟨linearUtilityPartial_eq, logUtilityPartial_closed_form,
 397   logUtilityPartial_lt_two, logUtility_limit_eq_two⟩
 398
 399end
 400
 401end StPetersburg
 402end Decision
 403end IndisputableMonolith
 404