posterior distribution calculation

Stream: maths

[leo Robert]

I am currently thinking about how to calculate the posterior distribution of the following problem:

1. Let x1, . . . , xm be i.i.d. sample from a normal distribution with mean \mu and variance \sigma^2. Suppose for each x_i we observe y_i = |x_i| rather than x_i. How do I calculate the posterior distribution of p(x_i | y_i, \mu, \sigma^2) for this problem?
2. In addition, can we directly derive the gradient of the parameters \mu and \sigma^2? Use the log-likelihood function l(\mu, \sigma^2; y) to derive the parameters. I found that this seems to be difficult to find because the distribution of y is more complicated.

[Rémy Degenne]

Short answer: at the moment we don't have the tools that would allow an easy computation.

Let's proceed with the longer answer.
You can express the conditional distribution of x given y with ProbabilityTheory.condDistrib, which is formally a Markov kernel (ProbabilityTheory.Kernel).

Alternatively, it might be easier to not work with random variables but with measures and Markov kernels. You have a Gaussian measure that you map by a measurable function (the absolute value). You can identify the function with its deterministic kernel and use the definition of a posterior kernel that I wrote here: https://github.com/RemyDegenne/testing-lower-bounds/blob/0f09ff100a06a5e4542181514bfff74213ae126b/TestingLowerBounds/Kernel/BayesInv.lean#L43 . What is called bayesInv there is a posterior (it's called Bayesian inverse in some parts of the literature). However note that this is not in Mathlib but in another project and the lemmas about it depend on other results from that project.

That does not tell you much about how you can actually compute the posterior, and I am afraid that at the moment Mathlib will have very few lemmas to help you with that, but at least you can write that object in Lean.

[Rémy Degenne]

Sorry I just saw that this is in the #maths channel, and not #Is there code for X? . Are you asking about how to do it in Lean, or how to do it in paper maths?

[leo Robert]

Yeah, I want to ask how to do it in paper math

[Kevin Buzzard]

Then why are you asking on the lean Zulip? :-)