Komlós Lemma - #399

Merged

RemyDegenne merged 37 commits into

RemyDegenne:masterfrom

May 1, 2026

Commits on Apr 24, 2026

Komlos lemma initial draft
TBUGTB
committed
2f5dbe4
feat(blueprint): more details on Komlos construction
TBUGTB
committed
7fa3bd6
refactor(blueprint): reindex \tilde{g}
TBUGTB
committed
03c0e09
feat(Komlos Lemma): detailed formal draft for Komlos construction
TBUGTB
committed
9bd30d4
fix(Komlos lemma): correct typos and author note
TBUGTB
committed
e2d056d
feat(Komlos): congruence lemma for komlos_formula
TBUGTB
committed
09843d6
refactor(ConvexWeights): golf proof
TBUGTB
committed
f506634
feat(Komlos): complete scaffolding for komlos_convex_weights
TBUGTB
committed
836eba6
refactor: rename to follow Mathlib style guide
TBUGTB
committed
9483676
refactor: use Finsupp.sum instead of Finset.sum
TBUGTB
committed
92091c3
feat(Komlos): finish proof of komlos_base
TBUGTB
committed
a0d556e
feat(Komlos): progress in komlos_step
TBUGTB
committed
970c607
feat(ConvexWeights): Add missing basic lemmas
TBUGTB
committed
3c023fe
feat(ConvexWeights): AI-generated proofs for simple lemmas
TBUGTB
committed
79e5f5f
refactor(Komlos): general cleanup
TBUGTB
committed
59ba5af
feat(Komlos): Prove remaining sorry
TBUGTB
committed
81ccba7
fix(blueprint): add missing \leanok
TBUGTB
committed
1bf5e1f
refactor(Komlos): separate out lemma from long proof
TBUGTB
committed
d8472a3
refactor(Komlos): fix linter errors
TBUGTB
committed
d14c9b3
feat(Komlos): add remaining intermediate Komlos lemmas
TBUGTB
committed
2509afb
refactor: use StdSimplex for representing convex weights

TBUGTB
and
Copilot
committed
af1b500
feat(Komlos): prove first weights are zero
TBUGTB
committed
4585b0e
refactor(Komlos): move global gtilde inside proof
TBUGTB
committed
f37c90f
fix(Komlos): add missing declnames in blueprint
TBUGTB
committed
880f044
fix(Komlos): fix linter message
TBUGTB
committed
da1f34d

Commits on Apr 27, 2026

refactor(ConvexWeights): lemmas on convex weights
TBUGTB
committed
d653b44
refactor: further cleanup of proofs
TBUGTB
committed
0910d27
refactor(Komlos): golf proof
TBUGTB
committed
04fd754

Commits on Apr 28, 2026

refactor: golf
TBUGTB
committed
de87a8e
refactor(Komlos): golf
TBUGTB
committed
756be15
fix: blueprint fixes
TBUGTB
committed
031b0b1

Commits on Apr 29, 2026

refactor: rename convexWeightsMul to StdSimplex.bind
TBUGTB
committed
718051f

Commits on Apr 30, 2026

Apply suggestions from code review

TBUGTB
and
RemyDegenne
authored
8dd4517
fix: repair proofs broken by accepting quick changes
TBUGTB
committed
da5fad4
chore: import new file in BrownianMotion.lean
TBUGTB
committed
9c67464

Commits on May 1, 2026

refactor(Komlos): generalize komlos_convex to ordered semifield
TBUGTB
committed
c33c1ad
refactor: implement review suggestions
TBUGTB
committed
4b4a72c