|
/- |
|
SPDX-License-Identifier: Apache-2.0 |
|
-/ |
|
import Mathlib.Analysis.SpecificLimits.Normed |
|
import Mathlib.Topology.Algebra.InfiniteSum.NatInt |
|
import Mathlib.Topology.Algebra.InfiniteSum.Order |
|
import Mathlib.Probability.ProductMeasure |
|
import Mathlib.Probability.Independence.InfinitePi |
|
import Mathlib.Analysis.SpecificLimits.Basic |
|
|
|
set_option linter.style.header false |
|
|
|
/-! |
|
# Gambler's Ruin for a Biased Walk |
|
|
|
This file is a self-contained Lean development of the biased ±1 walk catch-up |
|
probability used in Rosenfeld's analysis of hashrate-based double-spending. |
|
For an adversary with step probability `q`, honest step probability `p = 1 - q`, |
|
and `q < 1/2`, the probability of ever catching up from deficit `z` is |
|
`(q / p) ^ z`. |
|
-/ |
|
|
|
namespace GamblersRuin |
|
|
|
noncomputable def negBinTerm (q : ℝ) (d k : ℕ) : ℝ := |
|
((d + k - 1).choose k : ℝ) * (1 - q) ^ d * q ^ k |
|
|
|
theorem ruin_recurrence {q : ℝ} (hq1 : q < 1) (z : ℕ) : |
|
(q / (1 - q)) ^ (z + 1) |
|
= q * (q / (1 - q)) ^ z + (1 - q) * (q / (1 - q)) ^ (z + 2) := by |
|
have hne : (1 : ℝ) - q ≠ 0 := by linarith |
|
have key : q / (1 - q) = q + (1 - q) * (q / (1 - q)) ^ 2 := by |
|
field_simp |
|
ring |
|
calc (q / (1 - q)) ^ (z + 1) = (q / (1 - q)) ^ z * (q / (1 - q)) := by ring |
|
_ = (q / (1 - q)) ^ z * (q + (1 - q) * (q / (1 - q)) ^ 2) := by rw [← key] |
|
_ = q * (q / (1 - q)) ^ z + (1 - q) * (q / (1 - q)) ^ (z + 2) := by ring |
|
|
|
end GamblersRuin |
|
|
|
namespace GamblersRuin.Walk |
|
|
|
open MeasureTheory |
|
|
|
structure BiasedCoin where |
|
|
|
q : ℝ |
|
|
|
q_nonneg : 0 ≤ q |
|
|
|
q_lt_half : q < 1 / 2 |
|
|
|
namespace BiasedCoin |
|
|
|
variable (B : BiasedCoin) |
|
|
|
def p : ℝ := 1 - B.q |
|
|
|
theorem q_lt_one : B.q < 1 := by have := B.q_lt_half; linarith |
|
|
|
theorem p_pos : 0 < B.p := by have := B.q_lt_half; unfold p; linarith |
|
|
|
theorem p_nonneg : 0 ≤ B.p := B.p_pos.le |
|
|
|
theorem p_le_one : B.p ≤ 1 := by have := B.q_nonneg; unfold p; linarith |
|
|
|
theorem q_lt_p : B.q < B.p := by have := B.q_lt_half; unfold p; linarith |
|
|
|
theorem ratio_nonneg : 0 ≤ B.q / B.p := div_nonneg B.q_nonneg B.p_nonneg |
|
|
|
theorem ratio_lt_one : B.q / B.p < 1 := (div_lt_one B.p_pos).mpr B.q_lt_p |
|
|
|
noncomputable def coin : Measure Bool := |
|
ENNReal.ofReal B.p • Measure.dirac true + ENNReal.ofReal B.q • Measure.dirac false |
|
|
|
@[simp] theorem coin_true : B.coin {true} = ENNReal.ofReal B.p := by |
|
simp [coin, Measure.dirac_apply' _ (MeasurableSet.singleton true)] |
|
|
|
@[simp] theorem coin_false : B.coin {false} = ENNReal.ofReal B.q := by |
|
simp [coin, Measure.dirac_apply' _ (MeasurableSet.singleton false)] |
|
|
|
theorem coin_singleton (b : Bool) : |
|
B.coin {b} = ENNReal.ofReal (if b then B.p else B.q) := by |
|
cases b <;> simp |
|
|
|
instance : IsProbabilityMeasure B.coin where |
|
measure_univ := by |
|
have hq := B.q_nonneg |
|
have hp := B.p_nonneg |
|
simp only [coin, Measure.add_apply, Measure.smul_apply, measure_univ, |
|
smul_eq_mul, mul_one] |
|
rw [← ENNReal.ofReal_add hp hq] |
|
simp [p] |
|
|
|
noncomputable def mu : Measure (ℕ → Bool) := Measure.infinitePi fun _ => B.coin |
|
|
|
instance : IsProbabilityMeasure B.mu := by unfold mu; infer_instance |
|
|
|
end BiasedCoin |
|
|
|
def count (b : Bool) (ω : ℕ → Bool) (m : ℕ) : ℕ := |
|
((Finset.range m).filter fun i => ω i = b).card |
|
|
|
abbrev honestCount : (ℕ → Bool) → ℕ → ℕ := count true |
|
|
|
abbrev advCount : (ℕ → Bool) → ℕ → ℕ := count false |
|
|
|
def counts (ω : ℕ → Bool) : ℕ → ℕ × ℕ := fun n => (honestCount ω n, advCount ω n) |
|
|
|
@[simp] theorem counts_apply (ω : ℕ → Bool) (n : ℕ) : |
|
counts ω n = (honestCount ω n, advCount ω n) := rfl |
|
|
|
def shift (t : ℕ) (ω : ℕ → Bool) : ℕ → Bool := fun i => ω (t + i) |
|
|
|
@[simp] theorem shift_apply (t : ℕ) (ω : ℕ → Bool) (i : ℕ) : |
|
shift t ω i = ω (t + i) := rfl |
|
|
|
theorem shift_shift (s t : ℕ) (ω : ℕ → Bool) : |
|
shift t (shift s ω) = shift (s + t) ω := by |
|
funext i |
|
simp [shift, Nat.add_assoc] |
|
|
|
@[simp] theorem count_zero (b : Bool) (ω : ℕ → Bool) : count b ω 0 = 0 := by |
|
simp [count] |
|
|
|
theorem count_succ (b : Bool) (ω : ℕ → Bool) (m : ℕ) : |
|
count b ω (m + 1) = count b ω m + if ω m = b then 1 else 0 := by |
|
rw [count, Finset.range_add_one, Finset.filter_insert] |
|
split <;> simp [count, Finset.card_insert_of_notMem] |
|
|
|
theorem count_one (b : Bool) (ω : ℕ → Bool) : |
|
count b ω 1 = if ω 0 = b then 1 else 0 := by |
|
rw [show (1 : ℕ) = 0 + 1 from rfl, count_succ, count_zero, Nat.zero_add] |
|
|
|
theorem count_eq_sum (b : Bool) (ω : ℕ → Bool) (m : ℕ) : |
|
count b ω m = ∑ i ∈ Finset.range m, if ω i = b then 1 else 0 := by |
|
rw [count, Finset.card_filter] |
|
|
|
theorem count_mono (b : Bool) (ω : ℕ → Bool) : Monotone (count b ω) := by |
|
intro m n hmn |
|
exact Finset.card_le_card (Finset.filter_subset_filter _ (Finset.range_mono hmn)) |
|
|
|
theorem count_le_self (b : Bool) (ω : ℕ → Bool) (m : ℕ) : count b ω m ≤ m := by |
|
simpa [count] using Finset.card_filter_le (Finset.range m) fun i => ω i = b |
|
|
|
theorem count_succ_le (b : Bool) (ω : ℕ → Bool) (m : ℕ) : |
|
count b ω (m + 1) ≤ count b ω m + 1 := by |
|
rw [count_succ]; split <;> omega |
|
|
|
theorem count_true_add_count_false (ω : ℕ → Bool) (m : ℕ) : |
|
count true ω m + count false ω m = m := by |
|
induction m with |
|
| zero => simp |
|
| succ m ih => rw [count_succ, count_succ]; cases h : ω m <;> simp <;> omega |
|
|
|
theorem count_shift (b : Bool) (ω : ℕ → Bool) (t s : ℕ) : |
|
count b ω (t + s) = count b ω t + count b (shift t ω) s := by |
|
induction s with |
|
| zero => simp |
|
| succ s ih => rw [← Nat.add_assoc, count_succ, count_succ, ih, shift_apply, |
|
Nat.add_assoc] |
|
|
|
theorem exists_count_eq {b : Bool} {ω : ℕ → Bool} {M d : ℕ} |
|
(h : d ≤ count b ω M) : ∃ m ≤ M, count b ω m = d := by |
|
induction M with |
|
| zero => exact ⟨0, le_rfl, by simp at h ⊢; omega⟩ |
|
| succ M ih => |
|
rcases le_or_gt d (count b ω M) with h' | h' |
|
· obtain ⟨m, hm, hmeq⟩ := ih h' |
|
exact ⟨m, hm.trans (Nat.le_succ M), hmeq⟩ |
|
· have := count_succ_le b ω M |
|
exact ⟨M + 1, le_rfl, by omega⟩ |
|
|
|
def catchupEvent (s d : ℕ) : Set (ℕ → Bool) := |
|
{ω | ∃ n, d ≤ honestCount ω n ∧ honestCount ω n ≤ advCount ω n + s} |
|
|
|
@[simp] theorem mem_catchupEvent {s d : ℕ} {ω : ℕ → Bool} : |
|
ω ∈ catchupEvent s d ↔ |
|
∃ n, d ≤ honestCount ω n ∧ honestCount ω n ≤ advCount ω n + s := |
|
Iff.rfl |
|
|
|
def lagEvent (z : ℕ) : Set (ℕ → Bool) := |
|
{ω | ∃ n, honestCount ω n + z ≤ advCount ω n} |
|
|
|
@[simp] theorem mem_lagEvent {z : ℕ} {ω : ℕ → Bool} : |
|
ω ∈ lagEvent z ↔ ∃ n, honestCount ω n + z ≤ advCount ω n := |
|
Iff.rfl |
|
|
|
def lagEventWithin (N z : ℕ) : Set (ℕ → Bool) := |
|
{ω | ∃ n ≤ N, honestCount ω n + z ≤ advCount ω n} |
|
|
|
@[simp] theorem mem_lagEventWithin {N z : ℕ} {ω : ℕ → Bool} : |
|
ω ∈ lagEventWithin N z ↔ ∃ n ≤ N, honestCount ω n + z ≤ advCount ω n := |
|
Iff.rfl |
|
|
|
theorem lagEventWithin_mono (z : ℕ) : Monotone (lagEventWithin · z) := by |
|
intro N N' hNN' ω ⟨n, hn, h⟩ |
|
exact ⟨n, hn.trans hNN', h⟩ |
|
|
|
theorem lagEvent_eq_iUnion (z : ℕ) : lagEvent z = ⋃ N, lagEventWithin N z := by |
|
ext ω |
|
simp only [mem_lagEvent, Set.mem_iUnion, mem_lagEventWithin] |
|
exact ⟨fun ⟨n, h⟩ => ⟨n, n, le_rfl, h⟩, fun ⟨N, n, _, h⟩ => ⟨n, h⟩⟩ |
|
|
|
def levelEvent (d : ℕ) : Set (ℕ → Bool) := {ω | ∃ m, honestCount ω m = d} |
|
|
|
@[simp] theorem mem_levelEvent {d : ℕ} {ω : ℕ → Bool} : |
|
ω ∈ levelEvent d ↔ ∃ m, honestCount ω m = d := |
|
Iff.rfl |
|
|
|
noncomputable def hitWithin (q : ℝ) : ℕ → ℕ → ℝ |
|
| 0, 0 => 1 |
|
| 0, _ + 1 => 0 |
|
| _ + 1, 0 => 1 |
|
| N + 1, z + 1 => q * hitWithin q N z + (1 - q) * hitWithin q N (z + 2) |
|
|
|
@[simp] theorem hitWithin_zero_right (q : ℝ) (N : ℕ) : hitWithin q N 0 = 1 := by |
|
cases N <;> rfl |
|
|
|
@[simp] theorem hitWithin_zero_succ (q : ℝ) (z : ℕ) : |
|
hitWithin q 0 (z + 1) = 0 := rfl |
|
|
|
theorem hitWithin_succ_succ (q : ℝ) (N z : ℕ) : |
|
hitWithin q (N + 1) (z + 1) |
|
= q * hitWithin q N z + (1 - q) * hitWithin q N (z + 2) := rfl |
|
|
|
noncomputable def catchupProb (q : ℝ) (z : ℕ) : ℝ := ⨆ N, hitWithin q N z |
|
|
|
noncomputable abbrev negbinWeight (q : ℝ) (d k : ℕ) : ℝ := negBinTerm q d k |
|
|
|
theorem measurable_count_cylinderEvents (b : Bool) (m : ℕ) : |
|
Measurable[MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) {i : ℕ | i < m}] |
|
(fun ω : ℕ → Bool => count b ω m) := by |
|
have : (fun ω : ℕ → Bool => count b ω m) |
|
= fun ω => ∑ i ∈ Finset.range m, if ω i = b then 1 else 0 := by |
|
funext ω; exact count_eq_sum b ω m |
|
rw [this] |
|
refine Finset.measurable_sum _ fun i hi => ?_ |
|
have h1 : Measurable[MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) |
|
{i : ℕ | i < m}] (fun ω : ℕ → Bool => ω i) := |
|
measurable_cylinderEvent_apply (Finset.mem_range.mp hi) |
|
exact (Measurable.of_discrete (f := fun x : Bool => if x = b then 1 else 0)).comp h1 |
|
|
|
theorem measurable_count (b : Bool) (m : ℕ) : |
|
Measurable (fun ω : ℕ → Bool => count b ω m) := |
|
(measurable_count_cylinderEvents b m).mono cylinderEvents_le_pi le_rfl |
|
|
|
theorem measurable_shift (t : ℕ) : Measurable (shift t) := |
|
measurable_pi_iff.mpr fun i => measurable_pi_apply (t + i) |
|
|
|
theorem measurable_shift_cylinderEvents (t : ℕ) : |
|
Measurable[MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) {i : ℕ | t ≤ i}] |
|
(shift t) := by |
|
rw [@measurable_pi_iff] |
|
exact fun i => measurable_cylinderEvent_apply (Nat.le_add_right t i) |
|
|
|
theorem measurable_counts : Measurable counts := |
|
measurable_pi_iff.mpr fun n => |
|
(measurable_count true n).prodMk (measurable_count false n) |
|
|
|
theorem measurableSet_catchupEvent (s d : ℕ) : |
|
MeasurableSet (catchupEvent s d) := by |
|
have : catchupEvent s d = ⋃ n, (fun ω => (honestCount ω n, advCount ω n)) ⁻¹' |
|
{p : ℕ × ℕ | d ≤ p.1 ∧ p.1 ≤ p.2 + s} := by |
|
ext ω; simp [catchupEvent] |
|
rw [this] |
|
exact MeasurableSet.iUnion fun n => |
|
((measurable_count true n).prodMk (measurable_count false n)) .of_discrete |
|
|
|
theorem measurableSet_lagEvent (z : ℕ) : MeasurableSet (lagEvent z) := by |
|
have : lagEvent z = ⋃ n, (fun ω => (honestCount ω n, advCount ω n)) ⁻¹' |
|
{p : ℕ × ℕ | p.1 + z ≤ p.2} := by |
|
ext ω; simp [lagEvent] |
|
rw [this] |
|
exact MeasurableSet.iUnion fun n => |
|
((measurable_count true n).prodMk (measurable_count false n)) .of_discrete |
|
|
|
theorem measurableSet_lagEventWithin (N z : ℕ) : |
|
MeasurableSet (lagEventWithin N z) := by |
|
have : lagEventWithin N z |
|
= ⋃ n, ⋃ _ : n ≤ N, (fun ω => (honestCount ω n, advCount ω n)) ⁻¹' |
|
{p : ℕ × ℕ | p.1 + z ≤ p.2} := by |
|
ext ω; simp [lagEventWithin] |
|
rw [this] |
|
exact MeasurableSet.iUnion fun n => MeasurableSet.iUnion fun _ => |
|
((measurable_count true n).prodMk (measurable_count false n)) .of_discrete |
|
|
|
theorem measurableSet_levelEvent (d : ℕ) : MeasurableSet (levelEvent d) := by |
|
have : levelEvent d = ⋃ m, (fun ω => honestCount ω m) ⁻¹' {d} := by |
|
ext ω; simp [levelEvent] |
|
rw [this] |
|
exact MeasurableSet.iUnion fun m => |
|
(measurable_count true m) (measurableSet_singleton d) |
|
|
|
end GamblersRuin.Walk |
|
|
|
namespace GamblersRuin.Walk |
|
|
|
open MeasureTheory |
|
|
|
def coordEvent (n : ℕ) (b : Bool) : Set (ℕ → Bool) := {ω | ω n = b} |
|
|
|
@[simp] theorem mem_coordEvent {n : ℕ} {b : Bool} {ω : ℕ → Bool} : |
|
ω ∈ coordEvent n b ↔ ω n = b := |
|
Iff.rfl |
|
|
|
theorem coordEvent_eq_pi (n : ℕ) (b : Bool) : |
|
coordEvent n b = Set.pi (({n} : Finset ℕ) : Set ℕ) fun _ => ({b} : Set Bool) := by |
|
ext ω |
|
simp [coordEvent] |
|
|
|
theorem coordEvent_eq_preimage (n : ℕ) (b : Bool) : |
|
coordEvent n b = (fun ω : ℕ → Bool => ω n) ⁻¹' {b} := rfl |
|
|
|
theorem measurableSet_coordEvent (n : ℕ) (b : Bool) : |
|
MeasurableSet (coordEvent n b) := by |
|
rw [coordEvent_eq_preimage] |
|
exact (measurable_pi_apply n) (measurableSet_singleton b) |
|
|
|
theorem measurableSet_coordEvent_cylinderEvents {Δ : Set ℕ} {n : ℕ} (hn : n ∈ Δ) |
|
(b : Bool) : |
|
MeasurableSet[MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) Δ] |
|
(coordEvent n b) := by |
|
rw [coordEvent_eq_preimage] |
|
exact (measurable_cylinderEvent_apply hn) (measurableSet_singleton b) |
|
|
|
variable (B : BiasedCoin) |
|
|
|
theorem mu_coordEvent (n : ℕ) (b : Bool) : B.mu (coordEvent n b) = B.coin {b} := by |
|
rw [coordEvent_eq_pi, BiasedCoin.mu, |
|
Measure.infinitePi_pi (μ := fun _ : ℕ => B.coin) |
|
fun _ _ => measurableSet_singleton b] |
|
simp |
|
|
|
@[simp] theorem mu_coordEvent_true (n : ℕ) : |
|
B.mu (coordEvent n true) = ENNReal.ofReal B.p := by |
|
rw [mu_coordEvent]; simp |
|
|
|
@[simp] theorem mu_coordEvent_false (n : ℕ) : |
|
B.mu (coordEvent n false) = ENNReal.ofReal B.q := by |
|
rw [mu_coordEvent]; simp |
|
|
|
end GamblersRuin.Walk |
|
|
|
namespace GamblersRuin.Walk |
|
|
|
open MeasureTheory ProbabilityTheory |
|
|
|
variable (B : BiasedCoin) |
|
|
|
theorem map_shift (t : ℕ) : B.mu.map (shift t) = B.mu := |
|
Measure.map_infinitePi_infinitePi_of_inj |
|
(P := fun _ : ℕ => B.coin) (f := fun i : ℕ => t + i) |
|
fun a b hab => by simpa using hab |
|
|
|
theorem mu_shift_preimage (t : ℕ) {A : Set (ℕ → Bool)} (hA : MeasurableSet A) : |
|
B.mu (shift t ⁻¹' A) = B.mu A := by |
|
conv_rhs => rw [← map_shift B t] |
|
rw [Measure.map_apply (measurable_shift t) hA] |
|
|
|
theorem indep_prefix_tail (t : ℕ) : |
|
Indep (MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) {i : ℕ | i < t}) |
|
(MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) {i : ℕ | t ≤ i}) |
|
B.mu := by |
|
have hind : iIndepFun (fun (i : ℕ) (ω : ℕ → Bool) => ω i) B.mu := |
|
iIndepFun_infinitePi (X := fun _ => id) fun _ => measurable_id |
|
have h := indep_iSup_of_disjoint |
|
(m := fun i : ℕ => |
|
MeasurableSpace.comap (fun ω : ℕ → Bool => ω i) inferInstance) |
|
(fun i => measurable_iff_comap_le.mp (measurable_pi_apply i)) hind |
|
(Set.disjoint_left.mpr fun i (hi : i < t) (hi' : t ≤ i) => by omega) |
|
exact h |
|
|
|
theorem mu_inter_shift_preimage (t : ℕ) {E A : Set (ℕ → Bool)} |
|
(hE : MeasurableSet[MeasureTheory.cylinderEvents (X := fun _ : ℕ => Bool) |
|
{i : ℕ | i < t}] E) |
|
(hA : MeasurableSet A) : |
|
B.mu (E ∩ shift t ⁻¹' A) = B.mu E * B.mu A := by |
|
have hshift : MeasurableSet[MeasureTheory.cylinderEvents |
|
(X := fun _ : ℕ => Bool) {i : ℕ | t ≤ i}] (shift t ⁻¹' A) := |
|
measurable_shift_cylinderEvents t hA |
|
rw [(Indep_iff _ _ _).mp (indep_prefix_tail B t) E (shift t ⁻¹' A) hE hshift, |
|
mu_shift_preimage B t hA] |
|
|
|
theorem mu_coordEvent_inter_shift_one (b : Bool) {A : Set (ℕ → Bool)} |
|
(hA : MeasurableSet A) : |
|
B.mu (coordEvent 0 b ∩ shift 1 ⁻¹' A) = B.coin {b} * B.mu A := by |
|
rw [mu_inter_shift_preimage B 1 |
|
(measurableSet_coordEvent_cylinderEvents (by simp) b) hA, |
|
mu_coordEvent] |
|
|
|
end GamblersRuin.Walk |
|
|
|
namespace GamblersRuin.Walk |
|
|
|
open MeasureTheory Filter |
|
|
|
section HitWithin |
|
|
|
variable {q : ℝ} |
|
|
|
theorem hitWithin_nonneg (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : |
|
∀ N z, 0 ≤ hitWithin q N z := by |
|
intro N |
|
induction N with |
|
| zero => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => simp |
|
| succ N ih => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => |
|
rw [hitWithin_succ_succ] |
|
exact add_nonneg (mul_nonneg hq0 (ih z)) |
|
(mul_nonneg (by linarith) (ih (z + 2))) |
|
|
|
theorem hitWithin_le_one (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : |
|
∀ N z, hitWithin q N z ≤ 1 := by |
|
intro N |
|
induction N with |
|
| zero => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => simp |
|
| succ N ih => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => |
|
rw [hitWithin_succ_succ] |
|
have h1 := mul_le_mul_of_nonneg_left (ih z) hq0 |
|
have h2 := mul_le_mul_of_nonneg_left (ih (z + 2)) |
|
(by linarith : (0 : ℝ) ≤ 1 - q) |
|
linarith |
|
|
|
theorem hitWithin_succ_le (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : |
|
∀ N z, hitWithin q N z ≤ hitWithin q (N + 1) z := by |
|
intro N |
|
induction N with |
|
| zero => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => simpa using hitWithin_nonneg hq0 hq1 1 (z + 1) |
|
| succ N ih => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => |
|
rw [hitWithin_succ_succ, hitWithin_succ_succ] |
|
exact add_le_add (mul_le_mul_of_nonneg_left (ih z) hq0) |
|
(mul_le_mul_of_nonneg_left (ih (z + 2)) (by linarith)) |
|
|
|
theorem hitWithin_mono_horizon (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (z : ℕ) : |
|
Monotone fun N => hitWithin q N z := |
|
monotone_nat_of_le_succ fun N => hitWithin_succ_le hq0 hq1 N z |
|
|
|
theorem hitWithin_le_pow (hq0 : 0 ≤ q) (hq1 : q < 1) : |
|
∀ N z, hitWithin q N z ≤ (q / (1 - q)) ^ z := by |
|
have hr0 : 0 ≤ q / (1 - q) := div_nonneg hq0 (by linarith) |
|
intro N |
|
induction N with |
|
| zero => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => simpa using pow_nonneg hr0 (z + 1) |
|
| succ N ih => |
|
intro z |
|
cases z with |
|
| zero => simp |
|
| succ z => |
|
rw [hitWithin_succ_succ, ruin_recurrence hq1 z] |
|
exact add_le_add (mul_le_mul_of_nonneg_left (ih z) hq0) |
|
(mul_le_mul_of_nonneg_left (ih (z + 2)) (by linarith)) |
|
|
|
theorem bddAbove_hitWithin (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (z : ℕ) : |
|
BddAbove (Set.range fun N => hitWithin q N z) := by |
|
refine ⟨1, ?_⟩ |
|
rintro y ⟨N, rfl⟩ |
|
exact hitWithin_le_one hq0 hq1 N z |
|
|
|
theorem tendsto_hitWithin (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (z : ℕ) : |
|
Tendsto (fun N => hitWithin q N z) atTop (nhds (catchupProb q z)) := |
|
tendsto_atTop_ciSup (hitWithin_mono_horizon hq0 hq1 z) |
|
(bddAbove_hitWithin hq0 hq1 z) |
|
|
|
@[simp] theorem catchupProb_zero (q : ℝ) : catchupProb q 0 = 1 := by |
|
simp [catchupProb] |
|
|
|
theorem catchupProb_nonneg (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (z : ℕ) : |
|
0 ≤ catchupProb q z := |
|
(hitWithin_nonneg hq0 hq1 0 z).trans |
|
(le_ciSup (bddAbove_hitWithin hq0 hq1 z) 0) |
|
|
|
theorem catchupProb_le_pow (hq0 : 0 ≤ q) (hq1 : q < 1) (z : ℕ) : |
|
catchupProb q z ≤ (q / (1 - q)) ^ z := |
|
ciSup_le fun N => hitWithin_le_pow hq0 hq1 N z |
|
|
|
theorem catchupProb_succ (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (z : ℕ) : |
|
catchupProb q (z + 1) |
|
= q * catchupProb q z + (1 - q) * catchupProb q (z + 2) := by |
|
have h4 : Tendsto (fun N => hitWithin q (N + 1) (z + 1)) atTop |
|
(nhds (catchupProb q (z + 1))) := |
|
(tendsto_hitWithin hq0 hq1 (z + 1)).comp (tendsto_add_atTop_nat 1) |
|
have h5 : Tendsto |
|
(fun N => q * hitWithin q N z + (1 - q) * hitWithin q N (z + 2)) atTop |
|
(nhds (q * catchupProb q z + (1 - q) * catchupProb q (z + 2))) := |
|
((tendsto_hitWithin hq0 hq1 z).const_mul q).add |
|
((tendsto_hitWithin hq0 hq1 (z + 2)).const_mul (1 - q)) |
|
have heq : (fun N => hitWithin q (N + 1) (z + 1)) |
|
= fun N => q * hitWithin q N z + (1 - q) * hitWithin q N (z + 2) := |
|
funext fun N => hitWithin_succ_succ q N z |
|
exact tendsto_nhds_unique (heq ▸ h4) h5 |
|
|
|
private theorem ruinDefect_increment (hq0 : 0 ≤ q) (hq : q < 1 / 2) (z : ℕ) : |
|
((q / (1 - q)) ^ (z + 1) - catchupProb q (z + 1)) |
|
- ((q / (1 - q)) ^ z - catchupProb q z) |
|
= (q / (1 - q)) ^ z * ((q / (1 - q)) - catchupProb q 1) := by |
|
induction z with |
|
| zero => simp |
|
| succ z ih => |
|
have hp : (0 : ℝ) < 1 - q := by linarith |
|
have hpne : (1 : ℝ) - q ≠ 0 := ne_of_gt hp |
|
have hq1 : q < 1 := by linarith |
|
|
|
have hu := catchupProb_succ hq0 hq1.le z |
|
have hr := ruin_recurrence hq1 z |
|
have hstep : (1 - q) * (q / (1 - q)) = q := by field_simp |
|
refine mul_left_cancel₀ hpne ?_ |
|
calc (1 - q) * (((q / (1 - q)) ^ (z + 2) - catchupProb q (z + 2)) |
|
- ((q / (1 - q)) ^ (z + 1) - catchupProb q (z + 1))) |
|
= q * (((q / (1 - q)) ^ (z + 1) - catchupProb q (z + 1)) |
|
- ((q / (1 - q)) ^ z - catchupProb q z)) := by |
|
linear_combination hu - hr |
|
_ = q * ((q / (1 - q)) ^ z * ((q / (1 - q)) - catchupProb q 1)) := by |
|
rw [ih] |
|
_ = (1 - q) * ((q / (1 - q)) ^ (z + 1) |
|
* ((q / (1 - q)) - catchupProb q 1)) := by |
|
rw [pow_succ] |
|
linear_combination |
|
(-((q / (1 - q)) ^ z * ((q / (1 - q)) - catchupProb q 1))) * hstep |
|
|
|
theorem catchupProb_eq (hq0 : 0 ≤ q) (hq : q < 1 / 2) (z : ℕ) : |
|
catchupProb q z = (q / (1 - q)) ^ z := by |
|
have hq1 : q < 1 := by linarith |
|
have hp : (0 : ℝ) < 1 - q := by linarith |
|
have hr0 : 0 ≤ q / (1 - q) := div_nonneg hq0 hp.le |
|
have hr1 : q / (1 - q) < 1 := (div_lt_one hp).mpr (by linarith) |
|
set w : ℕ → ℝ := fun z => (q / (1 - q)) ^ z - catchupProb q z with hw |
|
have hw_nonneg : ∀ z, 0 ≤ w z := fun z => |
|
sub_nonneg.mpr (catchupProb_le_pow hq0 hq1 z) |
|
have hw_le : ∀ z, w z ≤ (q / (1 - q)) ^ z := fun z => by |
|
have := catchupProb_nonneg hq0 hq1.le z |
|
simp only [hw] |
|
linarith |
|
have hincr : ∀ z, w (z + 1) - w z = (q / (1 - q)) ^ z * w 1 := by |
|
intro z |
|
have h := ruinDefect_increment hq0 hq z |
|
simp only [hw] at h ⊢ |
|
rw [h] |
|
congr 1 |
|
simp |
|
have hmono : Monotone w := |
|
monotone_nat_of_le_succ fun z => by |
|
have h := hincr z |
|
have := mul_nonneg (pow_nonneg hr0 z) (hw_nonneg 1) |
|
linarith |
|
|
|
have hw1 : w 1 = 0 := by |
|
have htend : Tendsto (fun z : ℕ => (q / (1 - q)) ^ z) atTop (nhds 0) := |
|
tendsto_pow_atTop_nhds_zero_of_lt_one hr0 hr1 |
|
have hle : ∀ᶠ z : ℕ in atTop, w 1 ≤ (q / (1 - q)) ^ z := by |
|
filter_upwards [eventually_ge_atTop 1] with z hz |
|
exact (hmono hz).trans (hw_le z) |
|
exact le_antisymm (ge_of_tendsto htend hle) (hw_nonneg 1) |
|
|
|
have hzero : ∀ z, w z = 0 := by |
|
intro z |
|
induction z with |
|
| zero => simp [hw, catchupProb_zero] |
|
| succ z ih => |
|
have h := hincr z |
|
rw [hw1, ih] at h |
|
simpa using h |
|
have := hzero z |
|
simp only [hw] at this |
|
linarith |
|
|
|
end HitWithin |
|
|
|
theorem lagEventWithin_lag_zero (N : ℕ) : lagEventWithin N 0 = Set.univ := by |
|
ext ω |
|
simp only [mem_lagEventWithin, Set.mem_univ, iff_true] |
|
exact ⟨0, Nat.zero_le N, by simp⟩ |
|
|
|
theorem lagEventWithin_horizon_zero (z : ℕ) : lagEventWithin 0 (z + 1) = ∅ := by |
|
ext ω |
|
simp only [mem_lagEventWithin, Set.mem_empty_iff_false, iff_false] |
|
rintro ⟨n, hn, h⟩ |
|
obtain rfl : n = 0 := Nat.le_zero.mp hn |
|
simp at h |
|
|
|
theorem count_succ_shift (b : Bool) (ω : ℕ → Bool) (s : ℕ) : |
|
count b ω (s + 1) = (if ω 0 = b then 1 else 0) + count b (shift 1 ω) s := by |
|
rw [Nat.add_comm s 1, count_shift, count_one] |
|
|
|
theorem lagEventWithin_succ_succ (N z : ℕ) : |
|
lagEventWithin (N + 1) (z + 1) |
|
= (coordEvent 0 false ∩ shift 1 ⁻¹' lagEventWithin N z) |
|
∪ (coordEvent 0 true ∩ shift 1 ⁻¹' lagEventWithin N (z + 2)) := by |
|
ext ω |
|
simp only [mem_lagEventWithin, Set.mem_union, Set.mem_inter_iff, |
|
mem_coordEvent, Set.mem_preimage] |
|
constructor |
|
· rintro ⟨n, hn, h⟩ |
|
match n with |
|
| 0 => |
|
replace h : count true ω 0 + (z + 1) ≤ count false ω 0 := h |
|
simp at h |
|
| s + 1 => |
|
replace h : count true ω (s + 1) + (z + 1) ≤ count false ω (s + 1) := h |
|
have hct := count_succ_shift true ω s |
|
have hcf := count_succ_shift false ω s |
|
cases hb : ω 0 with |
|
| false => |
|
rw [hb] at hct hcf |
|
simp at hct hcf |
|
refine Or.inl ⟨rfl, s, by omega, ?_⟩ |
|
change count true (shift 1 ω) s + z ≤ count false (shift 1 ω) s |
|
omega |
|
| true => |
|
rw [hb] at hct hcf |
|
simp at hct hcf |
|
refine Or.inr ⟨rfl, s, by omega, ?_⟩ |
|
change count true (shift 1 ω) s + (z + 2) ≤ count false (shift 1 ω) s |
|
omega |
|
· rintro (⟨hb, s, hs, h⟩ | ⟨hb, s, hs, h⟩) |
|
· replace h : count true (shift 1 ω) s + z ≤ count false (shift 1 ω) s := h |
|
have hct := count_succ_shift true ω s |
|
have hcf := count_succ_shift false ω s |
|
rw [hb] at hct hcf |
|
simp at hct hcf |
|
refine ⟨s + 1, by omega, ?_⟩ |
|
change count true ω (s + 1) + (z + 1) ≤ count false ω (s + 1) |
|
omega |
|
· replace h : count true (shift 1 ω) s + (z + 2) ≤ count false (shift 1 ω) s := h |
|
have hct := count_succ_shift true ω s |
|
have hcf := count_succ_shift false ω s |
|
rw [hb] at hct hcf |
|
simp at hct hcf |
|
refine ⟨s + 1, by omega, ?_⟩ |
|
change count true ω (s + 1) + (z + 1) ≤ count false ω (s + 1) |
|
omega |
|
|
|
variable (B : BiasedCoin) |
|
|
|
theorem mu_lagEventWithin : |
|
∀ N z, B.mu (lagEventWithin N z) = ENNReal.ofReal (hitWithin B.q N z) := by |
|
have hq0 := B.q_nonneg |
|
have hq1 := B.q_lt_one.le |
|
intro N |
|
induction N with |
|
| zero => |
|
intro z |
|
cases z with |
|
| zero => rw [lagEventWithin_lag_zero]; simp |
|
| succ z => rw [lagEventWithin_horizon_zero]; simp |
|
| succ N ih => |
|
intro z |
|
cases z with |
|
| zero => rw [lagEventWithin_lag_zero]; simp |
|
| succ z => |
|
rw [lagEventWithin_succ_succ] |
|
have hdisj : Disjoint |
|
(coordEvent 0 false ∩ shift 1 ⁻¹' lagEventWithin N z) |
|
(coordEvent 0 true ∩ shift 1 ⁻¹' lagEventWithin N (z + 2)) := by |
|
refine Set.disjoint_left.mpr ?_ |
|
rintro ω ⟨h1, -⟩ ⟨h2, -⟩ |
|
rw [mem_coordEvent] at h1 h2 |
|
simp [h1] at h2 |
|
rw [measure_union hdisj |
|
((measurableSet_coordEvent 0 true).inter |
|
((measurable_shift 1) (measurableSet_lagEventWithin N (z + 2)))), |
|
mu_coordEvent_inter_shift_one B false (measurableSet_lagEventWithin N z), |
|
mu_coordEvent_inter_shift_one B true |
|
(measurableSet_lagEventWithin N (z + 2)), |
|
ih z, ih (z + 2), BiasedCoin.coin_false, BiasedCoin.coin_true] |
|
have hh1 := hitWithin_nonneg hq0 hq1 N z |
|
have hh2 := hitWithin_nonneg hq0 hq1 N (z + 2) |
|
rw [← ENNReal.ofReal_mul hq0, ← ENNReal.ofReal_mul B.p_nonneg, |
|
← ENNReal.ofReal_add (mul_nonneg hq0 hh1) (mul_nonneg B.p_nonneg hh2), |
|
hitWithin_succ_succ] |
|
rfl |
|
|
|
theorem mu_lagEvent (z : ℕ) : |
|
B.mu (lagEvent z) = ENNReal.ofReal ((B.q / B.p) ^ z) := by |
|
rw [lagEvent_eq_iUnion] |
|
have htend := tendsto_measure_iUnion_atTop (μ := B.mu) (lagEventWithin_mono z) |
|
have h2 : Tendsto (fun N => B.mu (lagEventWithin N z)) atTop |
|
(nhds (ENNReal.ofReal (catchupProb B.q z))) := by |
|
simp only [mu_lagEventWithin] |
|
exact (ENNReal.continuous_ofReal.tendsto _).comp |
|
(tendsto_hitWithin B.q_nonneg B.q_lt_one.le z) |
|
rw [tendsto_nhds_unique htend h2, |
|
catchupProb_eq B.q_nonneg B.q_lt_half z] |
|
rfl |
|
|
|
end GamblersRuin.Walk |
