Shannon entropy (base D)

For an implicit finite index type $\iota$ (supplied via a Fintype instance, i.e. any type known to have finitely many elements, with no constraint on what those elements represent), an arbitrary function $p:\iota\to\mathbb{R}$ (no hypothesis of nonnegativity, boundedness, or normalization is imposed — $p$ need not sum to $1$, need not be nonnegative, and individual values $p(i)$ may be zero, negative, or any real number), and a natural number $D:\mathbb{N}$ (used where a real number is expected, via the standard coercion, with no constraint such as $D\ge2$), the term entropy p D denotes the real number $-\sum_{i\in\iota} p(i)\cdot\log_D(p(i))$, where the sum ranges over every element of the finite type $\iota$ and $\log_D(x) := \dfrac{\log x}{\log D}$ is Mathlib's Real.logb, built from the natural logarithm Real.log under the stated total-function conventions: $\log 0 := 0$, and for $x<0$, $\log x := \log|x|$ (so Real.log is defined on all of $\mathbb{R}$, never undefined or infinite). Because Real.logb is literally the quotient of two Real.log values, and Mathlib's real division is a total function with $a/0:=0$ for every $a\in\mathbb{R}$, the two degenerate bases can be read off directly from the given definition: at $D=0$, $\log D=\log 0=0$ by the stated convention, so $\log_0(x)=\log(x)/0=0$ for every real $x$, making every summand $p(i)\cdot\log_0(p(i))=p(i)\cdot 0=0$ and hence entropy p 0 = 0 for every $p$; at $D=1$, $\log D=\log 1=0$ (the ordinary value of the natural logarithm at $1$), so likewise $\log_1(x)=\log(x)/0=0$ for every $x$, giving entropy p 1 = 0 for every $p$ as well — in both degenerate cases the entire expression collapses to $0$ regardless of $p$, with no case split, exception, or ill-defined term anywhere in the computation. For $D\ge2$, $\log D>0$ is the genuine natural logarithm, and $\log_D$ behaves as the ordinary base-$D$ logarithm on the positive reals; but since no positivity is assumed of $p$, for any index $i$ with $p(i)=0$ the summand is $0\cdot(\log 0/\log D)=0\cdot 0=0$ irrespective of $D$ (via the same $\log 0:=0$ convention, not a separately-imposed "$0\log 0:=0$" rule), and for any index $i$ with $p(i)<0$ the summand is $p(i)\cdot\bigl(\log|p(i)|/\log D\bigr)$ — the logarithm silently substitutes the absolute value of the negative input, yielding an ordinary (possibly negative, possibly positive) real number with no error raised; consequently entropy p D need not be nonnegative, need not be bounded, and carries no guarantee of matching any conventional notion of entropy unless further hypotheses on $p$ (e.g. nonnegativity, or normalization $\sum_i p(i)=1$) are supplied elsewhere — this declaration supplies none. The definition carries the noncomputable marker, a Lean computability annotation that does not affect the mathematical value described above.