ENNReal Komlos lemma proof draft - #358

Draft

Citronhat wants to merge 12 commits into

RemyDegenne:masterfrom

Citronhat:proof-cleanup

Commits on Dec 31, 2025

Draft: reorganize proof and add explanation for review
Citronhat
committed
3179707
dup
Citronhat
committed
48ba389
dap
Citronhat
committed
8624bec
gap
Citronhat
committed
1bb893c
Try to fix `komlos_ennreal` missing error.
Citronhat
committed
3c21ba1

Commits on Jan 1, 2026

Fix komlos_ennreal missing.
Citronhat
committed
02ca6f8

Commits on Jan 30, 2026

Commits on Feb 2, 2026

generalize to finite measures
RemyDegenne
committed
971741b

Commits on Feb 6, 2026

generalize to s-finite
RemyDegenne
committed
2c5ccca