statistical models

Stream: mathlib4

[Zixiao Wang]

Hi! I'm exploring the use of Lean 4 for formalizing statistical models, and I was wondering if there’s any existing guidance or libraries for representing parametric, nonparametric, or otherwise predefined statistical models. I tried searching for “parametric models” in the mathlib or community resources but didn’t find much that seemed related.

If anyone has pointers—whether design patterns, relevant definitions, or example developments—I’d really appreciate it. Thanks!

Best,
Zixiao

[Aaron Liu]

What exactly do you mean by "statistical model"?

[Zixiao Wang]

like a class or structure of parametric model?

[Aaron Liu]

We have stuff like docs#ProbabilityTheory.gaussianReal but I still don't know if that's what you're looking for.

[Aaron Liu]

This is "a family of probability distributions that has a finite number of parameters" (quote from Wikipedia)

[Zixiao Wang]

thanks for the info! yup i saw this, I was looking for a more generic version rather than restricting the distribution to be gaussian

[Aaron Liu]

Wdym generic version? What would a generic version look like?

[Aaron Liu]

Maybe docs#MeasureTheory.IsProbabilityMeasure, if you drop "gaussian" from "gaussian probability measure" that's what you get

[Aaron Liu]

I don't know what you want