Definition of pdf as rnDeriv

Stream: mathlib4

[Thomas Zhu]

Why is docs#MeasureTheory.pdf not defined as pdf X ℙ μ := (map X ℙ).rnDeriv μ? It seems to me the RN derivative is a more natural definition, and HasPDF X ℙ μ can be defined (rather than proven as docs#MeasureTheory.pdf.hasPDF_iff) as Measurable X ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ. As far as I can understand, this definition is equivalent to the current definition. Then it seems many lemmas about pdf can use lemmas about rnDeriv.

Also having the (definitional) equality pdf X ℙ μ = (map X ℙ).rnDeriv μ would be really nice. Right now both pdf and rnDeriv are defined using Classical.choose, and one can only prove this equality in general up to ae under additional assumptions like SigmaFinite μ.

[Ruben Van de Velde]

Does it predate rnDeriv?

[Thomas Zhu]

Ruben Van de Velde said:

Does it predate rnDeriv?

It could; the headers of both files say 2021 written by @Jason KY. and I'm not familiar with development of mathlib3. @Jason KY. was there any reason pdf was defined independent of rnDeriv?

[Jason KY.]

They were written at the same time IIRC which is the reason. I think it would be a good idea to try changing the definition of pdfs since I'm not very happy with the definition myself. @Rémy Degenne has also added a lot of API for working with rnDeriv so it is probably much easier to do so now as well

[Jason KY.]

I think one reason why pdf is defined like this is that with the current formulation you can talk about density wrt any measure while with rnDeriv it is only meaningful when you have a HaveLebesgueDecompositon

[Jason KY.]

But I suppose in probability theory you only really care about the density wrt to the Lebesgue measure anyhow so it is not a big reason

[Thomas Zhu]

Yes, and also doesn't HasPDF already imply HaveLebesgueDecomposition? docs#MeasureTheory.pdf.haveLebesgueDecomposition_of_hasPDF

[Jason KY.]

Oh yes, that correct. So I guess I have no worries then :)

[Thomas Zhu]

I am willing to do a draft PR of changing the definition of pdf to rnDeriv if that's a better definition.

[Thomas Zhu]

The reason this came up is that I am working on some entropy lemmas for my own, and it would be nice to define entropy of a measure to be the expectation of the log RN derivative wrt this measure, but also the entropy of a random variable to be the expectation of pdf * log(pdf). If pdf is definitionally equal to rnDeriv, then the measure definition of entropy would be essentially the same as the entropy of a random variable.

[Yaël Dillies]

@Thomas Zhu, you should check out teorth.github.io/pfr. We have a definition of entropy and an ever growing list of lemmas about it.

[Thomas Zhu]

Yaël Dillies said:

Thomas Zhu, you should check out teorth.github.io. We have a definition of entropy and an ever growing list of lemmas about it.

Hi! I just found out about this amazing project. I was working on some lemmas on my own (for fun, not intending to PR), but your lemmas are already covering much more than what I have! I would only be additionally interested in entropy over an infinite probability space over a reference measure other than the counting measure (i.e. H(ν) = ∫ log(dν/dμ) ∂ν vs H(p) = ∑ -p(x)log(p(x))), which I think the project doesn't need?

[Rémy Degenne]

We will not prove lemmas about that for the PFR project, indeed. I have proved a few in this branch of mathlib, if you want to have a look: branch#RD_kl . Look at the file Mathlib/Probability/Divergences/KullbackLeibler

[Rémy Degenne]

I proved that it's nonnegative, as well as a version of the Donsker-Varadhan duality formula

[Yaël Dillies]

What's the plan for integration in mathlib, actually? Should we migrate the PFR lemmas about entropy to your definition?

[Rémy Degenne]

(I am slowly PRing stuff to mathlib about withDensity, rnDeriv and soon tilted measures. Those results come next)

[Rémy Degenne]

Yaël Dillies said:

What's the plan for integration in mathlib, actually? Should we migrate the PFR lemmas about entropy to your definition?

I don't know exactly how we should transfer the entropy results of PFR to mathlib, but I think there is room for a definition of entropy in finite spaces, separate from the Kullback-Leibler divergence definition.

[Thomas Zhu]

I agree, I think proving results / algorithms on finite spaces like the Huffman code are still significant.

[Thomas Zhu]

On an unrelated note, I think HasPDF should be defined as a def or structure like HasDerivAt or HasSum, not a class? Currently I don't think there should be many scenarios where you would want to infer an instance of HasPDF implicitly rather than explicitly showing HasPDF. https://github.com/leanprover-community/mathlib4/blob/c6979569edc545f999b82d8a833b190c918aec2e//Mathlib/Probability/Density.lean#L68-L71