Helper

logr_eq1

Section log_extra

Type Lemma

Proof Lines 10

Lemma logr_eq1 (x : R) : 0 < x -> (log x = 0) <-> (x = 1).

log x = 0 iff x = 1 (for positive x). This is fundamental for entropy calculations where log(prob) = 0 implies the probability is 1 (certainty).

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...