Zulip Chat Archive
Stream: Is there code for X?
Topic: Information theory
Adomas Baliuka (Aug 06 2023 at 22:59):
Is there any lean4 treatment of e.g. Shannon's source coding theorem? I've seen something in Coq but not in Lean. Would something like this be included in Mathlib if someone ported it (well enough) from Coq?
Scott Morrison (Aug 07 2023 at 01:52):
No, and yes!
Notification Bot (Aug 07 2023 at 12:17):
ab has marked this topic as resolved.
Notification Bot (Aug 07 2023 at 20:17):
Ben Ryjikov has marked this topic as unresolved.
Notification Bot (Aug 07 2023 at 20:17):
Ben Ryjikov has marked this topic as unresolved.
Last updated: Dec 20 2023 at 11:08 UTC