Skip to content

feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap#1098

Open
dennj wants to merge 1 commit into
leanprover-community:masterfrom
dennj:axiomatized-entropy
Open

feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap#1098
dennj wants to merge 1 commit into
leanprover-community:masterfrom
dennj:axiomatized-entropy

Conversation

@dennj
Copy link
Copy Markdown
Contributor

@dennj dennj commented May 13, 2026

No description provided.

@dennj dennj changed the title feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger ove… feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap May 13, 2026
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this file is getting pretty long now. Is it possible we can split it up into seperate modules (hopefully in line with some nice API structure)?

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, definitely a lot of this isn't "Defs". Most of it could go in another AxiomatizedEntropy file, the stuff that isn't filling in sorries already in there. At a minimum the Defs file shouldn't depend on the DPI file.

@jstoobysmith jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label May 14, 2026
@Timeroot
Copy link
Copy Markdown
Collaborator

Great, thank you!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants