Skip to content

feat(Analysis/SpecialFunctions): add the Chase-Lovett diagonal reduction for binEntropy#41523

Open
Harmenszoon wants to merge 2 commits into
leanprover-community:masterfrom
Harmenszoon:frankl-binentropy-diagonal
Open

feat(Analysis/SpecialFunctions): add the Chase-Lovett diagonal reduction for binEntropy#41523
Harmenszoon wants to merge 2 commits into
leanprover-community:masterfrom
Harmenszoon:frankl-binentropy-diagonal

Commits

Commits on Jul 9, 2026