discrete_itotheoremProved here from basic factspropext, Classical.choice, Quot.sound
discrete_itoLean 4Proved here from basic factsFormally verified
/-- **The discrete Itô formula.** For any real sequence `S₀, S₁, …` the left-point sums satisfy`∑_{k<n} Sₖ (Sₖ₊₁ − Sₖ) = (Sₙ² − S₀²)/2 − ½ ∑_{k<n} (Sₖ₊₁ − Sₖ)²`.The last sum is the quadratic variation. For a smooth path it tends to `0` under refinement and werecover `∫ S dS = (Sₙ² − S₀²)/2`; for Brownian motion it tends to `t`, which gives`∫₀ᵗ B dB = (B_t² − t)/2`. Proof: induction on `n`; each step is the identity`a (b − a) = (b² − a²)/2 − (b − a)²/2`. -/theorem discrete_ito (S : ℕ → ℝ) (n : ℕ) : ∑ k ∈ Finset.range n, S k * (S (k + 1) - S k) = (S n ^ 2 - S 0 ^ 2) / 2 - (∑ k ∈ Finset.range n, (S (k + 1) - S k) ^ 2) / 2 := by induction n with | zero => simp | succ n ih => rw [Finset.sum_range_succ, Finset.sum_range_succ, ih] ring
discrete_stratonovichtheoremProved here from basic factspropext, Classical.choice, Quot.sound
discrete_stratonovichLean 4Proved here from basic factsFormally verified
/-- **The discrete Stratonovich formula.** With midpoint values `(Sₖ + Sₖ₊₁)/2` instead ofleft-point values, the sum telescopes exactly and the ordinary chain rule holds:`∑_{k<n} (Sₖ + Sₖ₊₁)/2 · (Sₖ₊₁ − Sₖ) = (Sₙ² − S₀²)/2`. The two sums differ by half the quadraticvariation, so for Brownian paths the choice of evaluation point matters. -/theorem discrete_stratonovich (S : ℕ → ℝ) (n : ℕ) : ∑ k ∈ Finset.range n, (S k + S (k + 1)) / 2 * (S (k + 1) - S k) = (S n ^ 2 - S 0 ^ 2) / 2 := by induction n with | zero => simp | succ n ih => rw [Finset.sum_range_succ, ih] ring
random_walk_itotheoremProved here from basic factspropext, Classical.choice, Quot.sound
random_walk_itoLean 4Proved here from basic factsFormally verified
/-- **Itô's formula for the simple random walk.** If `S₀ = 0` and every step is `±1`, thequadratic variation after `n` steps is exactly `n`, so`∑_{k<n} Sₖ (Sₖ₊₁ − Sₖ) = (Sₙ² − n)/2`. Rescaling space by `√n` and time by `n` turns this into`∫₀¹ B dB = (B₁² − 1)/2`. Proof: the discrete Itô formula with `(±1)² = 1`. -/theorem random_walk_ito (S : ℕ → ℝ) (h0 : S 0 = 0) (hstep : ∀ k, S (k + 1) - S k = 1 ∨ S (k + 1) - S k = -1) (n : ℕ) : ∑ k ∈ Finset.range n, S k * (S (k + 1) - S k) = (S n ^ 2 - n) / 2 := by have hqv : ∑ k ∈ Finset.range n, (S (k + 1) - S k) ^ 2 = n := by rw [Finset.sum_congr rfl fun k _ => show (S (k + 1) - S k) ^ 2 = 1 by rcases hstep k with h | h <;> rw [h] <;> norm_num] simp rw [discrete_ito, h0, hqv] ring
/-- The Poisson probabilities `pₖ(r) = e^{-r} rᵏ / k!`: the probability of exactly `k` arrivalsin a time interval of length `t` for a Poisson process of rate `λ`, with `r = λt`. -/noncomputable def poissonPMF (r : ℝ) (k : ℕ) : ℝ := Real.exp (-r) * r ^ k / k.factorial
poissonPMF_eqtheoremApplies a library theorempropext, Classical.choice, Quot.sound
poissonPMF_eqLean 4Applies a library theoremFormally verified
/-- Our `poissonPMF` agrees with the point masses of Mathlib's Poisson distribution `Po(r)`(`ProbabilityTheory.poissonMeasure_real_singleton`). -/theorem poissonPMF_eq (r : ℝ≥0) (k : ℕ) : (poissonMeasure r).real {k} = poissonPMF r k := poissonMeasure_real_singleton r k
poisson_convolutiontheoremProved here from basic factspropext, Classical.choice, Quot.sound
poisson_convolutionLean 4Proved here from basic factsFormally verified
/-- **Poisson counts add.** `∑_{j ≤ k} pⱼ(s) p_{k−j}(t) = pₖ(s + t)`: if `N_s` and `N_{s+t} − N_s`are independent Poisson variables with means `s` and `t`, their sum is Poisson with mean`s + t`. This is the consistency (Chapman–Kolmogorov) condition that makes the Poisson processwell defined. Proof: expand `(s + t)ᵏ` by the binomial theorem (`add_pow`) and write`C(k, j) = k! / (j! (k − j)!)` (`Nat.cast_choose`). -/theorem poisson_convolution (s t : ℝ) (k : ℕ) : ∑ j ∈ Finset.range (k + 1), poissonPMF s j * poissonPMF t (k - j) = poissonPMF (s + t) k := by simp only [poissonPMF] rw [add_pow, Finset.mul_sum, Finset.sum_div] refine Finset.sum_congr rfl fun j hj => ?_ have hjk : j ≤ k := Nat.lt_succ_iff.mp (Finset.mem_range.mp hj) rw [Nat.cast_choose ℝ hjk, neg_add, Real.exp_add] have h1 : (j.factorial : ℝ) ≠ 0 := by positivity have h2 : ((k - j).factorial : ℝ) ≠ 0 := by positivity have h3 : (k.factorial : ℝ) ≠ 0 := by positivity field_simp
law_of_rare_eventstheoremApplies a library theorempropext, Classical.choice, Quot.sound
law_of_rare_eventsLean 4Applies a library theoremFormally verified
/-- **The law of rare events** (Poisson limit theorem). If `n pₙ → r`, the binomialprobabilities `C(n, k) pₙᵏ (1 − pₙ)^{n−k}` tend to `e^{-r} rᵏ / k!`. Chop `[0, t]` into `n` slotswith an arrival in each with probability `λt/n`: in the limit the count is Poisson. This isMathlib's `tendsto_choose_mul_pow_of_tendsto_mul_atTop`. -/theorem law_of_rare_events {p : ℕ → ℝ} {r : ℝ} (k : ℕ) (hr : Tendsto (fun n => n * p n) atTop (𝓝 r)) : Tendsto (fun n => n.choose k * p n ^ k * (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r) * r ^ k / k.factorial)) := tendsto_choose_mul_pow_of_tendsto_mul_atTop k hr
exp_memorylesstheoremProved here from basic factspropext, Classical.choice, Quot.sound
exp_memorylessLean 4Proved here from basic factsFormally verified
/-- **Exponential waiting times are memoryless.** If `T` has the exponential distribution withrate `r > 0`, then `P(T > s + t) = P(T > s) · P(T > t)` for `s, t ≥ 0`, i.e.`P(T > s + t | T > s) = P(T > t)`: having waited `s` units tells you nothing. This is why theholding times of a Poisson process (and of any continuous-time Markov chain) are exponential.Proof: Mathlib's formula `F(x) = 1 − e^{−rx}` for the distribution function (`cdf_expMeasure_eq`)and `e^{a+b} = eᵃ eᵇ`. -/theorem exp_memoryless {r : ℝ} (hr : 0 < r) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : 1 - cdf (expMeasure r) (s + t) = (1 - cdf (expMeasure r) s) * (1 - cdf (expMeasure r) t) := by rw [cdf_expMeasure_eq hr, cdf_expMeasure_eq hr, cdf_expMeasure_eq hr] simp only [add_nonneg hs ht, hs, ht, ite_true, sub_sub_cancel] rw [← Real.exp_add] ring_nf
two_state_forwardtheoremProved here from basic factspropext, Classical.choice, Quot.sound
two_state_forwardLean 4Proved here from basic factsFormally verified
/-- **The two-state chain solves Kolmogorov's forward equation.** A chain on `{0, 1}` jumps`0 → 1` at rate `a` and `1 → 0` at rate `b` (with `a + b > 0`). Its transition probability`p(t) = P(X_t = 0 | X_0 = 0) = b/(a+b) + a/(a+b) · e^{−(a+b)t}` satisfies `p(0) = 1` and`p′(t) = −a p(t) + b (1 − p(t))`: probability flows out of `0` at rate `a` and back in at rate`b`. As `t → ∞`, `p(t) → b/(a+b)`, the stationary probability of state `0`. -/theorem two_state_forward {a b : ℝ} (hab : 0 < a + b) (t : ℝ) : (b / (a + b) + a / (a + b) * Real.exp (-(a + b) * 0) = 1) ∧ HasDerivAt (fun s => b / (a + b) + a / (a + b) * Real.exp (-(a + b) * s)) (-a * (b / (a + b) + a / (a + b) * Real.exp (-(a + b) * t)) + b * (1 - (b / (a + b) + a / (a + b) * Real.exp (-(a + b) * t)))) t := by have hne : a + b ≠ 0 := hab.ne' constructor · field_simp simp ring · have hexp : HasDerivAt (fun s => Real.exp (-(a + b) * s)) (Real.exp (-(a + b) * t) * (-(a + b))) t := by have := ((hasDerivAt_id t).const_mul (-(a + b))).exp simpa using this convert (hexp.const_mul (a / (a + b))).const_add (b / (a + b)) using 1 field_simp ring
brownian_incrementtheoremApplies a library theorempropext, Classical.choice, Quot.sound
brownian_incrementLean 4Applies a library theoremFormally verified
/-- **Brownian increments are Gaussian:** `B_s − B_t` has law `N(0, |s − t|)`. This is Mathlib's`IsPreBrownianReal.hasLaw_sub`. -/theorem brownian_increment {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (s t : ℝ≥0) : HasLaw (B s - B t) (gaussianReal 0 (nndist s.1 t.1)) P := hB.hasLaw_sub s t
brownian_scalingtheoremApplies a library theorempropext, Classical.choice, Quot.sound
brownian_scalingLean 4Applies a library theoremFormally verified
/-- **Brownian scaling.** If `B` is a Brownian motion and `c > 0`, then `t ↦ c^{−1/2} B_{ct}` isagain a Brownian motion: zooming in on a Brownian path by `c` in time and `√c` in space gives aBrownian path. This is Mathlib's `IsBrownianReal.smul`. -/theorem brownian_scaling {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) {c : ℝ≥0} (hc : c ≠ 0) : IsBrownianReal (fun t ω => (√c)⁻¹ * B (c * t) ω) P := hB.smul hc
brownian_time_inversiontheoremApplies a library theorempropext, Classical.choice, Quot.sound
brownian_time_inversionLean 4Applies a library theoremFormally verified
/-- **Time inversion.** If `B` is a pre-Brownian motion, so is `t ↦ t B_{1/t}`. It convertsstatements about `t → ∞` into statements about `t → 0`. This is Mathlib's`IsPreBrownianReal.inv`. -/theorem brownian_time_inversion {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) : IsPreBrownianReal (fun t ω => t * B (1 / t) ω) P := hB.inv
/-- The candidate solution of `dS = μ S dt + σ S dB`, written as a function of time `t` and ofthe value `x = B_t` of the driving Brownian motion: `f(t, x) = S₀ exp((μ − σ²/2) t + σ x)`. -/noncomputable def gbm (S₀ μ σ t x : ℝ) : ℝ := S₀ * Real.exp ((μ - σ ^ 2 / 2) * t + σ * x)
gbm_itotheoremProved here from basic factspropext, Classical.choice, Quot.sound
gbm_itoLean 4Proved here from basic factsFormally verified
/-- **The calculus behind geometric Brownian motion.** For `f = gbm S₀ μ σ`:`∂ₓf = σ f`, `∂ₓₓf = σ² f`, `∂ₜf = (μ − σ²/2) f`, and hence `∂ₜf + ½ ∂ₓₓf = μ f`.Itô's formula `df(t, B_t) = (∂ₜf + ½ ∂ₓₓf) dt + ∂ₓf dB_t` then gives`dS_t = μ S_t dt + σ S_t dB_t` for `S_t = f(t, B_t)`: the `−σ²/2` in the exponent is exactlycancelled by Itô's correction term `½ ∂ₓₓf`. (Itô's formula itself is not in Mathlib; thistheorem verifies the derivatives it needs.) -/theorem gbm_ito (S₀ μ σ t x : ℝ) : HasDerivAt (fun y => gbm S₀ μ σ t y) (σ * gbm S₀ μ σ t x) x ∧ HasDerivAt (fun y => σ * gbm S₀ μ σ t y) (σ ^ 2 * gbm S₀ μ σ t x) x ∧ HasDerivAt (fun s => gbm S₀ μ σ s x) ((μ - σ ^ 2 / 2) * gbm S₀ μ σ t x) t ∧ (μ - σ ^ 2 / 2) * gbm S₀ μ σ t x + σ ^ 2 * gbm S₀ μ σ t x / 2 = μ * gbm S₀ μ σ t x := by -- derivative in the space variable have hx : HasDerivAt (fun y => gbm S₀ μ σ t y) (σ * gbm S₀ μ σ t x) x := by have h := (((hasDerivAt_id x).const_mul σ).const_add ((μ - σ ^ 2 / 2) * t)).exp.const_mul S₀ convert h using 1 · simp only [gbm, id] · simp only [gbm, id] ring refine ⟨hx, ?_, ?_, by ring⟩ · convert hx.const_mul σ using 1 ring · have h := ((((hasDerivAt_id t).const_mul (μ - σ ^ 2 / 2)).add_const (σ * x)).exp).const_mul S₀ convert h using 1 · simp only [gbm, id] · simp only [gbm, id] ring
/-- **Midpoint sums telescope.** Hint: induction on `n`; in the successor case rewrite with`Finset.sum_range_succ` and the induction hypothesis, then `ring`. -/theorem discrete_stratonovich (S : ℕ → ℝ) (n : ℕ) : ∑ k ∈ Finset.range n, (S k + S (k + 1)) / 2 * (S (k + 1) - S k) = (S n ^ 2 - S 0 ^ 2) / 2 := by sorry
Show the compiled solution
discrete_stratonovichLean 4Proved here from basic factsFormally verified
/-- **The discrete Stratonovich formula.** With midpoint values `(Sₖ + Sₖ₊₁)/2` instead ofleft-point values, the sum telescopes exactly and the ordinary chain rule holds:`∑_{k<n} (Sₖ + Sₖ₊₁)/2 · (Sₖ₊₁ − Sₖ) = (Sₙ² − S₀²)/2`. The two sums differ by half the quadraticvariation, so for Brownian paths the choice of evaluation point matters. -/theorem discrete_stratonovich (S : ℕ → ℝ) (n : ℕ) : ∑ k ∈ Finset.range n, (S k + S (k + 1)) / 2 * (S (k + 1) - S k) = (S n ^ 2 - S 0 ^ 2) / 2 := by induction n with | zero => simp | succ n ih => rw [Finset.sum_range_succ, ih] ring
/-- **Itô's formula for the simple random walk.** Hint: first show that the quadratic variation`∑ k ∈ Finset.range n, (S (k + 1) - S k) ^ 2` equals `n` (each term is `1`), then rewrite with`Lumenary.StochasticProcesses.discrete_ito`. -/theorem random_walk_ito (S : ℕ → ℝ) (h0 : S 0 = 0) (hstep : ∀ k, S (k + 1) - S k = 1 ∨ S (k + 1) - S k = -1) (n : ℕ) : ∑ k ∈ Finset.range n, S k * (S (k + 1) - S k) = (S n ^ 2 - n) / 2 := by sorry
Show the compiled solution
random_walk_itoLean 4Proved here from basic factsFormally verified
/-- **Itô's formula for the simple random walk.** If `S₀ = 0` and every step is `±1`, thequadratic variation after `n` steps is exactly `n`, so`∑_{k<n} Sₖ (Sₖ₊₁ − Sₖ) = (Sₙ² − n)/2`. Rescaling space by `√n` and time by `n` turns this into`∫₀¹ B dB = (B₁² − 1)/2`. Proof: the discrete Itô formula with `(±1)² = 1`. -/theorem random_walk_ito (S : ℕ → ℝ) (h0 : S 0 = 0) (hstep : ∀ k, S (k + 1) - S k = 1 ∨ S (k + 1) - S k = -1) (n : ℕ) : ∑ k ∈ Finset.range n, S k * (S (k + 1) - S k) = (S n ^ 2 - n) / 2 := by have hqv : ∑ k ∈ Finset.range n, (S (k + 1) - S k) ^ 2 = n := by rw [Finset.sum_congr rfl fun k _ => show (S (k + 1) - S k) ^ 2 = 1 by rcases hstep k with h | h <;> rw [h] <;> norm_num] simp rw [discrete_ito, h0, hqv] ring