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

golf proofs (suggested by Timeroot)

98831c4
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Verify Transient and Automated Commits
succeeded Jul 9, 2026 in 43s