ENNReal Komlos lemma proof draft

[Citronhat]

Hi all,

First of all, I apologize for not making an update sooner. My trusted, old laptop gave up on me, and since a lot of my previous work was only in local commits, a lot of code was missing when I finally got a new machine.

This PR is a draft: it contains a working proof of komlos_ennreal, but the current state is not up to standard. The file is too long, and the structure deviates quite a bit from the blueprint proof.

Here is a broad overview of the proof strategy implemented:

1. Transformation: We map ENNReal values to [0, 1] using expInv (essentially $x \mapsto e^{-x}$, with $\infty \mapsto 0$). This allows us to work with bounded random variables.
2. Strict Convexity & Defect: We exploit the strict convexity of the exponential inverse. We define a defect function that quantifies how much the midpoint inequality is strict. The lemma, quantitative_convexity, relates the distance between points to this defect.
3. Abstract Komlós: We apply the komlos_convex lemma to the functional $\phi(X) = \mathbb{E}[ ext{expInv}(X)]$. This gives us a sequence of convex combinations $g_n$ where the functional values behave well.
4. $L^1$ Convergence: Using the defect estimates (prob_large_diff_le_defect), we show that the transformed sequence $ ext{expInv}(g_n)$ is Cauchy in $L^1$. This is the analytic core, translating the functional convergence from the abstract lemma into convergence in probability/mean.
5. Back to ENNReal: From $L^1$ convergence, we extract an almost surely convergent subsequence. We then use logNeg (inverse of expInv) to transfer this convergence back to the original ENNReal random variables.

I would appreciate any feedback on how to better structure this. Is the proof salvageable? If not, I am readily willing to pass the torch to someone more suitable. I have already spent way more time on the proof than I care to think about.

Closes #249