Prove Independence

Stream: new members

[SamuelShen]

My advisor asked me to study the Lean language and suggested that I try to prove the following proposition using Lean:

Let X₁, X₂, ..., Xₙ be a random sample drawn from a normal distribution N(μ, σ²). Define the sample mean X̄ and the sample variance S² as follows:

X̄ = (1/n) ∑ (from i = 1 to n) Xᵢ,
S² = (1/(n-1)) ∑ (from i = 1 to n) (Xᵢ - X̄)².

The goal is to prove that S² and the sample mean X̄ are statistically independent.

I already have a proof outline: First, both the sample mean X̄ and (X_i - X̄) are normally distributed variables. By calculating the expected value of their product, we find it to be 0, which implies that their covariance is 0. Since they are normally distributed variables, having zero covariance implies independence. Hence, it is clear that the sample mean X̄ is independent of each term within the summation of S², which means S² and X̄ are statistically independent.

My question is how to translate this proof outline into Lean code. Any assistance would be greatly appreciated! (I have already configured my Lean environment.)

Thank you in advance for your help!

[Riccardo Brasca]

Do you have any experience with Lean? Also, may I ask who is your advisor?

[SamuelShen]

I am pretty new to Lean

[SamuelShen]

I think I need package about Gaussian distribution?

[Riccardo Brasca]

We have ProbabilityTheory.gaussianReal that should be the gaussian distribution (I don't know anything about how probability is done in mathlib). Anyway if you are pretty new to Lean it is probably better to familiarize a little bit with the language, for example spending a couple of hours playing the natural number game.

[SamuelShen]

Thank you! very good advice! I would take it!

[Vincent Beffara]

Note that it is not true in general that uncorrellated gaussians are independent, the implication only holds for the components of a Gaussian vector. And since we only have real valued gaussians in mathlib you will have to essentially start proving basic things about Gaussian vectors, starting with the definition.

[Vincent Beffara]

This does not feel like a beginners project ...