Convenient types

Stream: Is there code for X?

[Pietro Lavino]

Working with measures, and I am wondering as I am setting up the early theorems whether it is convenient to use ".toReal" to convert values of measure from ℝ≥0∞ to ℝ or to leave everything in the type of ℝ≥0∞. Is this a significant choice or will it be trivial to switch back and forth?

[Kyle Miller]

Could you give some examples of theorems where you're making this decision?

[Yaël Dillies]

You might be interested in https://github.com/teorth/pfr/blob/master/PFR/ForMathlib/MeasureReal.lean

[Pietro Lavino]

Kyle Miller said:

Could you give some examples of theorems where you're making this decision?

I am trying to write in lean chapter 1 of the following book: https://56f05126-836c-454b-8ec9-915cf21f5646.filesusr.com/ugd/7e692e_ee12e0d539bf4403b4ac1947e6551edc.pdf , so everything in there for now. In proving for example the maximal entropy there is quite a bit of manipulation to be done with sums and measures. For now it seems to be working but I am wondering more for the rest of the theorems. A choice I made so far is in the definition of entropy to convert the measure of terms in partitions to real numbers. Next theorems are the one in proposition 1.7 like the relation between the entropy and information function

[Yaël Dillies]

Oh do you know that PFR has a formalisation of entropy? In fact, a lot of the dependency graph is about entropy.

[Pietro Lavino]

Yaël Dillies said:

Oh do you know that PFR has a formalisation of entropy? In fact, a lot of the dependency graph is about entropy.

what is PFR?

[Yaël Dillies]

It is the project to formalise the Polynomial Freiman-Ruzsa conjecture, aka Marton's conjecture. You can find information here: https://teorth.github.io/pfr

[Pietro Lavino]

(deleted)