Normal Distribution

Stream: new members

[Joshua Banks]

Hi, I am new to lean and trying to prove properties of normal distribution, does anyone have any idea about I could represent the mean and variance in lean. Thanks for any help.

[Kevin Buzzard]

A couple of students at Imperial have been working on the Gaussian, although they didn't push anything since October. Their work is here.

[Kalle Kytölä]

There are ways of talking about the mean (expected value) and variance of a real random variable in Lean, but unfortunately Gaussian distributions are not yet in mathlib (at least not with enough API to make them usable without a lot of work). (Kevin's link above contains work on such topics that is not yet in mathlib.)

Some possible spellings of such things in Lean are in the following. (Although I would prefer more direct statements about probability measures on ℝ instead of indirect statements about the laws of ℝ-valued random variables, but Gaussians are not yet in mathlib in either form...)

import probability.moments

open measure_theory

-- Let (Ω, F, ℙ) be a probability space.
variables {Ω : Type} [measurable_space Ω] (ℙ : measure Ω) [is_probability_measure ℙ]

-- Let Z be a real-valued random variable on this probability space.
variables (Z : Ω → ℝ) (Z_mble : measurable Z)

-- The distribution of the random variable Z (a probability measure on ℝ) under ℙ is spelled `ℙ.map Z`:
#check ℙ.map Z

-- I doubt that gaussian distributions have been defined in Lean's mathlib yet, so
-- at this point you should probably make further assumptions on the distribution of Z.
-- For example using the repo that Kevin linked to, one could write:
-- `variables m s : ℝ`
-- `variables measure.real_gaussian (ℙ.map Z) m s`

-- In any case, towards the spelling of the expected value and the variance...

-- The expected value of Z is its integral w.r.t. ℙ, which can be expressed in Lean as `∫ ω, Z ω ∂ℙ`:
#check ∫ ω, Z ω ∂ℙ
-- (For Z ∉ L¹(ℙ) this yields a junk value, as the expected value is ill-defined.)
-- Another spelling of the same thing is:
#check probability_theory.moment Z 1 ℙ

-- The variance of Z can be expressed in Lean as:
#check probability_theory.variance Z ℙ
-- (For Z ∉ L²(ℙ) this yields a junk value. `probability_theory.evariance Z ℙ` is
-- a safer but possibly less convenient [0, +∞] -valued alternative.)
-- Another spelling of the same thing is:
#check probability_theory.central_moment Z 2 ℙ

[Joshua Banks]

Thanks a lot for your comments that's very helpful and clarifies my issues currently

[Joshua Banks]

Image-09-02-2023-at-23.32.jpeg

I'm not sure if this is possible or how to go about doing so but does anyone know how this could be translated into a lemma in lean? My main area of confusion is how I would assume X is Standard normally distributed

[Kevin Buzzard]

You could just avoid the probability and write the integral directly

[Jason KY.]

Elaborating on Kevin's comment, you can use measure_theory.measure.with_densityto say the push forward measure of P along the random variable X is the Lebesgue measure with Gaussian density.