feat(Entropy): prove sandwiched Rényi DPI; remove axiom

[dennj]

Replace sandwichedRenyiEntropy_DPI_ax with a real proof via complex interpolation. Also prove faithful for any axiomatic relative entropy (Tomamichel construction), so RelEntropy qRelativeEnt instantiates without sorry. The downstream SteinsLemma.limit_hypotesting_eq_limit_rel_entropy loses one axiom.

Side effects: extract classical Hellinger overlap to a new ClassicalInfo/Hellinger.lean, split unbundled matrix-map properties into CPTPMap/Unbundled.lean, add a few upstream-worthy lemmas to ForMathlib/, and inline a number of single-use private helpers across Dual.lean, Relative.lean, and DPI.lean.

This PR is quite big and I need some help to simplify and golfing

[jstoobysmith]

@Timeroot made a PR that added some results to QuantumInfo which means there is a merge conflict with this PR now.

[Timeroot]

Wow @dennj, this is a very nice work! I had tried to coax an AI to do this mostly autonomously but it was still quite tricky. I had a proof of the same about a month ago (that I was slow to get merged, but is in there now), but this is still very valuable; it looks a more nicely self-contained proof. I didn't think that Mathlib was very well equipped to do the complex interpolation proof which is why I'm a bit surprised this went through!

I'm also very happy to see the cleanup in Dual.lean and in AxiomatizedEntropy. :) I guess I had the definition of dual wrong, so I'm glad that you fixed that; the proofs in AxiomatizedEntropy made me realize I had the definition of min wrong (it says ProjLE, your proof shows that it becomes trivial; it actually should be ProjLT now that I think about it). Awesome stuff. 😄

It'll definitely take me a bit of time to go through and merge/clean this.

As a first step, do you think you could pull of a separate PR that has all this /except/ for the stuff in DPI.lean, AxiomatizedEntropy, and ResourceTheory? Those remaining files all should be much easier for me to merge pretty much right away - they're obvious improvements and no merge conflicts.

Then, a PR for the AxiomatizedEntropy stuff would be the next I'd be happy to do. That should be pretty quick modulo a few fixes I'd like to make.

That will leave this PR then with the DPI.lean code. (The ResourceTheory files can be dropped, since those were already changed the same way, in master.) I'll go through that. I'm not sure atm if we'll use this new proof or the other proof of DPI, but either way it'll be best to keep both around since a lot of the machinery can be reused for other stuff either way.

[Timeroot]

Btw Dennj, if you want to put yourself as an author on Dual.lean, I think you've totally earned that... fixing the definition of dual is pretty critical. :)