Fractional operations

Stream: general

[Martin Dvořák]

Am I reïnventing the wheel?

I started developing API for fractional operations:
https://github.com/madvorak/fractional/

At this point, I should ask whether I am reïnventing the wheel.
Do we already have these notions in Mathlib?
Do we have this kind of theorems for them (such as I prove for my definitions) in Mathlib?

[Eric Wieser]

Do you really want to define this only for Fintypes?

structure Distr (α : Type) [Fintype α] : Type where
  theFun : α → ℝ
  nonNeg : 0 ≤ theFun
  sumOne : Finset.univ.sum theFun = 1

[Eric Wieser]

docs#PMF looks like the same thing

[Martin Dvořák]

Thanks for pointing it out! I didn't know about the definition in Mathlib.

[Eric Wieser]

There is also @Geoffrey Irving's https://github.com/google-deepmind/debate/blob/main/Prob/Pmf.lean, which argues that the builtin PMF is (or at least, was) hard to work with

[Geoffrey Irving]

I think PMF will always be harder to work with than finitely supported probability for a lot of applications, mostly because you can’t take a real expectation without knowing integrability. Sometimes you can’t deal only in ENNReal expectations, but then you don’t have a ring.

[Eric Wieser]

I would guess you could get a long way with something like a lift myPmf to FinsuppPmf in the middle of a proof or similar

[Eric Wieser]

mostly because you can’t take a real expectation without knowing integrability.

Hopefully this is a single theorem saying "for finite support, all PMFs are integrable"

[Geoffrey Irving]

If I want simp to apply 10 lemmas that rely on 6 things having finite support, including intermediate things that only exist in the middle of the simp, would that single theorem suffice?

[Eric Wieser]

If you also passed that theorem to simp, then yes

[Martin Dvořák]

I'm wondering whether I should use the Mathlib definition docs#PMF for everything.
For example, I have a theorem saying that the total variational distance cannot increase if you map both distributions by the same function:
https://github.com/madvorak/fractional/blob/f4ef8d0018dab67b9c7dda0b5f1939cdeeb783cb/Fractional/Distance.lean#L134
Would it be more difficult to prove analogical theorem for the Mathlib definitions?