Random Walk

Stream: new members

[Joshua Banks]

Hi, I am trying to define a simple random walk for example where the start is 0, and each increment is either +1 or -1, and looking to prove some simple properties of this, such as the sum expected sum of the walk is 0. I am struggling to work out how to define a sequence of random variables which can only take values of either 1 or -1. Does anyone know if this is possible in lean and give any pointers on how I could approach this. Thanks for any advice.

[Rémy Degenne]

Here is an example of how you could do this (in lean 3, since measure/probability theory has not been ported to lean 4 yet):

import probability.notation

open measure_theory

-- get probability notation, the notation `ℝ≥0∞` and the notation `∑`
open_locale probability_theory ennreal big_operators

-- define a measurable space with a measure, denoted by `ℙ`
variables {Ω : Type*} [measure_space Ω]

-- the real measure supported on -1 and 1, with probability 1/2 for each
noncomputable
def two_points_measure : measure ℝ :=
(2 : ℝ≥0∞)⁻¹ • measure.dirac (-1) + (2 : ℝ≥0∞)⁻¹ • measure.dirac 1

-- a sequence of random variables, each with law `two_points_measure`
variables {X : ℕ → Ω → ℝ} (h : ∀ n, measure.map (X n) ℙ = two_points_measure)

-- An example statement about the mean to check that we have imported everything.
example (n : ℕ) : ∀ᵐ ω, (∑ i in finset.range n, X n ω) / n ≤ 1 :=
sorry

-- 𝔼 is a notation for the integral against ℙ
-- TODO: prove it :)
example (n : ℕ) : 𝔼[∑ i in finset.range n, X n] = 0 :=
sorry

[Rémy Degenne]

In that example, I am not very happy about the way we have to write the measure.map = ... hypothesis. We should have a better API for probability, but we barely have any probability right now, so it's still not very polished.

[Rémy Degenne]

Also since I just made a definition for the measure you wanted, lean knows nothing about it. For example some lemmas might need a [is_probability_measure two_points_measure] instance: you will have to prove it. It is possible that we have a better way of defining finitely supported probability distributions, for example using docs#pmf.to_measure, but I don't know what we have about that.

[Kevin Buzzard]

If we barely have any probability right now, this classic random walk might be a great project to expose what we need to do.

[Rémy Degenne]

Another remark: my example said nothing about independence of the X i for different i. You might want to look at docs#probability_theory.strong_law_ae (the law of large numbers) for an example involving iid pairwise independent, identically distributed random variables.

[Yaël Dillies]

You might also like to see how we deal with the Erdos-Rényi model in LeanCamCombi. You should in particular be interested in weighted_cube.

[Ryan McCorvie]

@Joshua Banks Hi I'm also looking for first projects in lean, would you like to collaborate on simple random walks? I imagine, e.g., doing the arcsine laws along the lines of the combinatorial approach in Feller vol I.