Using refinement types

Stream: new members

[Kamila Szewczyk]

Hi, I have defined the Shannon Entropy function as follows:

noncomputable
def entropy (p : List ℝ) : ℝ := p.foldl (fun acc p => acc - p * log p) 0

How do I add extra bounds to it, like the size of p (>0), the fact that p must sum up to 1, and that all elements of p must be non-negative?

[Yaël Dillies]

You don't, but you state theorems with those assumptions added.

[Yaël Dillies]

Here is entropy in PFR, if you want inspiration: https://github.com/teorth/pfr/tree/master/PFR/ForMathlib/Entropy

[Kamila Szewczyk]

I see.. Unrelated question: If I have (h2 : x <= 1), how do I destructure it so that i can prove the statement independently for x < 1 and x == 1?

[Michael Stoll]

cases h2.eq_or_lt or rcases h2.eq_or_lt with h | h.

[Ruben Van de Velde]

Note that the first underscore should be a dot

[Ruben Van de Velde]

By the way, unrelated questions tend to go in new topics

[Kamila Szewczyk]

Thank you!

[Michael Stoll]

Ruben Van de Velde said:

Note that the first underscore should be a dot

Fixed.