This hand-written page lists the declarations that currently form the public mathematical story of the project. For a broader source-derived inventory, see the generated declaration index. Declaration names below link to their generated index entries, with direct source links beside them.

Finite entropy and information-measure layer
Mathematical statement Lean declaration Module Status
H(P) >= 0. Shannon.entropy_nonnegAPI index | source LeanInfoTheory.Shannon.Entropy Proved
H(delta_x) = 0. Shannon.entropy_pureAPI index | source LeanInfoTheory.Shannon.Entropy Proved
H(f_* P) = H(P) for an equivalence f. Shannon.entropy_map_equivAPI index | source LeanInfoTheory.Shannon.Entropy Proved
H(f_* P) = H(P) for an injective relabeling f. Shannon.entropy_map_injectiveAPI index | source LeanInfoTheory.Shannon.Entropy Proved
H(((A,B),C)) = H((A,(B,C))). Shannon.entropy_map_prodAssocAPI index | source LeanInfoTheory.Shannon.Entropy Proved
H(P) <= log |alpha| for a nonempty finite alphabet. Shannon.entropy_le_log_cardAPI index | source LeanInfoTheory.Shannon.EntropyBounds Proved
H(U_alpha) = log |alpha| for the uniform PMF. Shannon.entropy_uniformOfFintypeAPI index | source LeanInfoTheory.Shannon.EntropyBounds Proved
x_bits = x_nats / log 2. Shannon.natsToBitsAPI index | source LeanInfoTheory.Shannon.Units Defined
I(A;B) = I(B;A). Shannon.mutualInfo_map_swapAPI index | source LeanInfoTheory.Shannon.InfoMeasures Proved
I(A;B | C) = I(B;A | C). Shannon.condMutualInfo_map_swap12API index | source LeanInfoTheory.Shannon.InfoMeasures Proved
H(P) = E[-log P(X)] over PMF.toMeasure. Shannon.entropy_eq_integral_selfInfoAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Entropy Proved
H(A | B) = sum_b P_B(b) H(P_{A|B=b}). Shannon.condEntropy_eq_sum_sndMarginal_mul_condEntropyFstGivenSndAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Conditional Proved
0 <= H(A | B). Shannon.condEntropy_nonnegAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Theorems Proved
H(A,B) = H(B) + H(A | B). Shannon.entropy_eq_entropy_sndMarginal_add_condEntropyAPI index | source LeanInfoTheory.Shannon.InfoMeasures Proved
H(A | B,C) <= H(A | C). Shannon.condEntropy_le_condEntropy_fstThirdMarginalAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Theorems Proved
I(A;B) = D(P_AB || P_A x P_B). Shannon.mutualInfo_eq_toReal_klDiv_joint_indepProdAPI index | source LeanInfoTheory.Shannon.SemanticBridge.KL Proved
I(A;B | C) = sum_c P_C(c) I(A;B | C=c). Shannon.condMutualInfo_eq_sum_thirdMarginal_mul_condMutualInfoFstSndGivenThirdAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Conditional Proved
I(A;B | C) = sum_c P_C(c) D(P_{A,B|C=c} || P_{A|C=c} x P_{B|C=c}). Shannon.condMutualInfo_eq_sum_thirdMarginal_mul_condMutualInfoFstSndGivenThirdKLAPI index | source LeanInfoTheory.Shannon.SemanticBridge.KL Proved
0 <= I(A;B). Shannon.mutualInfo_nonnegAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Theorems Proved
0 <= I(A;B | C). Shannon.condMutualInfo_nonnegAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Theorems Proved
I(A;B,C) = I(A;C) + I(A;B | C). Shannon.mutualInfo_chain_rule_fstAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Theorems Proved
I(A;B,C) = I(A;B) + I(A;C | B). Shannon.mutualInfo_chain_rule_sndAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Theorems Proved
X -> Y -> Z iff its joint law is the canonical extension of P_XY through P_{Z|Y}. Shannon.isMarkovChain_iff_canonical_channelExtensionAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Markov Proved
X -> Y -> Z implies I(X;Z) <= I(X;Y). Shannon.mutualInfoOf_dataProcessingAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Markov Proved
Equality in Markov data processing holds iff X -> Z -> Y. Shannon.mutualInfoOf_dataProcessing_eq_iffAPI index | source LeanInfoTheory.Shannon.SemanticBridge.Markov Proved
D(pW || qW) <= D(p || q) for every finite stochastic channel W. Shannon.klDiv_channel_leAPI index | source LeanInfoTheory.Shannon.SemanticBridge.DataProcessing Proved
The real-valued KL channel inequality under input support inclusion. Shannon.toReal_klDiv_channel_leAPI index | source LeanInfoTheory.Shannon.SemanticBridge.DataProcessing Proved
A finite doubly stochastic channel cannot decrease entropy. Shannon.entropy_le_entropy_bind_of_doublyStochasticAPI index | source LeanInfoTheory.Shannon.SemanticBridge.DataProcessing Proved

Not Yet Covered

Canonical/minimal or general measurable sufficiency, exact Fano equality and sharpness, randomized/list decoding, AEP, source/channel coding theorems, and network converse examples are not formalized yet.