chore: bump mathlib to be31cde, preserve PMF APIs

[mathlib-nightly-testing]

Bump Mathlib from 9a6fbe0 to be31cde, preserving CSLib's PMF-based probability APIs.

The new Mathlib uniform-sampler aliases return measures, so suppressing deprecation warnings alone cannot compile the existing code. Keep a small compatibility shim in Cslib.Probability.PMF for uniformOfFinset, uniformOfFintype, and the three lemmas used downstream. The shim adapts the previous Mathlib definitions, with credit to Josha Dekker, Devon Tuma, and Kexing Ying.

The crypto files only change sampler imports and references. Their PMF models and proofs are preserved, deferring the broader probability API decision. Regression tests cover singleton sampling, a proper finite subset, and a uniform four-element sample mapped to a fair bit; the existing crypto tests continue to pass.

Validation:

• lake build --wfail --iofail
• lake exe mk_all --check
• lake test
• lake lint
• lake exe lint-style

AI assistance: Codex prepared the compatibility shim, restored the PMF APIs, added regression tests, and ran the checks above.

Closes #1078

[SamuelSchlesinger]

I've migrated to measure theory for the impacted aspects of this PR. Curious to get anyone else's perspective. For me, this lowers my comprehension and requires me to think about measures and what these terms mean more than I want to. However, I am not opposed to this if Mathlib is going to deprecate PMF after all.

Some more eyes other than me would be ideal, but I'll continue to think about this tonight and tomorrow.

[SamuelSchlesinger]

cc @crei

[chenson2018]

Just to repeat some conversation that Sam and I had earlier. There are a couple of short-term options:

• The first option is to keep the changes they've already pushed. I would do this if you're fairly certain that we'd like to head in the same direction as Mathlib here. (NB: if your pushed changes used AI, please edit to PR description to say so as usual)
• An alternative if you're not sure yet how you'd like to refactor: we can kick the can and have six months until these are removed from Mathlib. You would turn off warnings for just these specific theorems and merge essentially unchanged. I'd ask if you do this that you follow up on Zulip to make a more permanent decision.

I typically advocate very hard for staying aligned with Mathlib, and Sam mentioned some evidence that it could be useful here, along with innovations in do notation (see Lean Machine Learning > Do notation for Giry monad for instance) that might make working with things easier. I know there were some arguments from the other as as well though in CSLib > PMF monad and discrete probability.

I'll leave all this to your discretion, I just ask that one of these options gets merged in this PR fairly soon, please feel free to merge as soon as you decide. (There is not a rush, but I usually try to not go more than a couple of days before merging these.)

[SamuelSchlesinger]

I'm going to suppress the warnings for now and have a think about this and then write something up on the Zulip. I think these proofs and theorem statements are just worse the way things are on this PR.

[SamuelSchlesinger]

I'll push something up in a few minutes.