Definintion of Bregman Divergence

Stream: Is there code for X?

[Harvey South]

I'd like to work with Bregman Divergences in lean, but I don't have a good enough background to convert the definition of a Bregman Divergence into lean. Does it already exist?

[Notification Bot]

This topic was moved here from #Is there code for X? > Bregman Divergence by HSouth.