Finite information-measure API

This file keeps a public re-export entry point for finite information measures while the canonical finite-discrete definitions live in LeanInfoTheory.Shannon.

Project theorem files and documentation should prefer the namespaced Shannon.* names when the distinction matters. The exported names in LeanInfoTheory are convenience aliases for users who import the project root.

The export list is intentionally explicit. Keeping the public names grouped by topic makes it easier to notice when a new foundation lemma should become part of the user-facing finite information-measure API.