Definition of two relational random sequence

Stream: mathlib4

[haotian liu]

I want to define two random sequences, S and X, where the value of Sk is randomly drawn with equal probability from {1, 2, ..., N}, and Xk+1 = Xk - a * Sk, where 0 < a < 1.
How should I define the two random sequences S and X in Lean?
Or are there any documents in Lean that I can refer to?

[Yaël Dillies]

The idea is to define k ↦ S k as being drawn from the uniform distribution on {1, ..., N}, then define X by recursion using it.

[Yaël Dillies]

Is S an infinite sequence, or is it finite?

[haotian liu]

S is a finite sequence.

[haotian liu]

I still have a question. Suppose there is a random variable X, which follows the distribution μ. Are there any relevant theorems about random sampling in Mathlib?

variable {Ω : Type*} [MeasurableSpace Ω]
variable {X : Ω → ℝ} {μ : Measure Ω}

[haotian liu]

Yaël Dillies said:

The idea is to define k ↦ S k as being drawn from the uniform distribution on {1, ..., N}, then define X by recursion using it.

I still have a question, how should i write the recursion in Lean?

[Yaël Dillies]

Something like

def X (S : ℕ → ℝ) (a : ℝ) : ℕ → ℝ
  | 0 => sorry -- You didn't tell what you wanted here
  | k + 1 => X k - a * S k

[Yaël Dillies]

Maybe you will want to replace ℕ → ℝ with Fin n → ℝ for some n that you didn't specify to me

[haotian liu]

OK, Thank you very much!