Generated by scripts/generate_website_api_index.py from local Lean source files. This supplementary inventory includes non-stable examples and reference anchors. Source links target current development on master; dirty local lines may differ from that branch. Maintenance staging pins these links to its exact site commit. Current supported coverage is recorded in docs/current-public-api.json. The separate frozen v0.1.0 signature-bearing reference documents the released 601 declarations in 31 modules.

Current Index

718non-private source declarations
35modules with declarations
602theorems and lemmas
110definitions and abbrevs
717with doc comments

Declaration Kinds

Kind Count
Definition110
Inductive4
Instance2
Theorem602

Declarations

Declaration Kind Module Doc comment Source
LeanInfoTheory.projectNameDefinitionLeanInfoTheory.BasicPublic project name used by documentation and the website.line 23
LeanInfoTheory.StatusInductiveLeanInfoTheory.BasicA small status vocabulary for roadmap items and generated documentation.line 26
LeanInfoTheory.Examples.CommonCause.causeLawDefinitionLeanInfoTheory.Examples.CommonCauseA fair binary common cause.line 32
LeanInfoTheory.Examples.CommonCause.noisyCopyDefinitionLeanInfoTheory.Examples.CommonCauseA binary channel that copies its input correctly with probability `3 / 4`.line 35
LeanInfoTheory.Examples.CommonCause.noisyCopy_massesTheoremLeanInfoTheory.Examples.CommonCauseBoth channel rows are genuinely random and depend on the input.line 62
LeanInfoTheory.Examples.CommonCause.lawDefinitionLeanInfoTheory.Examples.CommonCauseTwo noisy observations sampled independently from the same binary cause.line 68
LeanInfoTheory.Examples.CommonCause.law_isMarkovTheoremLeanInfoTheory.Examples.CommonCauseThe observation-cause-observation law is a Markov triple.line 73
LeanInfoTheory.Examples.CommonCause.endpoints_condIndependentTheoremLeanInfoTheory.Examples.CommonCauseThe two observations are conditionally independent given their common cause.line 77
LeanInfoTheory.Examples.CommonCause.positiveFiber_isIndependentTheoremLeanInfoTheory.Examples.CommonCauseEvery positive-mass cause fiber has an independent endpoint law.line 83
LeanInfoTheory.Examples.CommonCause.endpoint_condMutualInfo_eq_zeroTheoremLeanInfoTheory.Examples.CommonCauseThe endpoint conditional mutual information given the cause vanishes.line 92
LeanInfoTheory.Examples.CommonCause.law_eq_canonical_channelExtensionTheoremLeanInfoTheory.Examples.CommonCauseThe canonical total conditional channel reconstructs the common-cause law.line 100
LeanInfoTheory.Examples.CommonCause.law_eq_some_channelExtensionTheoremLeanInfoTheory.Examples.CommonCauseSome channel from the cause reconstructs the common-cause law.line 106
LeanInfoTheory.Examples.Fano.PerfectDecoder.condEntropy_diagonal_eq_zeroTheoremLeanInfoTheory.Examples.FanoA diagonal Boolean joint law has zero conditional entropy under the identity decoder. This specializes the expanded PMF form of Fano's inequality.line 36
LeanInfoTheory.Examples.Fano.SingletonSource.condEntropy_eq_zeroTheoremLeanInfoTheory.Examples.FanoFano's q-ary form includes a singleton source alphabet without a public cardinality lower bound. Every decoder is necessarily correct on that source.line 64
LeanInfoTheory.Examples.Fano.BinaryConstantObservation.decodingErrorProbabilityOf_eq_halfTheoremLeanInfoTheory.Examples.FanoFor a fair Boolean source, a constant-false observation decoded by the identity function has error probability `1/2`.line 85
LeanInfoTheory.Examples.Fano.BinaryConstantObservation.condEntropyOf_le_binEntropy_halfTheoremLeanInfoTheory.Examples.FanoThe random-variable expanded Fano theorem bounds the conditional entropy in the constant-observation example by binary entropy at error probability `1/2`.line 108
LeanInfoTheory.Examples.Fano.BinaryConstantObservation.mutualInfoOf_fano_lower_boundTheoremLeanInfoTheory.Examples.FanoThe uniform-source mutual-information corollary specializes directly to the binary constant-observation example.line 122
LeanInfoTheory.Examples.Fano.BinaryConstantObservation.decodingErrorProbabilityOf_fano_lower_boundTheoremLeanInfoTheory.Examples.FanoThe normalized uniform-source converse gives a concrete lower bound on the same binary decoding-error probability.line 140
LeanInfoTheory.Examples.FiniteFamily.BooleanModel.VarInductiveLeanInfoTheory.Examples.FiniteFamilyNames for two source bits and their parity bit.line 38
LeanInfoTheory.Examples.FiniteFamily.BooleanModel.sourceDefinitionLeanInfoTheory.Examples.FiniteFamilyA uniform two-bit source.line 45
LeanInfoTheory.Examples.FiniteFamily.BooleanModel.coordinatesDefinitionLeanInfoTheory.Examples.FiniteFamilyThe two source coordinates together with their parity.line 49
LeanInfoTheory.Examples.FiniteFamily.BooleanModel.lawDefinitionLeanInfoTheory.Examples.FiniteFamilyThe full law of the Boolean family.line 55
LeanInfoTheory.Examples.FiniteFamily.BooleanModel.orderDefinitionLeanInfoTheory.Examples.FiniteFamilyThe order used by the mutual-information chain-rule example.line 59
LeanInfoTheory.Examples.FiniteFamily.BooleanModel.mutualInfo_chain_ruleTheoremLeanInfoTheory.Examples.FiniteFamilyThe family mutual-information chain rule on the Boolean model.line 63
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.VarInductiveLeanInfoTheory.Examples.FiniteFamilyNames for a Boolean coordinate and a ternary coordinate.line 311
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.AlphabetDefinitionLeanInfoTheory.Examples.FiniteFamilyThe coordinate alphabet, which depends on the variable name.line 317
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.sourceDefinitionLeanInfoTheory.Examples.FiniteFamilyA uniform source carrying one Boolean and one ternary coordinate.line 331
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.coordinatesDefinitionLeanInfoTheory.Examples.FiniteFamilyThe dependent family of source coordinates.line 335
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.lawDefinitionLeanInfoTheory.Examples.FiniteFamilyThe full law of the heterogeneous family.line 340
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.orderDefinitionLeanInfoTheory.Examples.FiniteFamilyThe textbook order of the two heterogeneous coordinates.line 344
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.entropy_chain_ruleTheoremLeanInfoTheory.Examples.FiniteFamilyThe source-family entropy chain rule for dependent coordinate alphabets.line 348
LeanInfoTheory.Examples.FiniteFamily.HeterogeneousModel.empty_entropyTheoremLeanInfoTheory.Examples.FiniteFamilyThe empty heterogeneous subfamily has zero entropy.line 357
LeanInfoTheory.Examples.KLTop.leftLawDefinitionLeanInfoTheory.Examples.KLTopThe pure law at `false`.line 37
LeanInfoTheory.Examples.KLTop.rightLawDefinitionLeanInfoTheory.Examples.KLTopThe pure law at `true`, whose support is disjoint from `leftLaw`.line 40
LeanInfoTheory.Examples.KLTop.laws_neTheoremLeanInfoTheory.Examples.KLTopThe two pure laws are unequal.line 43
LeanInfoTheory.Examples.KLTop.not_absolutelyContinuousTheoremLeanInfoTheory.Examples.KLTop`leftLaw` is not absolutely continuous with respect to `rightLaw`.line 49
LeanInfoTheory.Examples.KLTop.klDiv_eq_topTheoremLeanInfoTheory.Examples.KLTopFailed support inclusion makes the KL divergence infinite.line 56
LeanInfoTheory.Examples.KLTop.toReal_klDiv_eq_zeroTheoremLeanInfoTheory.Examples.KLTopTaking `ENNReal.toReal` sends the infinite KL value to zero.line 62
LeanInfoTheory.Examples.KLTop.toReal_zero_trapTheoremLeanInfoTheory.Examples.KLTopWithout absolute continuity, real-valued KL can be zero for two unequal laws; this is the branch excluded by `toReal_klDiv_pmf_eq_zero_iff`.line 71
LeanInfoTheory.Examples.StochasticChannels.averagingChannelDefinitionLeanInfoTheory.Examples.StochasticChannelsA non-permutation channel that replaces every input by a fair bit.line 37
LeanInfoTheory.Examples.StochasticChannels.entropy_le_after_averaging_via_invariantTheoremLeanInfoTheory.Examples.StochasticChannelsUniform invariance proves entropy growth for the averaging channel.line 55
LeanInfoTheory.Examples.StochasticChannels.entropy_le_after_averaging_via_columnsTheoremLeanInfoTheory.Examples.StochasticChannelsThe direct column-sum criterion proves the same entropy comparison.line 61
LeanInfoTheory.Examples.StochasticChannels.entropy_strictly_increases_from_pureTheoremLeanInfoTheory.Examples.StochasticChannelsAveraging strictly raises the entropy of a pure binary input.line 67
LeanInfoTheory.Examples.StochasticChannels.biasedLawDefinitionLeanInfoTheory.Examples.StochasticChannelsA full-support nonuniform reference law.line 74
LeanInfoTheory.Examples.StochasticChannels.biasedResetDefinitionLeanInfoTheory.Examples.StochasticChannelsA channel that resets every input to the nonuniform reference law.line 88
LeanInfoTheory.Examples.StochasticChannels.biasedLaw_ne_uniformTheoremLeanInfoTheory.Examples.StochasticChannelsThe invariant reference in this example is not the uniform law.line 91
LeanInfoTheory.Examples.StochasticChannels.biasedLaw_invariantTheoremLeanInfoTheory.Examples.StochasticChannelsThe nonuniform reference law is invariant under the reset channel.line 100
LeanInfoTheory.Examples.StochasticChannels.klDiv_contracts_toward_biasedTheoremLeanInfoTheory.Examples.StochasticChannelsOne reset step contracts KL divergence toward the nonuniform invariant law.line 105
LeanInfoTheory.Examples.StochasticChannels.leftLawDefinitionLeanInfoTheory.Examples.StochasticChannelsThe first of two source laws with disjoint support.line 112
LeanInfoTheory.Examples.StochasticChannels.rightLawDefinitionLeanInfoTheory.Examples.StochasticChannelsThe second of two source laws with disjoint support.line 115
LeanInfoTheory.Examples.StochasticChannels.source_support_not_subsetTheoremLeanInfoTheory.Examples.StochasticChannelsThe source support condition for real-valued cascade contraction fails.line 118
LeanInfoTheory.Examples.StochasticChannels.intermediate_laws_eqTheoremLeanInfoTheory.Examples.StochasticChannelsThe averaging stage merges the two source laws.line 123
LeanInfoTheory.Examples.StochasticChannels.intermediate_support_subsetTheoremLeanInfoTheory.Examples.StochasticChannelsSupport inclusion is restored after the averaging stage.line 128
LeanInfoTheory.Examples.StochasticChannels.klDiv_cascade_contractsTheoremLeanInfoTheory.Examples.StochasticChannels`ENNReal`-valued KL contracts along the two stochastic stages.line 134
LeanInfoTheory.Examples.StochasticChannels.toReal_klDiv_cascade_contracts_from_intermediateTheoremLeanInfoTheory.Examples.StochasticChannelsThe one-stage theorem gives the weaker intermediate-support real cascade contract directly, without requiring another public cascade declaration.line 147
LeanInfoTheory.Examples.StochasticChannels.mutualInfo_cascade_contractsTheoremLeanInfoTheory.Examples.StochasticChannelsMutual information contracts along the same two stochastic stages.line 160
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.fairBitDefinitionLeanInfoTheory.Examples.SufficientStatisticsA fair nuisance bit.line 41
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.noiseChannelDefinitionLeanInfoTheory.Examples.SufficientStatisticsA channel producing an independent fair nuisance bit.line 44
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.observationLawDefinitionLeanInfoTheory.Examples.SufficientStatisticsAttach an independent fair nuisance bit to a binary signal law.line 47
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.statisticDefinitionLeanInfoTheory.Examples.SufficientStatisticsKeep the signal coordinate and discard the nuisance coordinate.line 51
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.recoveryDefinitionLeanInfoTheory.Examples.SufficientStatisticsRestore a discarded nuisance bit independently of the model parameter.line 54
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.modelDefinitionLeanInfoTheory.Examples.SufficientStatisticsThe midpoint model fixes the signal bit to the parameter.line 93
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.statistic_not_injectiveTheoremLeanInfoTheory.Examples.SufficientStatisticsThe first-coordinate statistic is not globally injective.line 97
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.statistic_collides_on_supportTheoremLeanInfoTheory.Examples.SufficientStatisticsFor each parameter, two supported observations collide under the statistic.line 104
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.statistic_isSufficientTheoremLeanInfoTheory.Examples.SufficientStatisticsDiscarding the nuisance bit is sufficient for the whole model family.line 113
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.fairPriorDefinitionLeanInfoTheory.Examples.SufficientStatisticsA full-support prior used for the fixed-prior view.line 119
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.fairPrior_supportTheoremLeanInfoTheory.Examples.SufficientStatisticsThe fair prior reaches both parameter values.line 122
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.experimentLawDefinitionLeanInfoTheory.Examples.SufficientStatisticsThe generated parameter-observation law under the fair prior.line 127
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.statistic_isSufficient_fixedPriorTheoremLeanInfoTheory.Examples.SufficientStatisticsFamily sufficiency gives fixed-prior sufficiency under the fair prior.line 131
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.mutualInfo_preserved_fixedPriorTheoremLeanInfoTheory.Examples.SufficientStatisticsThe fixed-prior statistic preserves parameter-observation mutual information.line 139
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.exists_exactRecovery_fixedPriorTheoremLeanInfoTheory.Examples.SufficientStatisticsFixed-prior sufficiency supplies an exact complete-law recovery channel.line 149
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.statistic_isSufficient_forall_priorTheoremLeanInfoTheory.Examples.SufficientStatisticsThe same statistic is sufficient under every parameter prior.line 161
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.exists_fisherNeymanFactorizationTheoremLeanInfoTheory.Examples.SufficientStatisticsThe sufficient statistic satisfies the finite Fisher-Neyman factorization.line 170
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.klDiv_preservedTheoremLeanInfoTheory.Examples.SufficientStatisticsThe statistic preserves KL divergence between every pair of model laws.line 180
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.biasedSignalDefinitionLeanInfoTheory.Examples.SufficientStatisticsA full-support nonuniform signal law.line 190
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.overlapSignalModelDefinitionLeanInfoTheory.Examples.SufficientStatisticsTwo overlapping signal laws for the guarded binary KL characterization.line 204
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.overlapModelDefinitionLeanInfoTheory.Examples.SufficientStatisticsAttach the same nuisance bit to each overlapping signal law.line 209
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.overlap_support_subsetTheoremLeanInfoTheory.Examples.SufficientStatisticsThe overlapping model has the support inclusion required by the KL converse.line 213
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.overlap_statistic_isSufficientTheoremLeanInfoTheory.Examples.SufficientStatisticsThe first-coordinate statistic is sufficient for the overlapping model.line 227
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.overlap_channel_iff_klDiv_eqTheoremLeanInfoTheory.Examples.SufficientStatisticsThe channel-facing binary KL equality characterizes this sufficient model.line 234
LeanInfoTheory.Examples.SufficientStatistics.Ancillary.overlap_statistic_iff_klDiv_eqTheoremLeanInfoTheory.Examples.SufficientStatisticsThe statistic-facing binary KL equality gives the same characterization.line 245
LeanInfoTheory.Examples.SufficientStatistics.Constant.modelDefinitionLeanInfoTheory.Examples.SufficientStatisticsTwo point-mass model laws that must remain distinguishable.line 260
LeanInfoTheory.Examples.SufficientStatistics.Constant.statisticDefinitionLeanInfoTheory.Examples.SufficientStatisticsA statistic that discards the observation completely.line 263
LeanInfoTheory.Examples.SufficientStatistics.Constant.statistic_not_sufficientTheoremLeanInfoTheory.Examples.SufficientStatisticsThe constant statistic is not sufficient for the separated model.line 266
LeanInfoTheory.Examples.SufficientStatistics.MarginalOnly.lawDefinitionLeanInfoTheory.Examples.SufficientStatisticsA fair law for the marginal-only recovery counterexample.line 285
LeanInfoTheory.Examples.SufficientStatistics.MarginalOnly.resetRecoveryDefinitionLeanInfoTheory.Examples.SufficientStatisticsA recovery channel that forgets its input and resamples the fair law.line 288
LeanInfoTheory.Examples.SufficientStatistics.MarginalOnly.recovers_marginalTheoremLeanInfoTheory.Examples.SufficientStatisticsThe reset channel recovers the input marginal after the identity statistic.line 291
LeanInfoTheory.Examples.SufficientStatistics.MarginalOnly.does_not_recover_fullJointTheoremLeanInfoTheory.Examples.SufficientStatisticsMarginal recovery does not reconstruct the identity input-output coupling.line 297
LeanInfoTheory.Examples.SupportSensitive.ThreePointInductiveLeanInfoTheory.Examples.SupportSensitiveA three-point ambient alphabet with one point omitted from the example law.line 34
LeanInfoTheory.Examples.SupportSensitive.ThreePoint.instFintypeInstanceLeanInfoTheory.Examples.SupportSensitiveNo doc comment found.line 40
LeanInfoTheory.Examples.SupportSensitive.twoPointSupportDefinitionLeanInfoTheory.Examples.SupportSensitiveThe two atoms carrying mass in `twoPointLaw`.line 48
LeanInfoTheory.Examples.SupportSensitive.twoPointSupport_nonemptyTheoremLeanInfoTheory.Examples.SupportSensitiveThe support used by `twoPointLaw` is nonempty.line 51
LeanInfoTheory.Examples.SupportSensitive.twoPointLawDefinitionLeanInfoTheory.Examples.SupportSensitiveThe uniform law on two points of a three-point ambient alphabet.line 55
LeanInfoTheory.Examples.SupportSensitive.twoPointLaw_supportTheoremLeanInfoTheory.Examples.SupportSensitiveThe third ambient point is genuinely outside the support of `twoPointLaw`.line 60
LeanInfoTheory.Examples.SupportSensitive.supportBound_is_strictly_sharperTheoremLeanInfoTheory.Examples.SupportSensitiveFor `twoPointLaw`, the support-cardinality entropy bound is strictly sharper than the alphabet-cardinality bound.line 68
LeanInfoTheory.Examples.SupportSensitive.supportEncodingDefinitionLeanInfoTheory.Examples.SupportSensitiveA map that separates the support but collides at an unsupported point.line 80
LeanInfoTheory.Examples.SupportSensitive.supportWitnessDefinitionLeanInfoTheory.Examples.SupportSensitiveA second map agreeing with `supportEncoding` only on `twoPointLaw.support`.line 86
LeanInfoTheory.Examples.SupportSensitive.supportEncoding_not_injectiveTheoremLeanInfoTheory.Examples.SupportSensitive`supportEncoding` is not globally injective.line 92
LeanInfoTheory.Examples.SupportSensitive.supportEncoding_injOn_supportTheoremLeanInfoTheory.Examples.SupportSensitive`supportEncoding` is injective where `twoPointLaw` carries mass.line 100
LeanInfoTheory.Examples.SupportSensitive.supportEncoding_preserves_entropyTheoremLeanInfoTheory.Examples.SupportSensitiveSupport-restricted injectivity is enough to preserve entropy.line 107
LeanInfoTheory.Examples.SupportSensitive.functionalDependence_on_supportTheoremLeanInfoTheory.Examples.SupportSensitiveThe first variable is a function of the second on the source support.line 115
LeanInfoTheory.Examples.SupportSensitive.functionalDependence_not_globalTheoremLeanInfoTheory.Examples.SupportSensitiveThe same functional relation fails at the unsupported ambient point.line 126
LeanInfoTheory.Examples.SupportSensitive.fiberLawDefinitionLeanInfoTheory.Examples.SupportSensitiveA pure joint law with one positive and one null conditioning fiber.line 131
LeanInfoTheory.Examples.SupportSensitive.nullFiber_zeroTheoremLeanInfoTheory.Examples.SupportSensitiveA null conditioning fiber contributes numeric zero by convention.line 134
LeanInfoTheory.Examples.SupportSensitive.positiveFiber_ne_zeroTheoremLeanInfoTheory.Examples.SupportSensitiveThe other conditioning fiber has positive mass.line 144
LeanInfoTheory.Examples.SupportSensitive.positiveFiber_zero_iff_pureTheoremLeanInfoTheory.Examples.SupportSensitiveOn the positive fiber, zero entropy is equivalent to a pure conditional PMF.line 148
LeanInfoTheory.Examples.SupportSensitive.positiveFiber_is_pureTheoremLeanInfoTheory.Examples.SupportSensitiveThe positive conditional fiber in `fiberLaw` is pure at `false`.line 155
LeanInfoTheory.Examples.SupportSensitive.positiveFiber_zeroTheoremLeanInfoTheory.Examples.SupportSensitiveThe positive fiber therefore has zero entropy for the substantive pure-law reason.line 166
LeanInfoTheory.Examples.SupportSensitive.recoveryLawDefinitionLeanInfoTheory.Examples.SupportSensitiveA full-support binary source for the side-information recovery example.line 170
LeanInfoTheory.Examples.SupportSensitive.recoveryXDefinitionLeanInfoTheory.Examples.SupportSensitiveThe source variable whose second coordinate carries the random bit.line 173
LeanInfoTheory.Examples.SupportSensitive.recoverySideInfoDefinitionLeanInfoTheory.Examples.SupportSensitiveSide information revealing the random bit.line 176
LeanInfoTheory.Examples.SupportSensitive.forgetSecondDefinitionLeanInfoTheory.Examples.SupportSensitiveProcessing that discards the random second coordinate.line 179
LeanInfoTheory.Examples.SupportSensitive.recoverWithSideInfoDefinitionLeanInfoTheory.Examples.SupportSensitiveA decoder that reconstructs `recoveryX` using the side information.line 182
LeanInfoTheory.Examples.SupportSensitive.forgetSecond_loses_entropyTheoremLeanInfoTheory.Examples.SupportSensitiveWithout side information, `forgetSecond` does not preserve entropy.line 186
LeanInfoTheory.Examples.SupportSensitive.sideInfo_preserves_condEntropyTheoremLeanInfoTheory.Examples.SupportSensitiveSide information restores the exact conditional-entropy equality contract.line 205
PMF.toReal_nonnegTheoremLeanInfoTheory.Probability.FiniteEach atom of a `PMF` has nonnegative real mass.line 34
PMF.toReal_le_oneTheoremLeanInfoTheory.Probability.FiniteEach atom of a `PMF` has real mass at most one.line 38
PMF.sum_toRealTheoremLeanInfoTheory.Probability.FiniteOn a finite type, the real masses of a `PMF` sum to one.line 42
PMF.bind_toReal_applyTheoremLeanInfoTheory.Probability.FiniteOn a finite selector type, the real mass of a bind is the corresponding finite weighted sum of real masses.line 64
PMF.supportFinsetDefinitionLeanInfoTheory.Probability.FiniteThe finite set of atoms to which a finite PMF assigns nonzero mass. Its coercion to a set is `p.support`; this finset view is intended for finite sums and support-cardinality arguments.line 81
PMF.mem_supportFinsetTheoremLeanInfoTheory.Probability.FiniteMembership in `p.supportFinset` is membership in the set-valued PMF support.line 86
PMF.coe_supportFinsetTheoremLeanInfoTheory.Probability.FiniteThe finite support finset coerces to the set-valued PMF support.line 92
PMF.supportFinset_cardTheoremLeanInfoTheory.Probability.FiniteThe finite support finset has the set-theoretic support cardinality.line 98
PMF.supportFinset_nonemptyTheoremLeanInfoTheory.Probability.FiniteThe finite support finset of a PMF is nonempty.line 103
PMF.eq_pure_iff_support_eq_singletonTheoremLeanInfoTheory.Probability.FiniteA PMF is pure at `a` exactly when its support is the singleton `{a}`.line 109
PMF.map_apply_of_injectiveTheoremLeanInfoTheory.Probability.FiniteIf `f` is injective, pushing a PMF forward along `f` preserves the mass of each source atom at its image.line 129
PMF.map_apply_eq_zero_of_notMem_rangeTheoremLeanInfoTheory.Probability.FiniteIf a target atom is outside the range of a map, then the pushed-forward PMF assigns zero mass to that atom.line 155
PMF.map_apply_equivTheoremLeanInfoTheory.Probability.FinitePushing a PMF forward along an equivalence preserves the mass of each atom at the renamed atom.line 181
PMF.deterministicChannelDefinitionLeanInfoTheory.Probability.FiniteChannelThe deterministic channel induced by a function.line 48
PMF.channelCompDefinitionLeanInfoTheory.Probability.FiniteChannelComposition of two PMF-valued channels in sampling order: first sample through `W`, then sample through `V`.line 56
PMF.channelJointDefinitionLeanInfoTheory.Probability.FiniteChannelThe joint law of an input distributed as `p` and an output sampled from `W`.line 63
PMF.channelExtensionDefinitionLeanInfoTheory.Probability.FiniteChannelExtend a joint law of `(A,B)` by sampling `C` from a channel depending only on `B`. The result uses Lean's right-associated triple type `(A, B, C)`.line 71
PMF.deterministicChannel_applyTheoremLeanInfoTheory.Probability.FiniteChannelA deterministic channel returns the pure law at the function value.line 80
PMF.channelComp_applyTheoremLeanInfoTheory.Probability.FiniteChannelPointwise mass formula for channel composition.line 86
PMF.channelJoint_applyTheoremLeanInfoTheory.Probability.FiniteChannelThe induced joint mass factors as input mass times channel mass.line 93
PMF.channelExtension_applyTheoremLeanInfoTheory.Probability.FiniteChannelThe extended triple mass factors as pair mass times channel mass.line 109
PMF.channelJoint_map_fstTheoremLeanInfoTheory.Probability.FiniteChannelThe first projection of an induced joint law is its input law.line 129
PMF.channelJoint_map_sndTheoremLeanInfoTheory.Probability.FiniteChannelThe second projection of an induced joint law is the channel output law.line 150
PMF.channelExtension_map_inputTheoremLeanInfoTheory.Probability.FiniteChannelProjecting an extension to its original input pair recovers that pair law.line 170
PMF.channelExtension_map_outputPairTheoremLeanInfoTheory.Probability.FiniteChannelProjecting an extension to the channel input-output pair gives the induced joint law of the original second marginal and the extending channel.line 201
PMF.channelExtension_map_outputTheoremLeanInfoTheory.Probability.FiniteChannelProjecting an extension to its new output gives the corresponding output law.line 227
PMF.channelExtension_map_endpointsTheoremLeanInfoTheory.Probability.FiniteChannelFor a two-stage channel, projecting the generated triple to its endpoints gives the joint law induced by the composite channel.line 254
PMF.bind_channelCompTheoremLeanInfoTheory.Probability.FiniteChannelSending an input law through a composite channel is iterated `PMF.bind`.line 283
PMF.channelComp_pure_leftTheoremLeanInfoTheory.Probability.FiniteChannelThe pure channel is a left identity for channel composition.line 291
PMF.channelComp_pure_rightTheoremLeanInfoTheory.Probability.FiniteChannelThe pure channel is a right identity for channel composition.line 299
PMF.channelComp_assocTheoremLeanInfoTheory.Probability.FiniteChannelChannel composition is associative.line 306
PMF.bind_deterministicChannelTheoremLeanInfoTheory.Probability.FiniteChannelSending a law through a deterministic channel is `PMF.map`.line 317
PMF.channelComp_deterministic_leftTheoremLeanInfoTheory.Probability.FiniteChannelA deterministic first stage evaluates the following channel at its image.line 324
PMF.channelComp_deterministic_rightTheoremLeanInfoTheory.Probability.FiniteChannelA deterministic second stage maps each output law.line 333
PMF.channelJoint_deterministicChannelTheoremLeanInfoTheory.Probability.FiniteChannelThe joint law of a deterministic channel is the graph pushforward.line 341
PMF.channelExtension_deterministicChannelTheoremLeanInfoTheory.Probability.FiniteChannelExtending a pair law through a deterministic channel is its graph pushforward.line 349
PMF.mem_support_channelComp_iffTheoremLeanInfoTheory.Probability.FiniteChannelAn output lies in a composite channel's support through a supported intermediate atom.line 362
PMF.mem_support_channelJoint_iffTheoremLeanInfoTheory.Probability.FiniteChannelA pair is supported by the induced joint law exactly when both stages support it.line 371
PMF.channelJoint_eq_iff_eq_on_supportTheoremLeanInfoTheory.Probability.FiniteChannelTwo channels induce the same joint law from an input PMF exactly when they agree on every supported input atom. Their values away from the input support are irrelevant.line 382
PMF.mem_support_channelExtension_iffTheoremLeanInfoTheory.Probability.FiniteChannelA triple is supported by an extension exactly when its pair and new output are supported.line 411
PMF.binaryMixtureDefinitionLeanInfoTheory.Probability.FiniteMixtureThe binary mixture with weight `t` on `p` and weight `1 - t` on `q`. Equivalently, a Bernoulli selector chooses `p` on `true` and `q` on `false`.line 35
PMF.binaryMixture_applyTheoremLeanInfoTheory.Probability.FiniteMixturePointwise mass formula for a binary PMF mixture.line 43
PMF.binaryMixture_zeroTheoremLeanInfoTheory.Probability.FiniteMixtureA binary mixture of weight zero is its second component.line 52
PMF.binaryMixture_oneTheoremLeanInfoTheory.Probability.FiniteMixtureA binary mixture of weight one is its first component.line 62
LeanInfoTheory.Shannon.entropy_boolTheoremLeanInfoTheory.Shannon.BinaryEntropyThe entropy of a Boolean PMF is the binary entropy of its `true` mass. The identity includes the endpoint laws without separate positivity assumptions.line 36
LeanInfoTheory.Shannon.entropyDefinitionLeanInfoTheory.Shannon.EntropyShannon entropy, in nats, of a finite probability mass function.line 36
LeanInfoTheory.Shannon.entropy_eq_sumTheoremLeanInfoTheory.Shannon.EntropyThe defining finite-sum formula for Shannon entropy.line 40
LeanInfoTheory.Shannon.entropy_nonnegTheoremLeanInfoTheory.Shannon.EntropyShannon entropy is nonnegative for finite PMFs.line 45
LeanInfoTheory.Shannon.entropy_map_equivTheoremLeanInfoTheory.Shannon.EntropyEntropy is invariant under relabeling the alphabet by an equivalence. This is one of the basic sanity checks for finite entropy: only the masses matter, not the names of the atoms.line 61
LeanInfoTheory.Shannon.entropy_map_injectiveTheoremLeanInfoTheory.Shannon.EntropyEntropy is invariant under injective relabeling into a larger finite alphabet. Atoms outside the image of the relabeling have zero pushed-forward mass.line 76
LeanInfoTheory.Shannon.entropy_pureTheoremLeanInfoTheory.Shannon.EntropyA deterministic finite PMF has entropy zero.line 109
LeanInfoTheory.Shannon.entropy_eq_zero_iffTheoremLeanInfoTheory.Shannon.EntropyA finite PMF has entropy zero exactly when it is a pure law.line 137
LeanInfoTheory.Shannon.entropyOfDefinitionLeanInfoTheory.Shannon.EntropyEntropy of a finite-valued random variable under a discrete law.line 169
LeanInfoTheory.Shannon.entropyOf_eq_zero_iffTheoremLeanInfoTheory.Shannon.EntropyThe entropy of a finite-valued random variable is zero exactly when the variable is constant on the support of the source PMF.line 200
LeanInfoTheory.Shannon.entropyOf_idTheoremLeanInfoTheory.Shannon.EntropyEntropy of the identity random variable is the entropy of the original law.line 210
LeanInfoTheory.Shannon.entropyOf_comp_equivTheoremLeanInfoTheory.Shannon.EntropyRelabeling a finite-valued random variable by an equivalence preserves its entropy.line 215
LeanInfoTheory.Shannon.entropyOf_comp_injectiveTheoremLeanInfoTheory.Shannon.EntropyApplying an injective relabeling to a finite-valued random variable preserves its entropy.line 223
LeanInfoTheory.Shannon.jointEntropyDefinitionLeanInfoTheory.Shannon.EntropyJoint entropy is entropy of a joint finite distribution.line 233
LeanInfoTheory.Shannon.entropy_map_swapTheoremLeanInfoTheory.Shannon.EntropySwapping the two coordinates of a joint law preserves entropy.line 238
LeanInfoTheory.Shannon.entropy_map_prodAssocTheoremLeanInfoTheory.Shannon.EntropyReassociating a left-associated triple alphabet preserves entropy. This records that `H((A, B), C)` and `H(A, B, C)` are the same entropy after the canonical product reassociation equivalence.line 249
LeanInfoTheory.Shannon.entropy_map_prodAssoc_symmTheoremLeanInfoTheory.Shannon.EntropyReassociating a right-associated triple alphabet back to the left preserves entropy.line 256
LeanInfoTheory.Shannon.jointEntropy_map_swapTheoremLeanInfoTheory.Shannon.EntropySwapping the two coordinates of a joint law preserves joint entropy.line 264
LeanInfoTheory.Shannon.jointEntropyOfDefinitionLeanInfoTheory.Shannon.EntropyJoint entropy of two finite-valued random variables under a discrete law.line 270
LeanInfoTheory.Shannon.jointEntropyOf_swapTheoremLeanInfoTheory.Shannon.EntropyJoint entropy of two random variables is invariant under swapping their order.line 276
LeanInfoTheory.Shannon.entropyOf_prodAssocTheoremLeanInfoTheory.Shannon.EntropyEntropy of three finite-valued random variables is invariant under reassociating the product alphabet.line 290
LeanInfoTheory.Shannon.entropy_le_log_cardTheoremLeanInfoTheory.Shannon.EntropyBoundsFinite Shannon entropy is bounded above by the logarithm of the alphabet size. The proof is Jensen's inequality for the concave function `Real.negMulLog`, applied with uniform weights over the finite alphabet.line 39
LeanInfoTheory.Shannon.entropy_le_log_support_ncardTheoremLeanInfoTheory.Shannon.EntropyBoundsFinite Shannon entropy is bounded by the logarithm of the number of atoms with nonzero mass. Unlike `entropy_le_log_card`, this theorem counts only the PMF support and does not require a separate nonempty-alphabet instance.line 198
LeanInfoTheory.Shannon.entropyOf_le_log_support_ncardTheoremLeanInfoTheory.Shannon.EntropyBoundsThe entropy of a finite-valued random variable is bounded by the logarithm of the support size of its pushforward law.line 213
LeanInfoTheory.Shannon.entropy_uniformOfFintypeTheoremLeanInfoTheory.Shannon.EntropyBoundsThe uniform distribution reaches the finite entropy upper bound. Mathematically, this is the equality case `H(U_alpha) = log |alpha|` for the uniform law on a nonempty finite alphabet.line 225
LeanInfoTheory.Shannon.entropy_eq_log_card_iff_eq_uniformOfFintypeTheoremLeanInfoTheory.Shannon.EntropyBoundsFinite Shannon entropy reaches the alphabet-cardinality bound exactly at the uniform distribution.line 265
LeanInfoTheory.Shannon.entropy_eq_log_support_ncard_iff_eq_uniformOnSupportTheoremLeanInfoTheory.Shannon.EntropyBoundsFinite Shannon entropy reaches its support-cardinality bound exactly when the distribution is uniform on its support.line 391
LeanInfoTheory.Shannon.entropyOf_eq_log_card_iff_map_eq_uniformOfFintypeTheoremLeanInfoTheory.Shannon.EntropyBoundsA finite-valued random variable reaches the alphabet-cardinality entropy bound exactly when its law is uniform on the alphabet.line 437
LeanInfoTheory.Shannon.entropyOf_eq_log_support_ncard_iff_map_eq_uniformOnSupportTheoremLeanInfoTheory.Shannon.EntropyBoundsA finite-valued random variable reaches its law-support entropy bound exactly when that law is uniform on its support.line 449
LeanInfoTheory.Shannon.sum_mul_entropy_le_entropy_bindTheoremLeanInfoTheory.Shannon.EntropyConcavityEntropy is concave under a finite PMF-valued selector. This is the general finite-selector form of the textbook binary entropy concavity inequality.line 39
LeanInfoTheory.Shannon.binaryMixture_entropy_concaveTheoremLeanInfoTheory.Shannon.EntropyConcavityEntropy is concave under a binary PMF mixture.line 70
LeanInfoTheory.Shannon.binaryMixture_entropy_eq_iffTheoremLeanInfoTheory.Shannon.EntropyConcavityFor an interior binary weight, equality in entropy concavity holds exactly when the two component PMFs are equal.line 98
LeanInfoTheory.Shannon.decodingErrorIndicatorDefinitionLeanInfoTheory.Shannon.FanoThe Boolean error indicator for a deterministic decoder. It is `true` exactly when decoding the observation `y` does not recover the source symbol `x`. Decidable equality is chosen internally.line 54
LeanInfoTheory.Shannon.decodingErrorIndicator_eq_true_iffTheoremLeanInfoTheory.Shannon.FanoThe decoding-error indicator is `true` exactly on decoder failure.line 62
LeanInfoTheory.Shannon.decodingErrorIndicator_eq_false_iffTheoremLeanInfoTheory.Shannon.FanoThe decoding-error indicator is `false` exactly on decoder success.line 71
LeanInfoTheory.Shannon.decodingErrorProbabilityDefinitionLeanInfoTheory.Shannon.FanoThe probability that a deterministic decoder fails under a joint law. The PMF is a joint law of a source symbol and an observation, in that order.line 83
LeanInfoTheory.Shannon.decodingErrorProbabilityOfDefinitionLeanInfoTheory.Shannon.FanoThe probability that a deterministic decoder fails for random variables. Here `X` is the source variable, `Y` is the observation, and `decoder` tries to recover `X` from `Y`.line 94
LeanInfoTheory.Shannon.decodingErrorProbability_eq_sumTheoremLeanInfoTheory.Shannon.FanoThe decoding-error probability is the total mass of the joint atoms on which the decoder fails. This is the main finite-sum elimination theorem for decoding error.line 107
LeanInfoTheory.Shannon.decodingErrorProbability_nonnegTheoremLeanInfoTheory.Shannon.FanoA decoding-error probability is nonnegative.line 126
LeanInfoTheory.Shannon.decodingErrorProbability_le_oneTheoremLeanInfoTheory.Shannon.FanoA decoding-error probability is at most one.line 134
LeanInfoTheory.Shannon.decodingErrorProbabilityOf_nonnegTheoremLeanInfoTheory.Shannon.FanoThe decoding-error probability of random variables is nonnegative.line 142
LeanInfoTheory.Shannon.decodingErrorProbabilityOf_le_oneTheoremLeanInfoTheory.Shannon.FanoThe decoding-error probability of random variables is at most one.line 151
LeanInfoTheory.Shannon.entropy_decodingErrorIndicatorTheoremLeanInfoTheory.Shannon.FanoThe entropy, in nats, of the Boolean decoding-error indicator is the binary entropy of the decoding-error probability. The indicator is `true` exactly on decoder failure.line 165
LeanInfoTheory.Shannon.entropyOf_decodingErrorIndicatorTheoremLeanInfoTheory.Shannon.FanoThe entropy, in nats, of a random variable's Boolean decoding-error indicator is the binary entropy of its decoding-error probability. Here `X` is the source variable, `Y` is the observation, and `decoder` attempts to recover `X` from `Y`.line 180
LeanInfoTheory.Shannon.condEntropy_fanoTheoremLeanInfoTheory.Shannon.FanoFano's inequality for a finite joint law and a deterministic decoder, in nats. Here the first coordinate is the source, the second coordinate is the observation, and `decoder` attempts to recover the source from the observation. The decoding-error indicator is `true` exactly when decoding fails. No lower bound on the source-alphabet cardinality is required; in particular, the singleton case is included.line 552
LeanInfoTheory.Shannon.condEntropy_fano_qaryTheoremLeanInfoTheory.Shannon.FanoFano's inequality for a finite joint law, expressed with mathlib's `Real.qaryEntropy`, in nats. The error convention and decoder direction are the same as in `condEntropy_fano`. This form is valid without a lower bound on the source alphabet cardinality.line 609
LeanInfoTheory.Shannon.condEntropyOf_fanoTheoremLeanInfoTheory.Shannon.FanoThe random-variable form of `condEntropy_fano`, in nats. Here `X` is the finite source variable, `Y` is the finite observation, and `decoder` attempts to recover `X` from `Y`. The error indicator is `true` exactly when decoding fails. The source sample space itself need not be finite.line 636
LeanInfoTheory.Shannon.condEntropyOf_fano_qaryTheoremLeanInfoTheory.Shannon.FanoThe random-variable form of `condEntropy_fano_qary`, in nats. The decoder direction and error convention are those of `condEntropyOf_fano`. Only the value alphabets of `X` and `Y` must be finite.line 655
LeanInfoTheory.Shannon.condEntropy_fano_weakTheoremLeanInfoTheory.Shannon.FanoThe conventional weaker form of Fano's inequality for a finite joint law: `H(X | Y) <= log 2 + Pe * log |alpha|`. All logarithms are natural, so `log 2` is the one-bit textbook constant expressed in nats. No lower bound on the source-alphabet cardinality is required.line 677
LeanInfoTheory.Shannon.condEntropyOf_fano_weakTheoremLeanInfoTheory.Shannon.FanoThe random-variable form of `condEntropy_fano_weak`, in nats. Only the finite value alphabets of `X` and `Y` are required; the source sample space may be arbitrary.line 723
LeanInfoTheory.Shannon.decodingErrorProbability_fano_lower_boundTheoremLeanInfoTheory.Shannon.FanoFano's lower bound on the decoding-error probability for a finite joint law: `(H(X | Y) - log 2) / log |alpha| <= Pe`. The hypothesis `2 <= |alpha|` is needed here, unlike in the entropy forms of Fano's inequality, because it makes the logarithmic denominator strictly positive.line 745
LeanInfoTheory.Shannon.decodingErrorProbabilityOf_fano_lower_boundTheoremLeanInfoTheory.Shannon.FanoThe random-variable form of `decodingErrorProbability_fano_lower_bound`. Only the finite value alphabets of `X` and `Y` are required. The source sample space may be arbitrary.line 769
LeanInfoTheory.Shannon.mutualInfo_fano_lower_bound_of_uniform_sourceTheoremLeanInfoTheory.Shannon.FanoFano's mutual-information lower bound for a uniform finite source, in nats: `log |alpha| - log 2 - Pe * log |alpha| <= I(X;Y)`. The first marginal of the supplied joint law is the source law. No cardinality lower bound is needed because this theorem does not divide by `log |alpha|`.line 806
LeanInfoTheory.Shannon.mutualInfoOf_fano_lower_bound_of_uniform_sourceTheoremLeanInfoTheory.Shannon.FanoThe random-variable form of `mutualInfo_fano_lower_bound_of_uniform_source`. Uniformity is stated through the existing pushforward-law equality `p.map X = PMF.uniformOfFintype alpha`.line 827
LeanInfoTheory.Shannon.decodingErrorProbability_fano_lower_bound_of_uniform_sourceTheoremLeanInfoTheory.Shannon.FanoThe standard uniform-source Fano lower bound on decoding error, in nats: `1 - (I(X;Y) + log 2) / log |alpha| <= Pe`. The hypothesis `2 <= |alpha|` makes the logarithmic denominator strictly positive. Uniformity is expressed by equality of the first marginal with the existing finite uniform PMF.line 856
LeanInfoTheory.Shannon.decodingErrorProbabilityOf_fano_lower_bound_of_uniform_sourceTheoremLeanInfoTheory.Shannon.FanoThe random-variable form of `decodingErrorProbability_fano_lower_bound_of_uniform_source`. The sample space may be arbitrary; only the source and observation value alphabets are finite.line 893
LeanInfoTheory.Shannon.FamilyOutcomeDefinitionLeanInfoTheory.Shannon.FiniteFamilyThe outcome type of the variables selected by the finite atom `s`. No finiteness assumption is needed to form this type. Pointwise finiteness of the selected alphabets is required only when taking entropy.line 42
LeanInfoTheory.Shannon.familyLawOfDefinitionLeanInfoTheory.Shannon.FiniteFamilyThe joint law of an indexed family of random variables under a source PMF. The source type, variable-name type, and full dependent outcome type may all be infinite.line 51
LeanInfoTheory.Shannon.familyMarginalDefinitionLeanInfoTheory.Shannon.FiniteFamilyThe joint marginal law of the variables selected by the finite atom `s`.line 57
LeanInfoTheory.Shannon.familyEntropyDefinitionLeanInfoTheory.Shannon.FiniteFamilyShannon entropy, in nats, of the variables selected by the finite atom `s`.line 65
LeanInfoTheory.Shannon.familyEntropyOfDefinitionLeanInfoTheory.Shannon.FiniteFamilyShannon entropy, in nats, of a finite subfamily of random variables under a source PMF.line 74
LeanInfoTheory.Shannon.familyCondEntropyDefinitionLeanInfoTheory.Shannon.FiniteFamilyConditional entropy `H(A | B)` of two finite subfamilies. The atoms may overlap.line 87
LeanInfoTheory.Shannon.familyMutualInfoDefinitionLeanInfoTheory.Shannon.FiniteFamilyMutual information `I(A; B)` of two finite subfamilies. The atoms may overlap.line 97
LeanInfoTheory.Shannon.familyCondMutualInfoDefinitionLeanInfoTheory.Shannon.FiniteFamilyConditional mutual information `I(A; B | C)` of three finite subfamilies. The three-way union is normalized as `(A ∪ B) ∪ C`.line 107
LeanInfoTheory.Shannon.familyCondEntropyOfDefinitionLeanInfoTheory.Shannon.FiniteFamilyConditional entropy of two finite subfamilies under a source PMF.line 114
LeanInfoTheory.Shannon.familyMutualInfoOfDefinitionLeanInfoTheory.Shannon.FiniteFamilyMutual information of two finite subfamilies under a source PMF.line 122
LeanInfoTheory.Shannon.familyCondMutualInfoOfDefinitionLeanInfoTheory.Shannon.FiniteFamilyConditional mutual information of three finite subfamilies under a source PMF.line 130
LeanInfoTheory.Shannon.familyMarginal_restrictTheoremLeanInfoTheory.Shannon.FiniteFamilyRestricting a finite family marginal to a smaller atom gives the marginal on that smaller atom.line 143
LeanInfoTheory.Shannon.familyMarginal_familyLawOfTheoremLeanInfoTheory.Shannon.FiniteFamilyThe finite marginal of a source-indexed family is the joint law of its selected coordinates.line 154
LeanInfoTheory.Shannon.familyEntropy_eq_entropyOfTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily entropy is ordinary random-variable entropy of finite restriction.line 167
LeanInfoTheory.Shannon.familyEntropyOf_eq_entropyOfTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family entropy is ordinary entropy of the selected coordinates under the source law.line 178
LeanInfoTheory.Shannon.familyEntropyOf_congrTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily entropy on `s` depends only on the source variables selected by `s`.line 190
LeanInfoTheory.Shannon.familyEntropy_emptyTheoremLeanInfoTheory.Shannon.FiniteFamilyThe entropy of the empty family is zero.line 205
LeanInfoTheory.Shannon.familyEntropyOf_emptyTheoremLeanInfoTheory.Shannon.FiniteFamilyThe entropy of the empty source-indexed family is zero.line 223
LeanInfoTheory.Shannon.familyEntropy_singletonTheoremLeanInfoTheory.Shannon.FiniteFamilyThe entropy of a singleton family is the entropy of that coordinate.line 249
LeanInfoTheory.Shannon.familyEntropyOf_singletonTheoremLeanInfoTheory.Shannon.FiniteFamilyThe entropy of a singleton source-indexed family is the entropy of that source variable.line 264
LeanInfoTheory.Shannon.familyEntropy_nonnegTheoremLeanInfoTheory.Shannon.FiniteFamilyEntropy of every finite subfamily is nonnegative.line 273
LeanInfoTheory.Shannon.familyEntropyOf_nonnegTheoremLeanInfoTheory.Shannon.FiniteFamilyEntropy of every finite source-indexed subfamily is nonnegative.line 281
LeanInfoTheory.Shannon.familyEntropy_unionTheoremLeanInfoTheory.Shannon.FiniteFamilyEntropy on a union is the joint entropy of the two restricted subfamilies. The atoms may overlap; no disjointness or support assumption is required.line 353
LeanInfoTheory.Shannon.familyEntropyOf_unionTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family entropy on a union is the joint entropy of the two selected subfamilies.line 379
LeanInfoTheory.Shannon.familyEntropy_tripleUnionTheoremLeanInfoTheory.Shannon.FiniteFamilyEntropy on a three-way union is entropy of the right-associated triple of restricted subfamilies. All three atoms may overlap.line 412
LeanInfoTheory.Shannon.familyEntropyOf_tripleUnionTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family entropy on a three-way union is entropy of the right-associated triple of selected subfamilies.line 442
LeanInfoTheory.Shannon.familyCondEntropy_eq_condEntropyOfTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily conditional entropy is ordinary conditional entropy of the two restriction-valued random variables.line 480
LeanInfoTheory.Shannon.familyCondEntropyOf_eq_condEntropyOfTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family conditional entropy is ordinary conditional entropy of the two selected subfamilies.line 493
LeanInfoTheory.Shannon.familyMutualInfo_eq_mutualInfoOfTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily mutual information is ordinary mutual information of the two restriction-valued random variables.line 522
LeanInfoTheory.Shannon.familyMutualInfoOf_eq_mutualInfoOfTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family mutual information is ordinary mutual information of the two selected subfamilies.line 536
LeanInfoTheory.Shannon.familyCondMutualInfo_eq_condMutualInfoOfTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily conditional mutual information is ordinary conditional mutual information of the three restriction-valued random variables.line 565
LeanInfoTheory.Shannon.familyCondMutualInfoOf_eq_condMutualInfoOfTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family conditional mutual information is ordinary conditional mutual information of the three selected subfamilies.line 580
LeanInfoTheory.Shannon.familyCondEntropy_singletonsTheoremLeanInfoTheory.Shannon.FiniteFamilySingleton atoms recover conditional entropy of ordinary coordinates.line 677
LeanInfoTheory.Shannon.familyCondEntropyOf_singletonsTheoremLeanInfoTheory.Shannon.FiniteFamilySingleton source-family atoms recover conditional entropy of the corresponding ordinary random variables.line 706
LeanInfoTheory.Shannon.familyMutualInfo_singletonsTheoremLeanInfoTheory.Shannon.FiniteFamilySingleton atoms recover mutual information of ordinary coordinates.line 717
LeanInfoTheory.Shannon.familyMutualInfoOf_singletonsTheoremLeanInfoTheory.Shannon.FiniteFamilySingleton source-family atoms recover mutual information of the corresponding ordinary random variables.line 751
LeanInfoTheory.Shannon.familyCondMutualInfo_singletonsTheoremLeanInfoTheory.Shannon.FiniteFamilySingleton atoms recover conditional mutual information of ordinary coordinates.line 765
LeanInfoTheory.Shannon.familyCondMutualInfoOf_singletonsTheoremLeanInfoTheory.Shannon.FiniteFamilySingleton source-family atoms recover conditional mutual information of the corresponding ordinary random variables.line 808
LeanInfoTheory.Shannon.familyMutualInfo_swapTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily mutual information is symmetric: `I(B;A) = I(A;B)`.line 821
LeanInfoTheory.Shannon.familyMutualInfoOf_swapTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family mutual information is symmetric.line 831
LeanInfoTheory.Shannon.familyCondMutualInfo_swapTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily conditional mutual information is symmetric in its first two atoms: `I(B;A|C) = I(A;B|C)`.line 844
LeanInfoTheory.Shannon.familyCondMutualInfoOf_swapTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family conditional mutual information is symmetric in its first two atoms.line 854
LeanInfoTheory.Shannon.familyCondEntropy_empty_rightTheoremLeanInfoTheory.Shannon.FiniteFamilyConditioning on the empty atom leaves family entropy unchanged.line 866
LeanInfoTheory.Shannon.familyCondEntropy_empty_leftTheoremLeanInfoTheory.Shannon.FiniteFamilyThe empty atom has zero conditional entropy.line 875
LeanInfoTheory.Shannon.familyMutualInfo_empty_rightTheoremLeanInfoTheory.Shannon.FiniteFamilyMutual information with the empty right atom is zero.line 884
LeanInfoTheory.Shannon.familyCondMutualInfo_empty_rightTheoremLeanInfoTheory.Shannon.FiniteFamilyConditional mutual information with the empty second atom is zero.line 893
LeanInfoTheory.Shannon.familyCondMutualInfo_empty_conditioningTheoremLeanInfoTheory.Shannon.FiniteFamilyEmpty conditioning reduces conditional mutual information to mutual information.line 904
LeanInfoTheory.Shannon.familyMutualInfo_selfTheoremLeanInfoTheory.Shannon.FiniteFamilyThe mutual information of an atom with itself is its entropy.line 916
LeanInfoTheory.Shannon.familyMutualInfo_eq_entropy_sub_condEntropyTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily mutual information as `I(A;B) = H(A) - H(A|B)`.line 926
LeanInfoTheory.Shannon.familyMutualInfoOf_eq_entropyOf_sub_condEntropyOfTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family mutual information as `I(A;B) = H(A) - H(A|B)`.line 936
LeanInfoTheory.Shannon.familyCondMutualInfo_eq_condEntropy_sub_condEntropyTheoremLeanInfoTheory.Shannon.FiniteFamilyFamily conditional mutual information as `I(A;B|C) = H(A|C) - H(A|B ∪ C)`.line 951
LeanInfoTheory.Shannon.familyCondMutualInfoOf_eq_condEntropyOf_sub_condEntropyOfTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family conditional mutual information as `I(A;B|C) = H(A|C) - H(A|B ∪ C)`.line 965
LeanInfoTheory.Shannon.familyEntropy_union_chain_rule_rightTheoremLeanInfoTheory.Shannon.FiniteFamilyRight-oriented entropy chain rule: `H(A ∪ B) = H(B) + H(A | B)`.line 980
LeanInfoTheory.Shannon.familyEntropy_union_chain_rule_leftTheoremLeanInfoTheory.Shannon.FiniteFamilyLeft-oriented entropy chain rule: `H(A ∪ B) = H(A) + H(B | A)`.line 990
LeanInfoTheory.Shannon.familyEntropyOf_union_chain_rule_rightTheoremLeanInfoTheory.Shannon.FiniteFamilyRight-oriented source-family entropy chain rule.line 1001
LeanInfoTheory.Shannon.familyEntropyOf_union_chain_rule_leftTheoremLeanInfoTheory.Shannon.FiniteFamilyLeft-oriented source-family entropy chain rule.line 1012
LeanInfoTheory.Shannon.familyMutualInfo_union_chain_ruleTheoremLeanInfoTheory.Shannon.FiniteFamilyMutual-information union chain rule: `I(A ∪ B; C) = I(A; C) + I(B; C | A)`.line 1026
LeanInfoTheory.Shannon.familyMutualInfoOf_union_chain_ruleTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family mutual-information union chain rule.line 1041
LeanInfoTheory.Shannon.familyCondMutualInfo_union_chain_ruleTheoremLeanInfoTheory.Shannon.FiniteFamilyConditional-mutual-information union chain rule: `I(A ∪ B; C | D) = I(A; C | D) + I(B; C | A ∪ D)`. The four atoms may overlap; no disjointness hypothesis is required.line 1058
LeanInfoTheory.Shannon.familyCondMutualInfoOf_union_chain_ruleTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family conditional-mutual-information union chain rule.line 1071
LeanInfoTheory.Shannon.familyEntropyChainDefinitionLeanInfoTheory.Shannon.FiniteFamilyThe ordered conditional-entropy sum `∑ k, H({l[k]} | {l[0], ..., l[k-1]})`.line 1095
LeanInfoTheory.Shannon.familyMutualInfoChainDefinitionLeanInfoTheory.Shannon.FiniteFamilyThe ordered conditional-mutual-information sum `∑ k, I({l[k]}; B | {l[0], ..., l[k-1]})`.line 1106
LeanInfoTheory.Shannon.familyEntropy_eq_entropyChainTheoremLeanInfoTheory.Shannon.FiniteFamilyEntropy chain rule for an arbitrary ordered list of variable names. Repeated names are allowed: once a name has appeared, its later conditional entropy contribution is zero.line 1183
LeanInfoTheory.Shannon.familyEntropyOf_eq_entropyChainTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family entropy chain rule for an arbitrary ordered list.line 1198
LeanInfoTheory.Shannon.familyEntropy_chain_rule_of_nodupTheoremLeanInfoTheory.Shannon.FiniteFamilyTextbook entropy chain rule for a list of distinct variable names. The `Nodup` assumption records the textbook indexing convention; the primary chain rule above is stronger and also handles repeated names.line 1213
LeanInfoTheory.Shannon.familyEntropyOf_chain_rule_of_nodupTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family textbook entropy chain rule for distinct variable names.line 1224
LeanInfoTheory.Shannon.familyMutualInfo_eq_mutualInfoChainTheoremLeanInfoTheory.Shannon.FiniteFamilyMutual-information chain rule for an arbitrary ordered list of variable names. Repeated names are allowed, and the atom `b` may overlap the list.line 1297
LeanInfoTheory.Shannon.familyMutualInfoOf_eq_mutualInfoChainTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family mutual-information chain rule for an arbitrary ordered list.line 1320
LeanInfoTheory.Shannon.familyMutualInfo_chain_rule_of_nodupTheoremLeanInfoTheory.Shannon.FiniteFamilyTextbook mutual-information chain rule for distinct variable names. The primary chain rule above is stronger and also handles repeated names.line 1335
LeanInfoTheory.Shannon.familyMutualInfoOf_chain_rule_of_nodupTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family textbook mutual-information chain rule for distinct variable names.line 1351
LeanInfoTheory.Shannon.familyCondMutualInfo_chain_ruleTheoremLeanInfoTheory.Shannon.FiniteFamilyConditional-mutual-information chain rule for an arbitrary ordered list of variable names: `I(l; B | C) = ∑ k, I({l[k]}; B | C ∪ {l[0], ..., l[k-1]})`. Repeated names are allowed, including names already present in the conditioning atom.line 1373
LeanInfoTheory.Shannon.familyCondMutualInfoOf_chain_ruleTheoremLeanInfoTheory.Shannon.FiniteFamilySource-family ordered conditional-mutual-information chain rule. As in the law-facing theorem, repeated names and names already in the conditioning atom are allowed.line 1420
LeanInfoTheory.Shannon.fstMarginalDefinitionLeanInfoTheory.Shannon.InfoMeasuresThe first marginal of a finite joint PMF.line 35
LeanInfoTheory.Shannon.sndMarginalDefinitionLeanInfoTheory.Shannon.InfoMeasuresThe second marginal of a finite joint PMF.line 39
LeanInfoTheory.Shannon.fstMarginal_mapTheoremLeanInfoTheory.Shannon.InfoMeasuresTaking the first marginal after pushing a PMF forward to a pair is the same as pushing forward by the first coordinate of that pair-valued map.line 47
LeanInfoTheory.Shannon.sndMarginal_mapTheoremLeanInfoTheory.Shannon.InfoMeasuresTaking the second marginal after pushing a PMF forward to a pair is the same as pushing forward by the second coordinate of that pair-valued map.line 58
LeanInfoTheory.Shannon.fstMarginal_map_pairTheoremLeanInfoTheory.Shannon.InfoMeasuresFor a joint law built from random variables `(X, Y)`, the first marginal is the law of `X`.line 66
LeanInfoTheory.Shannon.sndMarginal_map_pairTheoremLeanInfoTheory.Shannon.InfoMeasuresFor a joint law built from random variables `(X, Y)`, the second marginal is the law of `Y`.line 73
LeanInfoTheory.Shannon.fstMarginal_map_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSwapping the two coordinates turns the first marginal into the original second marginal.line 80
LeanInfoTheory.Shannon.sndMarginal_map_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSwapping the two coordinates turns the second marginal into the original first marginal.line 87
LeanInfoTheory.Shannon.fstMarginal_applyTheoremLeanInfoTheory.Shannon.InfoMeasuresThe mass of the first marginal is the sum of the joint masses over the second coordinate.line 93
LeanInfoTheory.Shannon.sndMarginal_applyTheoremLeanInfoTheory.Shannon.InfoMeasuresThe mass of the second marginal is the sum of the joint masses over the first coordinate.line 120
LeanInfoTheory.Shannon.fstSndMarginalDefinitionLeanInfoTheory.Shannon.InfoMeasuresThe marginal on the first and second coordinates of a finite triple PMF.line 147
LeanInfoTheory.Shannon.fstSndMarginal_mapTheoremLeanInfoTheory.Shannon.InfoMeasuresProjection formula for the first-second marginal of a pushed-forward triple law.line 156
LeanInfoTheory.Shannon.fstSndMarginal_map_tripleTheoremLeanInfoTheory.Shannon.InfoMeasuresFor a joint law built from `(X, Y, Z)`, the first-second marginal is the joint law of `(X, Y)`.line 169
LeanInfoTheory.Shannon.fstThirdMarginalDefinitionLeanInfoTheory.Shannon.InfoMeasuresThe marginal on the first and third coordinates of a finite triple PMF.line 177
LeanInfoTheory.Shannon.sndThirdMarginalDefinitionLeanInfoTheory.Shannon.InfoMeasuresThe marginal on the second and third coordinates of a finite triple PMF.line 182
LeanInfoTheory.Shannon.thirdMarginalDefinitionLeanInfoTheory.Shannon.InfoMeasuresThe marginal on the third coordinate of a finite triple PMF.line 187
LeanInfoTheory.Shannon.fstThirdMarginal_mapTheoremLeanInfoTheory.Shannon.InfoMeasuresProjection formula for the first-third marginal of a pushed-forward triple law. This is the triple analogue of `fstMarginal_map`.line 196
LeanInfoTheory.Shannon.sndThirdMarginal_mapTheoremLeanInfoTheory.Shannon.InfoMeasuresProjection formula for the second-third marginal of a pushed-forward triple law. The product `alpha × beta × gamma` is right-associated in Lean.line 209
LeanInfoTheory.Shannon.thirdMarginal_mapTheoremLeanInfoTheory.Shannon.InfoMeasuresProjection formula for the third-coordinate marginal of a pushed-forward triple law.line 218
LeanInfoTheory.Shannon.fstThirdMarginal_map_tripleTheoremLeanInfoTheory.Shannon.InfoMeasuresFor a joint law built from `(X, Y, Z)`, the first-third marginal is the joint law of `(X, Z)`.line 230
LeanInfoTheory.Shannon.sndThirdMarginal_map_tripleTheoremLeanInfoTheory.Shannon.InfoMeasuresFor a joint law built from `(X, Y, Z)`, the second-third marginal is the joint law of `(Y, Z)`.line 242
LeanInfoTheory.Shannon.thirdMarginal_map_tripleTheoremLeanInfoTheory.Shannon.InfoMeasuresFor a joint law built from `(X, Y, Z)`, the third marginal is the law of `Z`.line 251
LeanInfoTheory.Shannon.fstThirdMarginal_map_swap12TheoremLeanInfoTheory.Shannon.InfoMeasuresAfter swapping the first two coordinates of `(A, B, C)`, the first-third marginal is the original second-third marginal.line 262
LeanInfoTheory.Shannon.sndThirdMarginal_map_swap12TheoremLeanInfoTheory.Shannon.InfoMeasuresAfter swapping the first two coordinates of `(A, B, C)`, the second-third marginal is the original first-third marginal.line 273
LeanInfoTheory.Shannon.thirdMarginal_map_swap12TheoremLeanInfoTheory.Shannon.InfoMeasuresSwapping the first two coordinates leaves the third marginal unchanged.line 281
LeanInfoTheory.Shannon.fstThirdMarginal_applyTheoremLeanInfoTheory.Shannon.InfoMeasuresThe mass of the first-third marginal is the sum of the triple joint masses over the second coordinate.line 291
LeanInfoTheory.Shannon.sndThirdMarginal_applyTheoremLeanInfoTheory.Shannon.InfoMeasuresThe mass of the second-third marginal is the sum of the triple joint masses over the first coordinate.line 329
LeanInfoTheory.Shannon.thirdMarginal_applyTheoremLeanInfoTheory.Shannon.InfoMeasuresThe mass of the third marginal is the sum of the triple joint masses over the first two coordinates.line 367
LeanInfoTheory.Shannon.apply_le_fstMarginalTheoremLeanInfoTheory.Shannon.InfoMeasuresA joint atom mass is bounded by the mass of its first marginal atom. This is the basic support/domination fact behind conditioning on the first coordinate.line 418
LeanInfoTheory.Shannon.apply_le_sndMarginalTheoremLeanInfoTheory.Shannon.InfoMeasuresA joint atom mass is bounded by the mass of its second marginal atom.line 429
LeanInfoTheory.Shannon.apply_le_fstThirdMarginalTheoremLeanInfoTheory.Shannon.InfoMeasuresIn a triple law, a full atom is bounded by the corresponding `(first, third)` marginal atom.line 441
LeanInfoTheory.Shannon.apply_le_sndThirdMarginalTheoremLeanInfoTheory.Shannon.InfoMeasuresIn a triple law, a full atom is bounded by the corresponding `(second, third)` marginal atom.line 454
LeanInfoTheory.Shannon.apply_le_thirdMarginalTheoremLeanInfoTheory.Shannon.InfoMeasuresIn a triple law, a full atom is bounded by the mass of its third-coordinate marginal atom. This is the support fact needed for conditioning on `gamma`.line 467
LeanInfoTheory.Shannon.apply_eq_zero_of_fstMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresIf a first marginal atom has zero mass, then every joint atom over that first coordinate has zero mass.line 488
LeanInfoTheory.Shannon.apply_eq_zero_of_sndMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresIf a second marginal atom has zero mass, then every joint atom over that second coordinate has zero mass.line 498
LeanInfoTheory.Shannon.fstMarginal_ne_zero_of_apply_ne_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresNonzero joint mass forces the corresponding first marginal mass to be nonzero.line 507
LeanInfoTheory.Shannon.sndMarginal_ne_zero_of_apply_ne_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresNonzero joint mass forces the corresponding second marginal mass to be nonzero.line 517
LeanInfoTheory.Shannon.apply_eq_zero_of_fstThirdMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresIf a `(first, third)` marginal atom has zero mass, then every triple atom over that pair has zero mass.line 528
LeanInfoTheory.Shannon.apply_eq_zero_of_sndThirdMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresIf a `(second, third)` marginal atom has zero mass, then every triple atom over that pair has zero mass.line 539
LeanInfoTheory.Shannon.apply_eq_zero_of_thirdMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresIf a third marginal atom has zero mass, then every triple atom over that third coordinate has zero mass.line 550
LeanInfoTheory.Shannon.fstThirdMarginal_ne_zero_of_apply_ne_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresNonzero triple mass forces the corresponding `(first, third)` marginal mass to be nonzero.line 561
LeanInfoTheory.Shannon.sndThirdMarginal_ne_zero_of_apply_ne_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresNonzero triple mass forces the corresponding `(second, third)` marginal mass to be nonzero.line 573
LeanInfoTheory.Shannon.thirdMarginal_ne_zero_of_apply_ne_zeroTheoremLeanInfoTheory.Shannon.InfoMeasuresNonzero triple mass forces the corresponding third-coordinate marginal mass to be nonzero.line 585
LeanInfoTheory.Shannon.condEntropyDefinitionLeanInfoTheory.Shannon.InfoMeasuresConditional entropy `H(alpha | beta)` of a finite joint PMF on `alpha × beta`.line 596
LeanInfoTheory.Shannon.mutualInfoDefinitionLeanInfoTheory.Shannon.InfoMeasuresMutual information `I(alpha; beta)` of a finite joint PMF on `alpha × beta`.line 601
LeanInfoTheory.Shannon.condMutualInfoDefinitionLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information `I(alpha; beta | gamma)` of a finite joint PMF on `alpha × beta × gamma`, where the product is Lean's right-associated product.line 609
LeanInfoTheory.Shannon.condEntropyOfDefinitionLeanInfoTheory.Shannon.InfoMeasuresConditional entropy `H(X | Y)` for finite-valued random variables.line 616
LeanInfoTheory.Shannon.mutualInfoOfDefinitionLeanInfoTheory.Shannon.InfoMeasuresMutual information `I(X; Y)` for finite-valued random variables.line 622
LeanInfoTheory.Shannon.condMutualInfoOfDefinitionLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information `I(X; Y | Z)` for finite-valued random variables.line 628
LeanInfoTheory.Shannon.mutualInfo_map_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresMutual information is symmetric under swapping the two coordinates of a joint law.line 637
LeanInfoTheory.Shannon.mutualInfoOf_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresMutual information of finite-valued random variables is symmetric: `I(Y;X) = I(X;Y)`.line 645
LeanInfoTheory.Shannon.condMutualInfo_map_swap12TheoremLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information is symmetric in its first two coordinates: `I(B;A | C) = I(A;B | C)`.line 659
LeanInfoTheory.Shannon.condMutualInfoOf_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information of finite-valued random variables is symmetric in the first two variables: `I(Y;X | Z) = I(X;Y | Z)`.line 685
LeanInfoTheory.Shannon.entropyOf_fstTheoremLeanInfoTheory.Shannon.InfoMeasuresEntropy of the first coordinate projection is entropy of the first marginal.line 698
LeanInfoTheory.Shannon.entropyOf_sndTheoremLeanInfoTheory.Shannon.InfoMeasuresEntropy of the second coordinate projection is entropy of the second marginal.line 705
LeanInfoTheory.Shannon.jointEntropyOf_fst_sndTheoremLeanInfoTheory.Shannon.InfoMeasuresThe joint entropy of the two coordinate projections of an existing pair law is the entropy of that pair law itself.line 715
LeanInfoTheory.Shannon.condEntropyOf_fst_sndTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional entropy of the coordinate projections of a pair law recovers the PMF-level conditional entropy of that pair law.line 730
LeanInfoTheory.Shannon.mutualInfoOf_fst_sndTheoremLeanInfoTheory.Shannon.InfoMeasuresMutual information of the coordinate projections of a pair law recovers the PMF-level mutual information of that pair law.line 745
LeanInfoTheory.Shannon.entropyOf_thirdTheoremLeanInfoTheory.Shannon.InfoMeasuresEntropy of the third coordinate projection is entropy of the third marginal.line 757
LeanInfoTheory.Shannon.jointEntropyOf_fst_thirdTheoremLeanInfoTheory.Shannon.InfoMeasuresJoint entropy of the first and third coordinate projections is the entropy of the first-third marginal.line 768
LeanInfoTheory.Shannon.jointEntropyOf_snd_thirdTheoremLeanInfoTheory.Shannon.InfoMeasuresJoint entropy of the second and third coordinate projections is the entropy of the second-third marginal.line 780
LeanInfoTheory.Shannon.condMutualInfoOf_fst_snd_thirdTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information of the coordinate projections of a triple law recovers the PMF-level `I(first; second | third)` quantity.line 792
LeanInfoTheory.Shannon.condEntropy_eqTheoremLeanInfoTheory.Shannon.InfoMeasuresUnfolding lemma for the entropy-identity definition of conditional entropy.line 809
LeanInfoTheory.Shannon.mutualInfo_eqTheoremLeanInfoTheory.Shannon.InfoMeasuresUnfolding lemma for the entropy-identity definition of mutual information.line 815
LeanInfoTheory.Shannon.condMutualInfo_eqTheoremLeanInfoTheory.Shannon.InfoMeasuresUnfolding lemma for the entropy-identity definition of conditional mutual information.line 824
LeanInfoTheory.Shannon.entropy_eq_entropy_sndMarginal_add_condEntropyTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional entropy chain rule for a joint PMF: `H(A,B) = H(B) + H(A | B)`.line 838
LeanInfoTheory.Shannon.entropy_eq_entropy_fstMarginal_add_condEntropy_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSwapped conditional entropy chain rule for a joint PMF: `H(A,B) = H(A) + H(B | A)`.line 849
LeanInfoTheory.Shannon.jointEntropyOf_eq_entropyOf_add_condEntropyOfTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional entropy chain rule for finite-valued random variables: `H(X,Y) = H(Y) + H(X | Y)`.line 864
LeanInfoTheory.Shannon.jointEntropyOf_eq_entropyOf_add_condEntropyOf_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSwapped conditional entropy chain rule for finite-valued random variables: `H(X,Y) = H(X) + H(Y | X)`.line 877
LeanInfoTheory.Shannon.entropy_chain_rule_rightTheoremLeanInfoTheory.Shannon.InfoMeasuresRight-oriented PMF entropy chain rule: `H(A,B) = H(B) + H(A|B)`.line 888
LeanInfoTheory.Shannon.entropy_chain_rule_leftTheoremLeanInfoTheory.Shannon.InfoMeasuresLeft-oriented PMF entropy chain rule: `H(A,B) = H(A) + H(B|A)`.line 895
LeanInfoTheory.Shannon.jointEntropyOf_chain_rule_rightTheoremLeanInfoTheory.Shannon.InfoMeasuresRight-oriented random-variable entropy chain rule.line 902
LeanInfoTheory.Shannon.jointEntropyOf_chain_rule_leftTheoremLeanInfoTheory.Shannon.InfoMeasuresLeft-oriented random-variable entropy chain rule.line 910
LeanInfoTheory.Shannon.condEntropyOf_eqTheoremLeanInfoTheory.Shannon.InfoMeasuresRandom-variable conditional entropy rewrites to joint entropy minus entropy of the conditioning variable.line 923
LeanInfoTheory.Shannon.condEntropyOf_pair_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional joint entropy is invariant under swapping the two variables being conditioned: `H(Y,X|Z) = H(X,Y|Z)`.line 935
LeanInfoTheory.Shannon.condEntropyOf_pair_chain_ruleTheoremLeanInfoTheory.Shannon.InfoMeasuresTriple conditional-entropy chain rule: `H(X,Y|Z) = H(Y|Z) + H(X|Y,Z)`.line 973
LeanInfoTheory.Shannon.condEntropyOf_pair_chain_rule_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSwapped triple conditional-entropy chain rule: `H(X,Y|Z) = H(X|Z) + H(Y|X,Z)`.line 989
LeanInfoTheory.Shannon.mutualInfoOf_eqTheoremLeanInfoTheory.Shannon.InfoMeasuresRandom-variable mutual information rewrites to the standard entropy identity `H(X) + H(Y) - H(X,Y)`.line 1008
LeanInfoTheory.Shannon.condMutualInfoOf_eqTheoremLeanInfoTheory.Shannon.InfoMeasuresRandom-variable conditional mutual information rewrites to the entropy identity `H(X,Z) + H(Y,Z) - H(Z) - H(X,Y,Z)`.line 1019
LeanInfoTheory.Shannon.condMutualInfoOf_eq_condEntropyOf_sub_condEntropyOfTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information as a difference of conditional entropies: `I(X;Y|Z) = H(X|Z) - H(X|Y,Z)`.line 1034
LeanInfoTheory.Shannon.condMutualInfoOf_eq_condEntropyOf_sub_condEntropyOf_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSymmetric conditional-entropy difference form: `I(X;Y|Z) = H(Y|Z) - H(Y|X,Z)`.line 1049
LeanInfoTheory.Shannon.condMutualInfoOf_eq_condEntropyOf_add_condEntropyOf_sub_condEntropyOf_pairTheoremLeanInfoTheory.Shannon.InfoMeasuresConditional mutual information as conditional marginal entropies minus conditional joint entropy: `I(X;Y|Z) = H(X|Z) + H(Y|Z) - H(X,Y|Z)`.line 1068
LeanInfoTheory.Shannon.mutualInfo_eq_entropy_fstMarginal_sub_condEntropyTheoremLeanInfoTheory.Shannon.InfoMeasuresMutual information as `I(A;B) = H(A) - H(A|B)`.line 1083
LeanInfoTheory.Shannon.mutualInfo_eq_entropy_sndMarginal_sub_condEntropy_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresMutual information as `I(A;B) = H(B) - H(B|A)`.line 1091
LeanInfoTheory.Shannon.mutualInfoOf_eq_entropyOf_sub_condEntropyOfTheoremLeanInfoTheory.Shannon.InfoMeasuresRandom-variable form `I(X;Y) = H(X) - H(X|Y)`.line 1100
LeanInfoTheory.Shannon.mutualInfoOf_eq_entropyOf_sub_condEntropyOf_swapTheoremLeanInfoTheory.Shannon.InfoMeasuresSymmetric random-variable form `I(X;Y) = H(Y) - H(Y|X)`.line 1109
LeanInfoTheory.Shannon.mutualInfoOf_condEntropyOf_decompositionTheoremLeanInfoTheory.Shannon.InfoMeasuresDecompose `I(Y;Z)` through an auxiliary variable `X`. In canonical nats, `I(Y;Z) = H(Y|X) - I(X;Z|Y) - H(Y|(X,Z)) + I(X;Z)`, where `(X,Z)` is the ordered conditioning pair. The source type is arbitrary; only the three observed alphabets are finite.line 1128
LeanInfoTheory.Shannon.mutualInfo_map_diagTheoremLeanInfoTheory.Shannon.InfoMeasuresA diagonal joint law has mutual information equal to its source entropy.line 1145
LeanInfoTheory.Shannon.mutualInfoOf_selfTheoremLeanInfoTheory.Shannon.InfoMeasuresThe mutual information of a finite-valued variable with itself is its entropy.line 1164
LeanInfoTheory.Shannon.logSumTermDefinitionLeanInfoTheory.Shannon.LogSumThe zero-safe extended-real scalar term in the finite log-sum inequality. The conventions are `0 * log (0 / b) = 0` for every `b`, including `b = 0`, and `a * log (a / 0) = top` when `a` is positive.line 386
LeanInfoTheory.Shannon.logSumTerm_zero_leftTheoremLeanInfoTheory.Shannon.LogSumA zero numerator contributes zero to the extended log-sum.line 391
LeanInfoTheory.Shannon.logSumTerm_pos_zeroTheoremLeanInfoTheory.Shannon.LogSumA positive numerator over a zero denominator contributes `top`.line 396
LeanInfoTheory.Shannon.logSumTerm_ne_botTheoremLeanInfoTheory.Shannon.LogSumAn extended log-sum term is never `bottom`.line 407
LeanInfoTheory.Shannon.sum_logSumTerm_ne_botTheoremLeanInfoTheory.Shannon.LogSumEvery finite selected sum of extended log-sum terms is never `bottom`.line 423
LeanInfoTheory.Shannon.logSum_inequalityTheoremLeanInfoTheory.Shannon.LogSumFinite log-sum inequality with the zero-safe conventions of `logSumTerm`. In particular, a selected positive numerator over a zero denominator makes the right-hand side `top`; no support or positivity guard is required.line 495
LeanInfoTheory.Shannon.logSum_eq_iff_exists_constant_ratioTheoremLeanInfoTheory.Shannon.LogSumEquality in the zero-safe finite log-sum inequality. Equality holds exactly when all active selected pairs have one common `ENNReal` numerator-to-denominator ratio. Selected `(0, 0)` pairs are inactive; the common ratio may be finite or `top`.line 547
LeanInfoTheory.Shannon.real_logSum_inequality_of_supportTheoremLeanInfoTheory.Shannon.LogSumGuarded Real finite log-sum inequality. The support guard excludes positive-over-zero selected pairs while permitting selected `(0, 0)` pairs.line 694
LeanInfoTheory.Shannon.real_logSum_eq_iff_exists_constant_ratio_of_supportTheoremLeanInfoTheory.Shannon.LogSumEquality in the guarded Real finite log-sum inequality holds exactly when all active selected pairs have one common finite ratio.line 709
LeanInfoTheory.Shannon.condFstGivenSndDefinitionLeanInfoTheory.Shannon.SemanticBridge.ConditionalConditional law of the first coordinate given a nonzero second-coordinate atom. Mathematically, this is the finite PMF `P_{A | B=b}(a) = P_{A,B}(a,b) / P_B(b)`. The proof argument `hb : sndMarginal p b ≠ 0` is part of the API so that zero-probability conditioning atoms do not receive a fake default distribution.line 52
LeanInfoTheory.Shannon.condFstGivenSnd_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalAtom formula for the conditional law: `P_{A | B=b}(a) = P_{A,B}(a,b) / P_B(b)`.line 72
LeanInfoTheory.Shannon.condFstGivenSnd_proof_irrelTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe conditional PMF does not depend on which proof of nonzero marginal mass was used to construct it.line 81
LeanInfoTheory.Shannon.condFstGivenSnd_apply_eq_zero_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalAn atom has zero conditional mass exactly when the corresponding joint atom has zero mass.line 93
LeanInfoTheory.Shannon.condFstGivenSnd_apply_ne_zero_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalAn atom has nonzero conditional mass exactly when the corresponding joint atom has nonzero mass.line 112
LeanInfoTheory.Shannon.support_condFstGivenSndTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe support of `P_{A | B=b}` is the fiber of the joint support over `b`.line 122
LeanInfoTheory.Shannon.condFstGivenSnd_mul_sndMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalJoint mass factors as conditional mass times the conditioning marginal: `P_{A | B=b}(a) * P_B(b) = P_{A,B}(a,b)`.line 133
LeanInfoTheory.Shannon.sndMarginal_mul_condFstGivenSndTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalJoint mass factors as the conditioning marginal times conditional mass: `P_B(b) * P_{A | B=b}(a) = P_{A,B}(a,b)`.line 144
LeanInfoTheory.Shannon.sndMarginal_toReal_mul_condFstGivenSnd_toRealTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalReal-valued version of the joint factorization: `P_B(b) * P_{A | B=b}(a) = P_{A,B}(a,b)` after converting masses to `Real`.line 155
LeanInfoTheory.Shannon.condEntropyFstGivenSndDefinitionLeanInfoTheory.Shannon.SemanticBridge.ConditionalEntropy of the conditional fiber, with explicit zero-mass branch. This helper is intended for expected conditional entropy formulas. If `P_B(b)=0`, the branch is the number `0`, not the entropy of an arbitrary default conditional PMF.line 171
LeanInfoTheory.Shannon.condEntropyFstGivenSnd_of_sndMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalZero-marginal conditioning atoms contribute zero to conditional-fiber entropy.line 180
LeanInfoTheory.Shannon.condEntropyFstGivenSnd_of_sndMarginal_ne_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalOn nonzero conditioning atoms, `condEntropyFstGivenSnd` is the entropy of the canonical conditional PMF `P_{A | B=b}`.line 190
LeanInfoTheory.Shannon.sndMarginal_toReal_mul_condEntropyFstGivenSndTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalPer-fiber conditional entropy identity. For each conditioning atom `b`, `p_B(b) * H(P_{A | B=b}) = sum_a h(p(a,b)) - h(p_B(b))`, where `h(x) = -x log x`. If `p_B(b)=0`, the left side uses the explicit zero branch of `condEntropyFstGivenSnd`, and the right side is zero because every joint atom over `b` has zero mass.line 205
LeanInfoTheory.Shannon.condEntropy_eq_sum_sndMarginal_mul_condEntropyFstGivenSndTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalExpected conditional entropy formula for the finite conditional-law API: `H(A | B) = sum_b p_B(b) * H(P_{A | B=b})`. The right-hand side is written using `condEntropyFstGivenSnd`, whose value is `0` on zero-marginal conditioning atoms and the entropy of the canonical conditional PMF on nonzero atoms.line 273
LeanInfoTheory.Shannon.pairThirdLawDefinitionLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe right-associated law `P_{A,B,C}` viewed as a law on `((A, B), C)`. This is the law whose conditional fibers over `C=c` are joint laws on `A × B`.line 311
LeanInfoTheory.Shannon.pairThirdLaw_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalAtom formula for the reassociated law `((A,B),C)`.line 317
LeanInfoTheory.Shannon.sndMarginal_pairThirdLawTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe second marginal of the reassociated law `((A,B),C)` is the law of `C`.line 335
LeanInfoTheory.Shannon.entropy_pairThirdLawTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalReassociating `(A,B,C)` as `((A,B),C)` preserves entropy.line 343
LeanInfoTheory.Shannon.condEntropy_pairThirdLaw_chain_ruleTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalPMF form of the triple conditional-entropy chain rule: `H(A,B|C) = H(B|C) + H(A|B,C)`.line 353
LeanInfoTheory.Shannon.condEntropy_pairThirdLaw_chain_rule_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalSwapped PMF form of the triple conditional-entropy chain rule: `H(A,B|C) = H(A|C) + H(B|A,C)`.line 377
LeanInfoTheory.Shannon.condFstSndGivenThirdDefinitionLeanInfoTheory.Shannon.SemanticBridge.ConditionalConditional joint law of the first two coordinates given a nonzero third coordinate atom. Mathematically, this is `P_{A,B | C=c}(a,b) = P_{A,B,C}(a,b,c) / P_C(c)`.line 402
LeanInfoTheory.Shannon.condFstSndGivenThird_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalAtom formula for `P_{A,B | C=c}`.line 423
LeanInfoTheory.Shannon.thirdMarginal_mul_condFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalJoint mass factors through the conditional joint law: `P_C(c) * P_{A,B|C=c}(a,b) = P_{A,B,C}(a,b,c)`.line 435
LeanInfoTheory.Shannon.thirdMarginal_toReal_mul_condFstSndGivenThird_toRealTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalReal-valued joint factorization for the conditional joint law: `P_C(c) * P_{A,B|C=c}(a,b) = P_{A,B,C}(a,b,c)`.line 448
LeanInfoTheory.Shannon.sndMarginal_fstThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe second marginal of the `(A,C)` law is the law of `C`.line 462
LeanInfoTheory.Shannon.sndMarginal_sndThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe second marginal of the `(B,C)` law is the law of `C`.line 478
LeanInfoTheory.Shannon.fstMarginal_condFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe first marginal of `P_{A,B|C=c}` is the conditional law `P_{A|C=c}`.line 500
LeanInfoTheory.Shannon.sndMarginal_condFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe second marginal of `P_{A,B|C=c}` is the conditional law `P_{B|C=c}`.line 530
LeanInfoTheory.Shannon.condFstGivenSnd_pairThirdLaw_eq_condFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalThe conditional law of `(A,B)` given `C=c`, obtained by conditioning the reassociated law `((A,B),C)`, is the same as `condFstSndGivenThird`.line 561
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThirdDefinitionLeanInfoTheory.Shannon.SemanticBridge.ConditionalConditional mutual information of the fiber over `C=c`. The value is zero when `P_C(c)=0`; otherwise it is the mutual information of the conditional joint law `P_{A,B|C=c}`.line 581
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThird_of_thirdMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalZero-marginal conditioning atoms contribute zero fiber mutual information.line 592
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThird_of_thirdMarginal_ne_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalOn nonzero third-coordinate atoms, the fiber CMI is the mutual information of `P_{A,B|C=c}`.line 604
LeanInfoTheory.Shannon.condMutualInfo_eq_condEntropy_marginalsTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalConditional mutual information can be rewritten as `H(A|C) + H(B|C) - H(A,B|C)`.line 617
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThird_eq_entropy_fibers_of_ne_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalOn a nonzero third-coordinate atom, fiber CMI is the entropy identity for the three conditional fibers: `I(A;B | C=c) = H(A|C=c) + H(B|C=c) - H(A,B|C=c)`.line 634
LeanInfoTheory.Shannon.thirdMarginal_toReal_mul_condMutualInfoFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalWeighted pointwise bridge between fiber CMI and the three conditional entropy fibers. The zero-marginal case is killed by the factor `P_C(c)`.line 663
LeanInfoTheory.Shannon.condMutualInfo_eq_sum_thirdMarginal_mul_condMutualInfoFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalExpected conditional mutual information formula: `I(A;B | C) = sum_c P_C(c) I(A;B | C=c)`. The fiber term is zero on zero-marginal `c` and otherwise the mutual information of `P_{A,B|C=c}`.line 685
LeanInfoTheory.Shannon.conditionalKlDivDefinitionLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLConditional relative entropy between two channels under a common input law. This is the KL divergence between the two induced joint laws. Consequently, channel values outside the support of `r` do not affect the result: their entire joint-law fiber has zero mass. No per-fiber KL convention is imposed at those null base atoms.line 51
LeanInfoTheory.Shannon.conditionalKlDiv_selfTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLConditional relative entropy from a channel to itself is zero.line 62
LeanInfoTheory.Shannon.conditionalKlDiv_eq_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLConditional relative entropy is the base-law-weighted sum of the fiberwise KL divergences. This identity is unconditional in `ENNReal`. An infinite KL value on a null base fiber contributes `0 * ⊤ = 0`, while an infinite KL value on an active fiber makes both sides `⊤`.line 117
LeanInfoTheory.Shannon.toReal_conditionalKlDiv_eq_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLReal-valued weighted-fiber formula for conditional relative entropy under support inclusion on the active base atoms: `D(W || V | r) = ∑ x, r(x) D(W_x || V_x)`. No support condition is imposed when `r x = 0`. In particular, an infinite fiber KL divergence on a null base atom contributes zero to the canonical `ENNReal` weighted sum before conversion to `Real`.line 232
LeanInfoTheory.Shannon.klDiv_channelJoint_eq_add_conditionalKlDivTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLKL chain rule for two finite channel-joint laws: `D(P_X P_{Y|X} || Q_X Q_{Y|X}) = D(P_X || Q_X) + D(P_{Y|X} || Q_{Y|X} | P_X)`. The conditional term is weighted by the numerator base law `p`. The identity is unconditional in `ENNReal`, including when either summand is `⊤`.line 271
LeanInfoTheory.Shannon.toReal_klDiv_channelJoint_eq_add_conditionalKlDivTheoremLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLReal-valued finite joint KL chain rule under support inclusion for the base laws and for every active numerator fiber: `D(P_X P_{Y|X} || Q_X Q_{Y|X}) = D(P_X || Q_X) + D(P_{Y|X} || Q_{Y|X} | P_X)`. The fiber condition is required only on `p.support`; an infinite fiber KL divergence at a null numerator atom does not affect the identity.line 300
LeanInfoTheory.Shannon.klDiv_bind_le_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityKL divergence is jointly convex under a common finite PMF-valued selector. The result is canonical in `ENNReal`. An inactive selector component may have infinite KL because its weighted contribution is `0 * top = 0`.line 262
LeanInfoTheory.Shannon.toReal_klDiv_bind_le_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityReal-valued KL joint convexity under support inclusion for every active selector component. No support condition is required when the selector mass is zero, even if that inactive component has infinite KL.line 291
LeanInfoTheory.Shannon.klDiv_binaryMixture_leTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityBinary joint convexity of KL divergence. The weight is `t` on the first component and `1 - t` on the second.line 338
LeanInfoTheory.Shannon.toReal_klDiv_binaryMixture_leTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityReal-valued binary KL joint convexity with support assumptions only for components whose weights can be nonzero. At `t = 0`, only the second support implication is used; at `t = 1`, only the first is used.line 379
LeanInfoTheory.Shannon.klDiv_binaryMixture_eq_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityEquality in binary KL joint convexity for an interior weight. The component support assumptions exclude infinite component divergences. Under those guards, equality holds exactly when the two component likelihood ratios agree pointwise, expressed without division by the cross-product law. When both reference masses at an atom are positive, the cross-product law is the usual equality of likelihood ratios. If one reference mass vanishes, support inclusion forces its corresponding numerator mass to vanish, so the division-free statement handles the absent component without assigning a meaning to `0 / 0`.line 858
LeanInfoTheory.Shannon.toReal_klDiv_binaryMixture_eq_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityReal-valued equality in binary KL joint convexity for an interior weight. The same component support assumptions make every KL divergence finite, so the exact cross-product characterization is preserved by `ENNReal.toReal`. The division-free condition has the same null-mass interpretation as the canonical `ENNReal` theorem: a component absent at an atom contributes matching zero numerator and reference masses rather than an artificial likelihood ratio.line 888
LeanInfoTheory.Shannon.mutualInfo_channelJoint_eq_entropy_bind_sub_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityMutual information across a finite PMF-valued channel is output entropy minus the input-weighted entropy of the channel laws.line 949
LeanInfoTheory.Shannon.sum_mul_mutualInfo_channelJoint_leTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityFor a fixed finite channel, mutual information is concave in the input law under a common finite PMF-valued selector.line 992
LeanInfoTheory.Shannon.mutualInfo_binaryMixture_input_concaveTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityFor a fixed finite channel, mutual information is concave along a binary mixture of input laws.line 1039
LeanInfoTheory.Shannon.mutualInfo_channelMixture_le_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityFor a fixed finite input law, mutual information is convex under a common finite PMF-valued selector of channels.line 1116
LeanInfoTheory.Shannon.mutualInfo_binaryChannelMixture_leTheoremLeanInfoTheory.Shannon.SemanticBridge.ConvexityFor a fixed finite input law, mutual information is convex along a binary mixture of channels.line 1182
LeanInfoTheory.Shannon.pmfChannelKernelDefinitionLeanInfoTheory.Shannon.SemanticBridge.DataProcessingThe mathlib kernel associated to a countable PMF-valued channel. This is a semantic view of the existing raw channel function, not a second public channel representation.line 58
LeanInfoTheory.Shannon.pmfChannelKernel.instIsMarkovKernelInstanceLeanInfoTheory.Shannon.SemanticBridge.DataProcessingA PMF-valued channel induces a Markov kernel through `pmfChannelKernel`.line 66
LeanInfoTheory.Shannon.pmfChannelKernel_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingEvaluating the kernel associated to a PMF channel recovers its PMF measure.line 77
LeanInfoTheory.Shannon.channelJoint_toMeasureTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingThe measure of an induced PMF joint law is the composition-product of the input measure and the associated Markov kernel.line 89
LeanInfoTheory.Shannon.channelPosteriorDefinitionLeanInfoTheory.Shannon.SemanticBridge.DataProcessingThe total posterior channel associated to an input law and a finite stochastic channel. On an output atom of positive probability this is the usual posterior input law. On a null output fiber it uses the fallback already documented by `condFstGivenSndChannel`; reconstruction makes that arbitrary branch semantically irrelevant.line 114
LeanInfoTheory.Shannon.channelPosterior_reconstructs_jointTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingSampling the posterior from the channel output law reconstructs the induced joint law in output-input order.line 123
LeanInfoTheory.Shannon.isSufficientChannel_iff_exists_common_posteriorTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingA finite-input channel is sufficient for a model family exactly when one parameter-independent posterior channel agrees with every model posterior on each supported output fiber. Writing `Q_t = (model t).bind W`, the witness `R` satisfies `channelPosterior (model t) W b = R b` whenever `Q_t b != 0`. Consequently, two models supporting the same output have the same posterior there. A model for which `b` is null imposes no condition, although another supporting model may determine `R b`; if `b` is null for the entire family, that row is wholly unconstrained. The support guard prevents the arbitrary fallback used by the total posterior on a null fiber from acquiring conditional-probability meaning.line 144
LeanInfoTheory.Shannon.klDiv_channel_eq_add_posteriorTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingExact KL decomposition for two input laws passed through the same finite stochastic channel. The first term is the divergence between the output laws. The remainder is the divergence between the two posterior kernels over the first output law, stated with mathlib composition-product measures. No support-inclusion assumption is needed because the identity is `ENNReal`-valued.line 243
LeanInfoTheory.Shannon.klDiv_channel_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingFinite relative entropy contracts when two input laws pass through the same stochastic channel. This is the primary channel data-processing inequality. It is unconditional because KL divergence is valued in `ENNReal`.line 299
LeanInfoTheory.Shannon.klDiv_channel_eq_iff_posterior_ae_eqTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingEquality in finite KL data processing holds exactly when the two posterior kernels agree almost everywhere under the first output law. Input support inclusion excludes the uninformative infinite-divergence case. This is the measure-level equality bridge; finite pointwise posterior forms can be derived by replacing almost-everywhere equality with equality on supported output atoms.line 353
LeanInfoTheory.Shannon.klDiv_channel_eq_iff_posterior_eq_on_supportTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingEquality in finite KL data processing holds exactly when the two posterior PMFs agree on every output atom reached by the first input law. This is the primary finite-facing equality theorem. The input support condition excludes infinite KL divergence, while the output support condition in the conclusion leaves the total posterior's arbitrary null-fiber values irrelevant.line 376
LeanInfoTheory.Shannon.toReal_klDiv_channel_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingReal-valued finite relative entropy contracts through a common stochastic channel when the first input law is supported by the second. Only the input support condition is needed; no separate support hypothesis on the output laws is required.line 400
LeanInfoTheory.Shannon.toReal_klDiv_channel_eq_iff_posterior_eq_on_supportTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingEquality in real-valued finite KL data processing holds exactly when the two posterior PMFs agree on every output atom reached by the first input law. Input support inclusion makes both KL divergences finite, so this theorem has no `ENNReal.toReal` top-branch ambiguity.line 420
LeanInfoTheory.Shannon.klDiv_map_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingKL data processing for a deterministic map of a finite alphabet.line 442
LeanInfoTheory.Shannon.toReal_klDiv_map_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingReal-valued KL data processing for a deterministic map, under input support inclusion.line 457
LeanInfoTheory.Shannon.klDiv_channelComp_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingAppending a common channel stage cannot increase the KL divergence between the two intermediate output laws.line 485
LeanInfoTheory.Shannon.klDiv_channel_cascade_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingTextbook-facing alias for `ENNReal`-valued KL contraction along a cascade.line 499
LeanInfoTheory.Shannon.toReal_klDiv_channelComp_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingReal-valued KL contraction for a channel cascade. The original input support condition suffices for the intermediate laws as well.line 515
LeanInfoTheory.Shannon.toReal_klDiv_channel_cascade_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingTextbook-facing alias for real-valued KL contraction along a cascade.line 532
LeanInfoTheory.Shannon.klDiv_channel_invariant_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingKL divergence to an invariant reference law cannot increase after one step of a finite stochastic channel.line 552
LeanInfoTheory.Shannon.toReal_klDiv_channel_invariant_leTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingReal-valued KL divergence to an invariant reference law contracts when the input law is supported by that reference.line 566
LeanInfoTheory.Shannon.entropy_le_entropy_bind_of_uniform_invariantTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingA finite channel that preserves the uniform law cannot decrease Shannon entropy. The discrete measurable structure used by the KL proof remains local, so the statement has only the natural finite nonempty alphabet assumptions.line 583
LeanInfoTheory.Shannon.entropy_le_entropy_bind_of_doublyStochasticTheoremLeanInfoTheory.Shannon.SemanticBridge.DataProcessingA finite doubly stochastic channel cannot decrease Shannon entropy. Each `W a` is already a probability law, hence supplies the row-stochastic condition. The displayed hypothesis is the remaining column-sum condition. No transition-matrix representation is introduced.line 604
LeanInfoTheory.Shannon.selfInfoDefinitionLeanInfoTheory.Shannon.SemanticBridge.EntropySelf-information of an atom under a finite PMF, in nats. It is `-log p(a)` when the real mass of `a` is nonzero, and `0` on zero-mass atoms. The zero branch is the usual entropy convention that zero-probability outcomes contribute no expected information.line 41
LeanInfoTheory.Shannon.selfInfo_of_toReal_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.EntropyA zero-mass atom has zero self-information by convention.line 46
LeanInfoTheory.Shannon.selfInfo_of_toReal_ne_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.EntropyA nonzero-mass atom has self-information `-log p(a)`.line 52
LeanInfoTheory.Shannon.toReal_mul_selfInfoTheoremLeanInfoTheory.Shannon.SemanticBridge.EntropyMultiplying self-information by the atom mass recovers the `Real.negMulLog` entropy summand.line 61
LeanInfoTheory.Shannon.entropy_eq_integral_selfInfoTheoremLeanInfoTheory.Shannon.SemanticBridge.EntropySemantic bridge for finite entropy: the finite-sum definition of `Shannon.entropy` is the expected self-information with respect to `PMF.toMeasure`. Informally, this is the textbook identity `H(P) = E[-log P(X)]`, with the zero-mass convention handled by `selfInfo`.line 75
LeanInfoTheory.Shannon.familyEntropy_monoTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyEntropy is monotone under inclusion of finite family atoms.line 58
LeanInfoTheory.Shannon.familyEntropyOf_monoTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilySource-family entropy is monotone under inclusion of finite atoms.line 70
LeanInfoTheory.Shannon.familyCondEntropy_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyConditional entropy of two finite subfamilies is nonnegative.line 79
LeanInfoTheory.Shannon.familyCondEntropyOf_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyConditional entropy of two finite source-indexed subfamilies is nonnegative.line 88
LeanInfoTheory.Shannon.familyCondMutualInfo_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyConditional mutual information of finite subfamilies is nonnegative.line 100
LeanInfoTheory.Shannon.familyCondMutualInfoOf_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyConditional mutual information of finite source-indexed subfamilies is nonnegative.line 112
LeanInfoTheory.Shannon.familyEntropy_submodularTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyEntropy of finite family atoms is submodular: `H(A) + H(B) - H(A ∪ B) - H(A ∩ B) ≥ 0`.line 124
LeanInfoTheory.Shannon.familyEntropyOf_submodularTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyEntropy of finite source-indexed family atoms is submodular.line 148
LeanInfoTheory.Shannon.familyMutualInfo_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyMutual information of two finite subfamilies is nonnegative.line 160
LeanInfoTheory.Shannon.familyMutualInfoOf_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyMutual information of two finite source-indexed subfamilies is nonnegative.line 170
LeanInfoTheory.Shannon.familyMutualInfo_le_entropy_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyFamily mutual information is at most the entropy of its left atom.line 179
LeanInfoTheory.Shannon.familyMutualInfo_le_entropy_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyFamily mutual information is at most the entropy of its right atom.line 188
LeanInfoTheory.Shannon.familyMutualInfoOf_le_entropyOf_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilySource-family mutual information is at most the entropy of its left atom.line 199
LeanInfoTheory.Shannon.familyMutualInfoOf_le_entropyOf_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilySource-family mutual information is at most the entropy of its right atom.line 208
LeanInfoTheory.Shannon.familyCondEntropy_le_entropyTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyConditioning on a finite family atom cannot increase family entropy.line 217
LeanInfoTheory.Shannon.familyCondEntropyOf_le_entropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyConditioning cannot increase entropy for finite source-indexed subfamilies.line 227
LeanInfoTheory.Shannon.familyCondEntropy_union_le_condEntropyTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyAdding a finite conditioning atom cannot increase family conditional entropy.line 238
LeanInfoTheory.Shannon.familyCondEntropyOf_union_le_condEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyAdding a finite conditioning atom cannot increase source-family conditional entropy.line 251
LeanInfoTheory.Shannon.familyEntropy_union_le_addTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyEntropy of a union of two finite family atoms is subadditive.line 261
LeanInfoTheory.Shannon.familyEntropyOf_union_le_addTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilySource-family entropy of a union of two finite atoms is subadditive.line 275
LeanInfoTheory.Shannon.familyEntropy_le_sum_singletonsTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyFamily entropy is at most the sum of the selected singleton entropies.line 287
LeanInfoTheory.Shannon.familyEntropyOf_le_sum_singletonsTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilySource-family entropy is at most the sum of the selected singleton entropies.line 311
LeanInfoTheory.Shannon.familyEntropy_subadditivity_of_nodupTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyTextbook n-way entropy subadditivity for a list of distinct variable names.line 323
LeanInfoTheory.Shannon.familyEntropyOf_subadditivity_of_nodupTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilySource-family textbook n-way entropy subadditivity for distinct variable names.line 337
LeanInfoTheory.Shannon.IsMutuallyIndependentFamilyDefinitionLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceA finite atom of a dependent PMF family is mutually independent when its joint marginal factors pointwise into its one-coordinate marginals. The product is indexed by the subtype of variables selected by `s`. This statement therefore supports dependent component alphabets, arbitrary ambient variable types, empty and singleton atoms, and zero coordinate masses without additional typeclass assumptions.line 54
LeanInfoTheory.Shannon.IsMutuallyIndependentFamilyOfDefinitionLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceMutual independence of a finite source-indexed family. This is a thin specialization of `IsMutuallyIndependentFamily` to the joint pushforward law `familyLawOf p X`; it introduces no separate source semantics.line 67
LeanInfoTheory.Shannon.isMutuallyIndependentFamily_emptyTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceEvery dependent PMF family is mutually independent on the empty atom.line 427
LeanInfoTheory.Shannon.isMutuallyIndependentFamily_singletonTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceEvery one-coordinate marginal is mutually independent.line 463
LeanInfoTheory.Shannon.isMutuallyIndependentFamilyOf_pair_iff_isIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceFor distinct indices, mutual independence of a two-variable source family is exactly independence of the corresponding pair of random variables. Distinctness is essential: when the indices coincide, the selected atom collapses to a singleton and is automatically mutually independent, whereas a random variable need not be independent of itself.line 644
LeanInfoTheory.Shannon.isMutuallyIndependentFamily_monoTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceMutual independence of a finite atom is inherited by each of its subatoms. Here the atom is finite because it is a `Finset`; the additional typeclass assumption says that the ambient family has pointwise-finite coordinate alphabets.line 667
LeanInfoTheory.Shannon.familyEntropy_eq_sum_singletons_iff_isMutuallyIndependentFamilyTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceThe entropy of a finite dependent-family marginal is the sum of its one-coordinate entropies exactly when the selected family is mutually independent.line 705
LeanInfoTheory.Shannon.familyEntropyOf_eq_sum_singletons_iff_isMutuallyIndependentFamilyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceThe source-family form of the finite entropy-additivity characterization of mutual independence.line 803
LeanInfoTheory.Shannon.fstMarginal_toReal_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsReal-valued first-marginal mass formula. Mathematically, for a finite joint PMF `p` on `alpha × beta`, `p_A(a) = sum_b p(a,b)`, now stated after converting all finite masses to real numbers.line 50
LeanInfoTheory.Shannon.sndMarginal_toReal_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsReal-valued second-marginal mass formula. Mathematically, for a finite joint PMF `p` on `alpha × beta`, `p_B(b) = sum_a p(a,b)`, now stated after converting all finite masses to real numbers.line 66
LeanInfoTheory.Shannon.sum_toReal_mul_fstMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsRewrite an expectation of a first-coordinate observable under the joint law as an expectation under the first marginal: `sum_{a,b} p(a,b) f(a) = sum_a p_A(a) f(a)`.line 80
LeanInfoTheory.Shannon.sum_toReal_mul_sndMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsRewrite an expectation of a second-coordinate observable under the joint law as an expectation under the second marginal: `sum_{a,b} p(a,b) f(b) = sum_b p_B(b) f(b)`.line 103
LeanInfoTheory.Shannon.entropy_eq_sum_toReal_mul_neg_logTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsEntropy as the elementary finite sum `sum_a p(a) * (-log p(a))`. This is definitionally the same as the `Real.negMulLog` formula, but this shape is better for comparing entropy identities with KL-divergence sums.line 131
LeanInfoTheory.Shannon.entropy_fstMarginal_eq_sum_jointTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsFirst-marginal entropy as a joint-law expectation: `H(A) = sum_{a,b} p(a,b) * (-log p_A(a))`.line 145
LeanInfoTheory.Shannon.entropy_sndMarginal_eq_sum_jointTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsSecond-marginal entropy as a joint-law expectation: `H(B) = sum_{a,b} p(a,b) * (-log p_B(b))`.line 164
LeanInfoTheory.Shannon.mutualInfo_eq_sum_neg_logTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsMutual information written as the joint expectation of the three entropy summands: `I(A;B) = sum_{a,b} p(a,b) * (-log p_A(a) + -log p_B(b) - -log p(a,b))`.line 186
LeanInfoTheory.Shannon.mutualInfo_summand_eq_log_ratioTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsPointwise algebra behind the KL formula for mutual information. For every atom `(a,b)`, the weighted entropy summand equals `p(a,b) * log (p(a,b) / (p_A(a) * p_B(b)))`. If `p(a,b)=0`, both sides are zero; otherwise nonzero joint mass forces both marginal masses to be nonzero.line 207
LeanInfoTheory.Shannon.mutualInfo_eq_sum_log_ratioTheoremLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsFinite log-ratio formula for mutual information: `I(A;B) = sum_{a,b} p(a,b) log (p(a,b) / (p_A(a) p_B(b)))`.line 239
LeanInfoTheory.Shannon.IsIndependentDefinitionLeanInfoTheory.Shannon.SemanticBridge.IndependenceA joint PMF is independent when it is the product of its marginals.line 44
LeanInfoTheory.Shannon.IsIndependentOfDefinitionLeanInfoTheory.Shannon.SemanticBridge.IndependenceTwo random variables are independent when their joint law is independent.line 49
LeanInfoTheory.Shannon.IsCondIndependentDefinitionLeanInfoTheory.Shannon.SemanticBridge.IndependenceThe first two coordinates of a triple PMF are conditionally independent given the third when every atom satisfies the cross-product factorization `p(a,b,c) * p_C(c) = p_AC(a,c) * p_BC(b,c)`. This definition is meaningful on null fibers and does not require choosing a conditional PMF from a proof that `p_C(c) ≠ 0`.line 62
LeanInfoTheory.Shannon.IsCondIndependentOfDefinitionLeanInfoTheory.Shannon.SemanticBridge.IndependenceTwo random variables are conditionally independent given a third when their mapped triple law is conditionally independent.line 72
LeanInfoTheory.Shannon.isCondIndependent_map_swap12TheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceSwapping the first two coordinates of a triple law preserves conditional independence.line 80
LeanInfoTheory.Shannon.isCondIndependentOf_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditional independence of random variables is symmetric in its first two variables.line 126
LeanInfoTheory.Shannon.isIndependent_iff_apply_eq_mul_marginalsTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceIndependence is equivalent to pointwise factorization into marginal masses.line 141
LeanInfoTheory.Shannon.isIndependent_indepProdTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceThe independent product of two PMFs is independent.line 160
LeanInfoTheory.Shannon.isIndependent_map_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceSwapping the coordinates of a joint law preserves independence.line 167
LeanInfoTheory.Shannon.isIndependentOf_iff_map_eq_indepProdTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceRandom-variable independence is equality of the joint law with the independent product of the two individual laws.line 205
LeanInfoTheory.Shannon.isIndependentOf_comp_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceDeterministic processing of the right variable preserves independence. The source and observed types are arbitrary: the PMF mapped-law proof needs no finiteness, measurable-space, or injectivity assumptions on the processing map.line 219
LeanInfoTheory.Shannon.isIndependentOf_iff_indepFunTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceThe PMF mapped-law definition of random-variable independence agrees with mathlib's measure-theoretic `ProbabilityTheory.IndepFun` predicate. Measurability and measurable-singleton assumptions are explicit here because they belong to the semantic bridge, not to the PMF-first definition `IsIndependentOf`.line 238
LeanInfoTheory.Shannon.isIndependentOf_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceIndependence of random variables is symmetric.line 255
LeanInfoTheory.Shannon.mutualInfo_eq_zero_iff_isIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceFinite mutual information is zero exactly when the joint PMF is independent. The proof chooses the discrete measurable structure only locally, uses the KL representation of mutual information, and discharges the necessary real-KL finiteness guard through support inclusion.line 276
LeanInfoTheory.Shannon.mutualInfoOf_eq_zero_iff_isIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceFinite-valued random variables have zero mutual information exactly when their mapped joint law is independent.line 297
LeanInfoTheory.Shannon.condEntropy_eq_entropy_left_iff_isIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditioning preserves the entropy of the left coordinate exactly when the two coordinates are independent.line 312
LeanInfoTheory.Shannon.condEntropyOf_eq_entropyOf_iff_isIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditioning preserves `H(X)` exactly when the finite-valued random variables `X` and `Y` are independent.line 328
LeanInfoTheory.Shannon.jointEntropy_eq_add_marginalEntropy_iff_isIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceJoint entropy is additive exactly when the two coordinates are independent.line 338
LeanInfoTheory.Shannon.jointEntropyOf_eq_add_entropyOf_iff_isIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceJoint entropy is additive exactly when the finite-valued random variables are independent.line 355
LeanInfoTheory.Shannon.jointEntropy_additive_iff_isIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceShort PMF alias for additivity of joint entropy under independence.line 368
LeanInfoTheory.Shannon.jointEntropyOf_additive_iff_isIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceShort random-variable alias for additivity of joint entropy under independence.line 376
LeanInfoTheory.Shannon.condMutualInfo_eq_zero_iff_condMutualInfoFstSndGivenThird_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceFinite conditional mutual information is zero exactly when every positive-mass conditional fiber has zero mutual information. The forward direction uses nonnegativity to extract zero from each term in the averaged conditional-mutual-information formula. The marginal guard lets us cancel the positive real fiber weight. In the reverse direction, null fibers have zero weight and every positive-mass fiber is zero by hypothesis.line 395
LeanInfoTheory.Shannon.isCondIndependent_iff_isIndependent_condFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceThe cross-product definition of conditional independence is equivalent to ordinary independence of the conditional joint law on every positive-mass fiber. No condition is needed on null fibers: the cross-product identity holds there because the corresponding first-third marginal has zero mass. The right-hand side is independent of the particular proof of nonzero marginal mass.line 438
LeanInfoTheory.Shannon.condMutualInfo_eq_zero_iff_isCondIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceFinite conditional mutual information is zero exactly when the first two coordinates are conditionally independent given the third. No conditional law needs to be chosen on null fibers. `IsCondIndependent` uses the cross-product identity on the original PMF, where those fibers satisfy the identity directly; conditional PMFs appear only for positive-mass fibers inside the proof.line 538
LeanInfoTheory.Shannon.condMutualInfoOf_eq_zero_iff_isCondIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceFinite-valued random variables have zero conditional mutual information exactly when they are conditionally independent under their mapped triple law.line 560
LeanInfoTheory.Shannon.condEntropy_eq_condEntropy_fstThirdMarginal_iff_isCondIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditioning the first coordinate on the second preserves its entropy given the third coordinate exactly under conditional independence.line 576
LeanInfoTheory.Shannon.condEntropyOf_eq_condEntropyOf_iff_isCondIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditioning `X` on `Y` preserves its entropy given `Z` exactly when `X` and `Y` are conditionally independent given `Z`.line 595
LeanInfoTheory.Shannon.condEntropy_pair_eq_add_condEntropy_iff_isCondIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditional joint entropy is additive exactly when the first two coordinates are conditionally independent given the third.line 615
LeanInfoTheory.Shannon.condEntropyOf_pair_eq_add_condEntropyOf_iff_isCondIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceConditional joint entropy of finite-valued random variables is additive exactly under conditional independence.line 634
LeanInfoTheory.Shannon.condEntropy_pair_additive_iff_isCondIndependentTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceShort PMF alias for conditional joint-entropy additivity.line 654
LeanInfoTheory.Shannon.condEntropyOf_pair_additive_iff_isCondIndependentOfTheoremLeanInfoTheory.Shannon.SemanticBridge.IndependenceShort random-variable alias for conditional joint-entropy additivity.line 664
LeanInfoTheory.Shannon.toMeasure_absolutelyContinuous_iff_support_subsetTheoremLeanInfoTheory.Shannon.SemanticBridge.KLAbsolute continuity between PMF measures is exactly inclusion of their set-valued supports. This statement does not require a finite alphabet: measurable singletons let the forward direction test individual atoms, while the reverse direction uses the PMF measure's zero-set characterization.line 63
LeanInfoTheory.Shannon.klDiv_pmf_ne_top_iff_support_subsetTheoremLeanInfoTheory.Shannon.SemanticBridge.KLOn a finite alphabet, PMF KL divergence is finite exactly when the first PMF's support is contained in the second PMF's support.line 89
LeanInfoTheory.Shannon.klDiv_pmf_eq_top_iff_not_support_subsetTheoremLeanInfoTheory.Shannon.SemanticBridge.KLOn a finite alphabet, PMF KL divergence is infinite exactly when support inclusion fails.line 108
LeanInfoTheory.Shannon.klDiv_pmf_eq_zero_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.KLKL divergence between two PMFs is zero exactly when the PMFs are equal. The alphabet need not be finite: PMF measures are finite measures, and measurable singletons make `PMF.toMeasure` injective.line 127
LeanInfoTheory.Shannon.toReal_klDiv_pmf_eq_zero_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.KLOn a finite alphabet and under support inclusion, real-valued PMF KL divergence is zero exactly when the PMFs are equal. The support hypothesis is essential: without KL finiteness, `ENNReal.toReal ⊤ = 0` would make the reverse characterization false.line 140
LeanInfoTheory.Shannon.toMeasure_withDensity_pmf_divTheoremLeanInfoTheory.Shannon.SemanticBridge.KLCountable PMF density formula. If `p.toMeasure ≪ q.toMeasure`, then `p.toMeasure` is obtained from `q.toMeasure` by the density `a ↦ p(a) / q(a)`. On atoms with `q(a)=0`, absolute continuity forces `p(a)=0`, so the formula is still valid.line 163
LeanInfoTheory.Shannon.toReal_klDiv_pmf_eq_sumTheoremLeanInfoTheory.Shannon.SemanticBridge.KLFinite KL expansion for absolutely continuous PMFs: `D(P || Q) = sum_a p(a) log (p(a) / q(a))`. The left-hand side is mathlib's measure-theoretic KL divergence applied to `PMF.toMeasure`; the right-hand side is the usual finite sum over atoms.line 194
LeanInfoTheory.Shannon.toReal_klDiv_pmf_uniformOfFinsetTheoremLeanInfoTheory.Shannon.SemanticBridge.KLKL divergence from a finite PMF to the uniform law on a nonempty finset is the uniform log-cardinality minus entropy, provided the PMF is supported on that finset: `D(P || U_s) = log |s| - H(P)`.line 233
LeanInfoTheory.Shannon.toReal_klDiv_pmf_uniformOfFintypeTheoremLeanInfoTheory.Shannon.SemanticBridge.KLFull-alphabet form of `toReal_klDiv_pmf_uniformOfFinset`: `D(P || U_alpha) = log |alpha| - H(P)`.line 277
LeanInfoTheory.Shannon.mutualInfo_eq_toReal_klDiv_joint_indepProdTheoremLeanInfoTheory.Shannon.SemanticBridge.KLSemantic bridge for finite mutual information: `I(A;B) = D(P_AB || P_A × P_B)`. Here `P_A × P_B` is represented by the finite independent-product PMF `indepProd (fstMarginal p) (sndMarginal p)`. This theorem is the finite textbook identity connecting the entropy definition of mutual information to mathlib's measure-theoretic KL divergence.line 298
LeanInfoTheory.Shannon.mutualInfo_eq_toReal_klDiv_joint_prod_marginalsTheoremLeanInfoTheory.Shannon.SemanticBridge.KLProduct-measure form of the finite mutual-information KL bridge: `I(A;B) = D(P_AB || P_A.toMeasure.prod P_B.toMeasure)`.line 322
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThirdKLDefinitionLeanInfoTheory.Shannon.SemanticBridge.KLFiberwise KL form of conditional mutual information. This is zero on zero-marginal third-coordinate atoms. On nonzero atoms it is `D(P_{A,B|C=c} || P_{A|C=c} × P_{B|C=c})`, using the marginals of the conditional joint law.line 343
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThird_eq_KLTheoremLeanInfoTheory.Shannon.SemanticBridge.KLThe fiber mutual-information helper agrees with the fiberwise KL expression `D(P_{A,B|C=c} || P_{A|C=c} × P_{B|C=c})`.line 360
LeanInfoTheory.Shannon.condMutualInfo_eq_sum_thirdMarginal_mul_condMutualInfoFstSndGivenThirdKLTheoremLeanInfoTheory.Shannon.SemanticBridge.KLAveraged conditional-KL bridge for finite conditional mutual information: `I(A;B | C) = sum_c P_C(c) D(P_{A,B|C=c} || P_{A|C=c} × P_{B|C=c})`. Zero-marginal `c` contribute zero by definition of `condMutualInfoFstSndGivenThirdKL`.line 384
LeanInfoTheory.Shannon.IsMarkovChainOfDefinitionLeanInfoTheory.Shannon.SemanticBridge.MarkovRandom variables `X`, `Y`, and `Z` form the Markov chain `X → Y → Z` when `X` and `Z` are conditionally independent given `Y`.line 49
LeanInfoTheory.Shannon.IsMarkovChainDefinitionLeanInfoTheory.Shannon.SemanticBridge.MarkovA triple PMF is a Markov chain in its first-to-second-to-third coordinate order.line 56
LeanInfoTheory.Shannon.isMarkovChain_iff_crossProductTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovA triple law is Markov in coordinate order exactly when every atom satisfies the cross-product factorization `p(a,b,c) * p_B(b) = p_AB(a,b) * p_BC(b,c)`. The identity also covers null middle-coordinate fibers, so it requires no finite-alphabet or measurable-space assumptions.line 72
LeanInfoTheory.Shannon.isMarkovChain_iff_isIndependent_condFstSndGivenThirdTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovA triple law is Markov exactly when its two endpoint coordinates are independent in every positive-mass conditional fiber of the middle coordinate. The displayed mapped law orders the coordinates as endpoint, endpoint, middle so that it can reuse `condFstSndGivenThird` directly.line 137
LeanInfoTheory.Shannon.isMarkovChain_iff_fiberwise_endpoints_independentTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovTextbook-facing alias for the positive-fiber Markov characterization.line 152
LeanInfoTheory.Shannon.condMutualInfoOf_eq_zero_iff_isMarkovChainOfTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovThe Markov condition `X → Y → Z` is equivalent to the textbook zero-CMI identity `I(X;Z | Y) = 0`.line 168
LeanInfoTheory.Shannon.isMarkovChainOf_reverseTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovReversing a Markov chain preserves the random-variable Markov condition.line 178
LeanInfoTheory.Shannon.isMarkovChain_map_reverseTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovReversing the coordinates of a triple law preserves its Markov condition.line 188
LeanInfoTheory.Shannon.condFstGivenSndChannelDefinitionLeanInfoTheory.Shannon.SemanticBridge.MarkovThe total channel from the second coordinate to the first associated with a joint PMF. For `P_B(b) != 0`, this is the canonical conditional law `P_{A | B=b}`. For a null fiber, it is the first marginal `P_A`. The fallback supplies a PMF without requiring an additional `Nonempty alpha` assumption; it has no intended conditional semantics and disappears from the weighted reconstruction laws.line 210
LeanInfoTheory.Shannon.condFstGivenSndChannel_of_sndMarginal_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovOn a null conditioning fiber, the total channel uses the documented fallback.line 222
LeanInfoTheory.Shannon.condFstGivenSndChannel_of_sndMarginal_ne_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovOn a positive conditioning fiber, the total channel is the canonical conditional PMF.line 229
LeanInfoTheory.Shannon.condFstGivenSndChannel_null_fiber_irrelevantTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovThe value chosen for a null conditional fiber is irrelevant after weighting by the conditioning marginal. The PMF `q` represents any alternative fallback.line 239
LeanInfoTheory.Shannon.sndMarginal_mul_condFstGivenSndChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovThe conditioning marginal times the total conditional-channel mass reconstructs the original joint mass on every fiber, including null fibers.line 251
LeanInfoTheory.Shannon.channelJoint_condFstGivenSndChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovSampling the total conditional channel from the second marginal reconstructs the original pair law with its coordinates in channel input-output order.line 265
LeanInfoTheory.Shannon.isMarkovChain_channelExtensionTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovExtending any pair law of `(A,B)` by sampling `C` from a channel depending only on `B` produces the Markov chain `A → B → C`. The result is type-generic and includes null middle-coordinate fibers through the cross-product characterization, without requiring a conditional PMF.line 285
LeanInfoTheory.Shannon.isMarkovChainOf_compTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovDeterministic post-processing of the middle variable always gives the forward Markov chain `X → Y → f(Y)`. Equivalently, `X` and `f(Y)` are conditionally independent given `Y`: `X ⟂ f(Y) | Y`.line 308
LeanInfoTheory.Shannon.isMarkovChain_iff_eq_channelExtension_condFstGivenSndChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovA finite triple law is Markov exactly when its first-two marginal, extended by the total conditional channel `P_{C | B}` extracted from its second-third marginal, reconstructs the original law. The second-third marginal is swapped into `(C,B)` order because `condFstGivenSndChannel` constructs a channel from the second coordinate to the first. Its documented null-fiber fallback is irrelevant: both the original and reconstructed atom masses vanish whenever the middle marginal does.line 338
LeanInfoTheory.Shannon.isMarkovChain_iff_canonical_channelExtensionTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovCompatibility alias for reconstruction by the canonical total conditional channel.line 411
LeanInfoTheory.Shannon.isMarkovChain_iff_exists_channelExtensionTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovTextbook channel-factorization characterization of a finite Markov triple: a law is Markov exactly when some channel from the middle alphabet extends its first-two marginal to the original triple law.line 425
LeanInfoTheory.Shannon.mutualInfo_markov_chain_ruleTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovExact mutual-information loss along a finite Markov triple: `I(A;B) = I(A;C) + I(A;B | C)`. This is the PMF form of the Markov chain rule. The Markov hypothesis removes the opposite conditional term `I(A;C | B)` from the ordinary chain rule.line 452
LeanInfoTheory.Shannon.mutualInfoOf_markov_chain_ruleTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovExact mutual-information loss along the finite Markov chain `X → Y → Z`: `I(X;Y) = I(X;Z) + I(X;Y | Z)`.line 475
LeanInfoTheory.Shannon.mutualInfo_dataProcessingTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovMutual-information data processing for a finite Markov triple: `I(A;C) <= I(A;B)` when `A -> B -> C`.line 498
LeanInfoTheory.Shannon.mutualInfoOf_dataProcessingTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovRandom-variable mutual-information data processing: `I(X;Z) <= I(X;Y)` when `X -> Y -> Z`.line 511
LeanInfoTheory.Shannon.condEntropyOf_dataProcessingTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovConditional-entropy form of data processing: `H(X|Y) <= H(X|Z)` when `X -> Y -> Z`.line 525
LeanInfoTheory.Shannon.condEntropy_dataProcessingTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovPMF form of the conditional-entropy data-processing consequence: `H(A|B) <= H(A|C)` when `A -> B -> C`.line 544
LeanInfoTheory.Shannon.mutualInfoOf_dataProcessing_eq_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovEquality in mutual-information data processing holds exactly when the reverse chain `X -> Z -> Y` is also Markov.line 557
LeanInfoTheory.Shannon.mutualInfo_dataProcessing_eq_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovFor a Markov triple law, equality in mutual-information data processing holds exactly when its first, third, and second coordinate variables form the reverse Markov chain.line 581
LeanInfoTheory.Shannon.condEntropyOf_dataProcessing_eq_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovUnder the forward chain `X -> Y -> Z`, equality in conditional-entropy data processing holds exactly when the reverse chain `X -> Z -> Y` is also Markov. Equivalently, `X` and `Y` are conditionally independent given `Z`, `X ⟂ Y | Z`; in this sense, `Z` retains all information about `X` carried by `Y`.line 599
LeanInfoTheory.Shannon.condEntropy_dataProcessing_eq_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovFor a Markov triple law, equality in conditional-entropy data processing holds exactly when its first, third, and second coordinate variables form the reverse Markov chain.line 617
LeanInfoTheory.Shannon.mutualInfo_channel_right_leTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovApplying a channel to the right coordinate of a finite joint law cannot increase mutual information.line 634
LeanInfoTheory.Shannon.mutualInfo_channel_left_leTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovApplying a channel to the left coordinate of a finite joint law cannot increase mutual information. The displayed bind is the law of the processed left output paired with the unchanged right coordinate.line 664
LeanInfoTheory.Shannon.mutualInfo_independent_channels_leTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovApplying independent channels to both coordinates of a finite joint law cannot increase mutual information. Conditional on an input pair `(a,b)`, the two channel outputs have law `indepProd (W a) (V b)`.line 706
LeanInfoTheory.Shannon.mutualInfo_channelComp_leTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovMutual information contracts along a two-stage finite channel cascade.line 725
LeanInfoTheory.Shannon.mutualInfo_channel_cascade_leTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovTextbook-facing alias for mutual-information contraction along a channel cascade.line 735
LeanInfoTheory.Shannon.mutualInfo_channel_map_output_leTheoremLeanInfoTheory.Shannon.SemanticBridge.MarkovDeterministically mapping every output law of a finite channel cannot increase its input-output mutual information.line 747
LeanInfoTheory.Shannon.indepProdDefinitionLeanInfoTheory.Shannon.SemanticBridge.ProductIndependent product of two probability mass functions. Mathematically, this is the law of `(X, Y)` when `X` has law `p`, `Y` has law `q`, and the two variables are independent.line 44
LeanInfoTheory.Shannon.indepProd_applyTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductThe atom mass of an independent product is the product of the two atom masses.line 68
LeanInfoTheory.Shannon.indepProd_apply_eq_zero_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductAn atom of the independent product has zero mass exactly when one of the two coordinate atoms has zero mass.line 83
LeanInfoTheory.Shannon.indepProd_apply_ne_zero_iffTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductAn atom belongs to the independent product support exactly when both coordinate atoms belong to the corresponding supports.line 93
LeanInfoTheory.Shannon.support_indepProdTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductThe support of an independent product is the product of the two supports.line 100
LeanInfoTheory.Shannon.fstMarginal_indepProdTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductThe first marginal of an independent product is the first factor law.line 109
LeanInfoTheory.Shannon.sndMarginal_indepProdTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductThe second marginal of an independent product is the second factor law.line 126
LeanInfoTheory.Shannon.indepProd_map_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductSwapping the coordinates of an independent product swaps the two factor laws.line 144
LeanInfoTheory.Shannon.indepProd_toMeasure_prodTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductThe independent product law assigns product rectangles the product of the factor probabilities.line 164
LeanInfoTheory.Shannon.indepProd_toMeasureTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductThe measure associated to the independent product PMF is the product of the two associated measures.line 213
LeanInfoTheory.Shannon.joint_toMeasure_absolutelyContinuous_indepProd_marginalsTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductA finite joint PMF is absolutely continuous with respect to the independent product of its two marginals. Mathematically, if the product of the marginal masses of `(a, b)` is zero, then one marginal atom is zero, hence the joint atom `p (a, b)` is zero. This is the support fact needed before comparing finite mutual information with KL divergence from the joint law to the product of its marginals.line 234
LeanInfoTheory.Shannon.joint_toMeasure_absolutelyContinuous_prod_marginalsTheoremLeanInfoTheory.Shannon.SemanticBridge.ProductProduct-measure version of `joint_toMeasure_absolutelyContinuous_indepProd_marginals`. This is the form expected by KL-divergence statements that use `Measure.prod` directly.line 269
LeanInfoTheory.Shannon.statisticTripleLawOfDefinitionLeanInfoTheory.Shannon.SemanticBridge.SufficiencyThe induced law of `(Theta, T(X), X)`. The `(parameter, statistic, observation)` coordinate order is intentional: it puts the statistic beside the parameter before the observation is reconstructed by a channel from statistic values, matching the recovery and channel factorization statements below.line 48
LeanInfoTheory.Shannon.IsSufficientStatisticOfDefinitionLeanInfoTheory.Shannon.SemanticBridge.SufficiencyUnder the fixed source law `p`, `T` is sufficient for `Theta` based on `X` when the reverse chain `Theta -> T(X) -> X` is Markov; equivalently, `Theta` and `X` are conditionally independent given `T(X)`. This is a fixed-law (or fixed-prior) predicate. The family-level `IsSufficientStatistic` below instead asks for one recovery channel that works for every model parameter, independently of a chosen prior.line 62
LeanInfoTheory.Shannon.isSufficientStatisticOf_iff_isMarkovChainOfTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFixed-prior sufficiency is exactly the reverse Markov condition.line 81
LeanInfoTheory.Shannon.isSufficientStatisticOf_iff_condMutualInfoOf_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyA finite-valued statistic is sufficient exactly when the parameter and the observation have zero conditional mutual information given the statistic.line 93
LeanInfoTheory.Shannon.isSufficientStatisticOf_iff_mutualInfoOf_eqTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyA finite-valued statistic is sufficient exactly when it preserves the mutual information between the parameter and the observation under the fixed law.line 108
LeanInfoTheory.Shannon.isSufficientStatisticOf_iff_condEntropyOf_eqTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyA finite-valued statistic is sufficient exactly when conditioning on it leaves the same parameter uncertainty as conditioning on the full observation.line 127
LeanInfoTheory.Shannon.isSufficientStatisticOf_iff_exists_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyA fixed-prior statistic is sufficient exactly when one channel from statistic values back to observations reconstructs the complete `(parameter, statistic, observation)` law. The same channel is used for every parameter value, and its behavior on a null statistic fiber is irrelevant.line 184
LeanInfoTheory.Shannon.exists_marginal_recovery_of_isSufficientStatisticOfTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencySufficiency implies that the observation marginal can be recovered from the statistic marginal. This is only a one-way consequence: marginal recovery by itself does not characterize sufficiency.line 216
LeanInfoTheory.Shannon.IsSufficientChannelDefinitionLeanInfoTheory.Shannon.SemanticBridge.SufficiencyA channel is sufficient for a model family when one recovery channel, shared by every parameter value, reconstructs each complete output-input joint law.line 267
LeanInfoTheory.Shannon.IsSufficientStatisticDefinitionLeanInfoTheory.Shannon.SemanticBridge.SufficiencyA deterministic statistic is sufficient for a model family when its induced deterministic channel is sufficient for that family.line 278
LeanInfoTheory.Shannon.isSufficientStatistic_idTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyThe identity statistic is sufficient for every model family.line 284
LeanInfoTheory.Shannon.isMarkovChainOf_of_isSufficientChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFor every parameter prior, a sufficient family channel gives the reverse Markov chain `parameter -> output -> input` in the generated experiment law.line 367
LeanInfoTheory.Shannon.condMutualInfo_eq_zero_of_isSufficientChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFor every finite parameter prior, sufficiency makes the parameter and input conditionally independent given the channel output.line 392
LeanInfoTheory.Shannon.mutualInfo_eq_of_isSufficientChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFor every finite parameter prior, a sufficient family channel preserves the mutual information between the parameter and the model observation.line 420
LeanInfoTheory.Shannon.condEntropy_eq_of_isSufficientChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFor every finite parameter prior, conditioning the parameter on a sufficient channel output leaves the same uncertainty as conditioning on the model input.line 443
LeanInfoTheory.Shannon.isSufficientChannel_iff_isMarkovChainOf_of_support_eq_univTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFor a prior supported on every parameter value, family sufficiency is equivalent to the reverse Markov condition in the generated experiment law. Only the model-input alphabet must be finite.line 481
LeanInfoTheory.Shannon.isSufficientChannel_iff_forall_isMarkovChainOfTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyOn a finite nonempty parameter alphabet, a family channel is sufficient exactly when it gives the reverse Markov chain for every parameter prior.line 565
LeanInfoTheory.Shannon.isSufficientStatistic_iff_isSufficientStatisticOf_of_support_eq_univTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFor a prior supported on every parameter value, family sufficiency of a deterministic statistic is equivalent to its fixed-prior sufficiency.line 604
LeanInfoTheory.Shannon.isSufficientStatistic_iff_forall_isSufficientStatisticOfTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyOn a finite nonempty parameter alphabet, a deterministic statistic is sufficient for a model family exactly when it is sufficient under every prior.line 620
LeanInfoTheory.Shannon.isSufficientStatistic_iff_exists_fisherNeymanFactorizationTheoremLeanInfoTheory.Shannon.SemanticBridge.SufficiencyFinite Fisher-Neyman factorization theorem for deterministic statistics. A statistic is sufficient for a model family exactly when every model mass factors through the statistic into a parameter-dependent factor `g` and one parameter-independent factor `h`. Pointwise finiteness of `h` makes each finite fiber mass `sum_{a : T a = b} h a` finite and permits normalization on a positive fiber. Pointwise finiteness of `g` separately excludes pathological top-valued witnesses and matches the canonical forward witness `g t b = (model t).map T b`; it is not the hypothesis used to normalize the recovery row.line 720
LeanInfoTheory.Shannon.klDiv_channel_eq_of_common_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLIf one channel exactly recovers the complete output-input joint law for each of two input laws, then the forward channel preserves their `ENNReal` KL divergence. No support inclusion is needed: data processing through the forward and recovery channels gives the two inequalities even when either divergence is infinite.line 62
LeanInfoTheory.Shannon.klDiv_channel_eq_iff_exists_common_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLUnder input support inclusion, equality in finite `ENNReal` KL data processing holds exactly when one channel recovers both complete output-input joint laws. The support hypothesis is needed only for the converse: it excludes the uninformative case where both KL divergences are `⊤`. The recovery-to-equality direction is the unconditional theorem above.line 93
LeanInfoTheory.Shannon.toReal_klDiv_channel_eq_iff_exists_common_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLThe real-valued finite KL equality case has the same common exact-recovery characterization under input support inclusion.line 129
LeanInfoTheory.Shannon.klDiv_map_eq_iff_exists_common_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLUnder input support inclusion, a deterministic statistic preserves `ENNReal` KL divergence exactly when one channel recovers both input-statistic graph laws from their statistic marginals.line 166
LeanInfoTheory.Shannon.toReal_klDiv_map_eq_iff_exists_common_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLThe real-valued deterministic-statistic equality case has the same common exact-recovery characterization under input support inclusion.line 189
LeanInfoTheory.Shannon.klDiv_eq_of_isSufficientChannelTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLA sufficient channel preserves `ENNReal` KL divergence between every pair of laws in the model family. The family sufficiency hypothesis already supplies one recovery channel shared by all parameter values, so no support inclusion is needed, even when the divergence is infinite.line 218
LeanInfoTheory.Shannon.klDiv_eq_of_isSufficientStatisticTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLA sufficient deterministic statistic preserves `ENNReal` KL divergence between every pair of laws in the model family.line 236
LeanInfoTheory.Shannon.isSufficientChannel_iff_klDiv_eq_boolTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLFor a Boolean-indexed model whose `false` law is supported within its `true` law, channel sufficiency is equivalent to preservation of their directed `ENNReal` KL divergence. The binary index is substantive: the guarded equality produces one recovery channel for these two laws, which therefore recovers every law in this family. No analogous converse for unrelated pairwise witnesses in a larger family is claimed.line 262
LeanInfoTheory.Shannon.isSufficientStatistic_iff_klDiv_eq_boolTheoremLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLFor a guarded Boolean-indexed model, a deterministic statistic is sufficient exactly when it preserves the directed `ENNReal` KL divergence from the `false` law to the `true` law.line 293
LeanInfoTheory.Shannon.mutualInfo_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsMutual information is nonnegative: `0 <= I(A;B)`. The proof passes through the semantic bridge `I(A;B) = D(P_AB || P_A x P_B)` and then uses nonnegativity of the real coercion of an `ENNReal` KL divergence.line 61
LeanInfoTheory.Shannon.condEntropyFstGivenSnd_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsFiber conditional entropy is nonnegative: `0 <= H(A | B=b)`. On zero-mass fibers this is `0 <= 0`; on nonzero fibers it reduces to entropy nonnegativity for the conditional law `P_{A|B=b}`.line 77
LeanInfoTheory.Shannon.condEntropyFstGivenSnd_eq_zero_iff_of_sndMarginal_ne_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsOn a nonzero conditioning fiber, conditional entropy is zero exactly when the canonical conditional PMF is pure.line 90
LeanInfoTheory.Shannon.condEntropy_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional entropy is nonnegative: `0 <= H(A | B)`. The proof uses the finite semantic bridge `H(A | B) = sum_b P_B(b) * H(P_{A|B=b})`, then every summand is nonnegative.line 110
LeanInfoTheory.Shannon.condEntropyOf_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional entropy of finite-valued random variables is nonnegative.line 119
LeanInfoTheory.Shannon.condEntropy_eq_zero_iff_exists_functionTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional entropy is zero exactly when the first coordinate is a function of the second coordinate on the support of the joint PMF.line 132
LeanInfoTheory.Shannon.condEntropyOf_eq_zero_iff_exists_functionTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional entropy of finite-valued random variables is zero exactly when the first variable is a function of the second on the source PMF support.line 222
LeanInfoTheory.Shannon.condEntropyOf_comp_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsA deterministic function of `Y` has zero conditional entropy given `Y`.line 251
LeanInfoTheory.Shannon.condEntropyOf_self_eq_zeroTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsA finite-valued random variable has zero conditional entropy given itself.line 261
LeanInfoTheory.Shannon.entropy_eq_entropy_sndMarginal_iff_exists_functionTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsJoint entropy equals the entropy of the second marginal exactly when the first coordinate is a function of the second on the joint support.line 273
LeanInfoTheory.Shannon.jointEntropyOf_eq_entropyOf_iff_exists_functionTheoremLeanInfoTheory.Shannon.SemanticBridge.Theorems`H(X,Y) = H(Y)` exactly when `X` is a function of `Y` on the source PMF support.line 299
LeanInfoTheory.Shannon.entropy_map_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsApplying a deterministic map to a finite PMF cannot increase entropy.line 341
LeanInfoTheory.Shannon.entropy_map_eq_iff_injOn_supportTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsApplying a deterministic map preserves entropy exactly when it is injective on the support of the source PMF.line 354
LeanInfoTheory.Shannon.entropyOf_comp_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing of a finite-valued variable cannot increase entropy.line 381
LeanInfoTheory.Shannon.entropyOf_comp_eq_iff_injOn_supportTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing preserves random-variable entropy exactly when the map is injective on the support of the law of the original variable.line 393
LeanInfoTheory.Shannon.condEntropyOf_deterministic_chain_ruleTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional deterministic chain rule: `H(X|Z) = H(f(X)|Z) + H(X|f(X),Z)`.line 406
LeanInfoTheory.Shannon.condEntropyOf_comp_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing cannot increase conditional entropy.line 438
LeanInfoTheory.Shannon.condEntropyOf_comp_eq_iff_exists_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing preserves conditional entropy exactly when `X` is recoverable from `(f(X), Z)` on the source PMF support.line 453
LeanInfoTheory.Shannon.condEntropy_map_fst_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsApplying a deterministic map to the first coordinate cannot increase `H(A|C)`.line 478
LeanInfoTheory.Shannon.condEntropy_map_fst_eq_iff_exists_recoveryTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsThe first-coordinate map preserves `H(A|C)` exactly when `A` is recoverable from `(f(A), C)` on the joint support.line 497
LeanInfoTheory.Shannon.condEntropy_le_entropy_fstMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditioning reduces entropy: `H(A|B) <= H(A)`.line 517
LeanInfoTheory.Shannon.mutualInfo_le_entropy_fstMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsMutual information is at most the entropy of the first marginal.line 526
LeanInfoTheory.Shannon.mutualInfo_le_entropy_sndMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsMutual information is at most the entropy of the second marginal.line 537
LeanInfoTheory.Shannon.entropy_fstMarginal_le_entropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsThe entropy of the first marginal is at most the joint entropy.line 549
LeanInfoTheory.Shannon.entropy_sndMarginal_le_entropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsThe entropy of the second marginal is at most the joint entropy.line 561
LeanInfoTheory.Shannon.entropy_le_entropy_fstMarginal_add_entropy_sndMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsJoint entropy is subadditive: `H(A,B) <= H(A) + H(B)`.line 572
LeanInfoTheory.Shannon.condEntropyOf_le_entropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable conditioning reduces entropy: `H(X|Y) <= H(X)`.line 581
LeanInfoTheory.Shannon.mutualInfoOf_le_entropyOf_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable mutual information is at most `H(X)`.line 591
LeanInfoTheory.Shannon.mutualInfoOf_le_entropyOf_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable mutual information is at most `H(Y)`.line 601
LeanInfoTheory.Shannon.entropyOf_le_jointEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsThe entropy of `X` is at most the joint entropy `H(X,Y)`.line 611
LeanInfoTheory.Shannon.entropyOf_le_jointEntropyOf_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsThe entropy of `Y` is at most the joint entropy `H(X,Y)`.line 621
LeanInfoTheory.Shannon.jointEntropyOf_le_entropyOf_add_entropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable joint entropy is subadditive: `H(X,Y) <= H(X) + H(Y)`.line 631
LeanInfoTheory.Shannon.condEntropy_le_entropy_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `H(A|B) <= H(A)`.line 643
LeanInfoTheory.Shannon.mutualInfo_le_entropy_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `I(A;B) <= H(A)`.line 650
LeanInfoTheory.Shannon.mutualInfo_le_entropy_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `I(A;B) <= H(B)`.line 657
LeanInfoTheory.Shannon.entropy_left_le_jointEntropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `H(A) <= H(A,B)`.line 664
LeanInfoTheory.Shannon.entropy_right_le_jointEntropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `H(B) <= H(A,B)`.line 671
LeanInfoTheory.Shannon.jointEntropy_le_add_marginalEntropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for joint-entropy subadditivity.line 678
LeanInfoTheory.Shannon.entropyOf_left_le_jointEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsLeft-oriented alias for `H(X) <= H(X,Y)`.line 685
LeanInfoTheory.Shannon.entropyOf_right_le_jointEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRight-oriented alias for `H(Y) <= H(X,Y)`.line 693
LeanInfoTheory.Shannon.jointEntropyOf_le_add_entropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsShort random-variable alias for joint-entropy subadditivity.line 701
LeanInfoTheory.Shannon.condMutualInfoFstSndGivenThird_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsFiber conditional mutual information is nonnegative: `0 <= I(A;B | C=c)`. On zero-mass fibers this is `0 <= 0`; on nonzero fibers it reduces to `mutualInfo_nonneg` applied to the conditional joint law `P_{A,B|C=c}`.line 718
LeanInfoTheory.Shannon.condMutualInfo_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional mutual information is nonnegative: `0 <= I(A;B | C)`. We use the finite semantic bridge `I(A;B | C) = sum_c P_C(c) * I(A;B | C=c)`, then each summand is nonnegative because both `P_C(c)` and the fiber mutual information are nonnegative.line 740
LeanInfoTheory.Shannon.condMutualInfoOf_nonnegTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional mutual information of finite-valued random variables is nonnegative.line 751
LeanInfoTheory.Shannon.fstMarginal_fstThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTaking the first marginal after projecting `(A,B,C)` to `(A,C)` recovers the first marginal of the original law: `(P_AC)_A = P_A`.line 767
LeanInfoTheory.Shannon.sndMarginal_eq_sndThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsViewing a triple law as a joint law of `A` and `(B,C)`, the second marginal is the same law as the explicit `(B,C)` marginal: `P_{B,C} = sndMarginal P_{A,(B,C)}`.line 780
LeanInfoTheory.Shannon.mutualInfo_chain_rule_fstTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsFirst mutual-information chain rule: `I(A;B,C) = I(A;C) + I(A;B | C)`. In Lean's right-associated product convention, a PMF `p : PMF (alpha × beta × gamma)` is also a joint law of `A` and `(B,C)`, so `mutualInfo p` denotes `I(A;B,C)`.line 797
LeanInfoTheory.Shannon.mutualInfo_chain_rule_sndTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsSecond mutual-information chain-rule variant: `I(A;B,C) = I(A;B) + I(A;C | B)`.line 812
LeanInfoTheory.Shannon.mutualInfoOf_chain_rule_fstTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable form of `mutualInfo_chain_rule_fst`: `I(X;Y,Z) = I(X;Z) + I(X;Y | Z)`.line 853
LeanInfoTheory.Shannon.mutualInfoOf_chain_rule_sndTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable form of `mutualInfo_chain_rule_snd`: `I(X;Y,Z) = I(X;Y) + I(X;Z | Y)`.line 867
LeanInfoTheory.Shannon.mutualInfoOf_deterministic_chain_rule_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic mutual-information chain rule: `I(X;Y) = I(f(X);Y) + I(X;Y | f(X))`.line 928
LeanInfoTheory.Shannon.mutualInfoOf_comp_left_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing of the left variable cannot increase mutual information.line 949
LeanInfoTheory.Shannon.mutualInfoOf_comp_right_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing of the right variable cannot increase mutual information.line 960
LeanInfoTheory.Shannon.mutualInfoOf_comp_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsDeterministic post-processing of both variables cannot increase mutual information.line 974
LeanInfoTheory.Shannon.mutualInfo_map_fst_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsMapping the first coordinate of a joint PMF cannot increase mutual information.line 989
LeanInfoTheory.Shannon.mutualInfo_map_snd_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsMapping the second coordinate of a joint PMF cannot increase mutual information.line 1005
LeanInfoTheory.Shannon.mutualInfo_map_prod_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsMapping both coordinates of a joint PMF cannot increase mutual information.line 1021
LeanInfoTheory.Shannon.mutualInfoOf_comp_both_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsExplicitly two-sided alias for deterministic mutual-information processing.line 1039
LeanInfoTheory.Shannon.mutualInfo_map_left_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsLeft-coordinate alias for deterministic processing of a joint PMF.line 1050
LeanInfoTheory.Shannon.mutualInfo_map_right_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRight-coordinate alias for deterministic processing of a joint PMF.line 1058
LeanInfoTheory.Shannon.mutualInfo_map_both_leTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsBoth-coordinate alias for deterministic processing of a joint PMF.line 1066
LeanInfoTheory.Shannon.condMutualInfo_eq_condEntropy_fstThirdMarginal_sub_condEntropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional mutual information as a difference of conditional entropies: `I(A;B | C) = H(A | C) - H(A | B,C)`.line 1080
LeanInfoTheory.Shannon.condMutualInfo_eq_condEntropy_sndThirdMarginal_sub_condEntropy_swap12TheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsSymmetric conditional-entropy difference form: `I(A;B | C) = H(B | C) - H(B | A,C)`.line 1093
LeanInfoTheory.Shannon.condEntropy_le_condEntropy_fstThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditioning reduces entropy: `H(A | B,C) <= H(A | C)`. The proof rewrites the difference as `I(A;B | C)` and uses conditional mutual information nonnegativity.line 1112
LeanInfoTheory.Shannon.condEntropyOf_pair_le_condEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable conditioning-reduces-entropy theorem: `H(X | Y,Z) <= H(X | Z)`.line 1126
LeanInfoTheory.Shannon.condMutualInfo_le_condEntropy_fstThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional mutual information is at most `H(A|C)`.line 1138
LeanInfoTheory.Shannon.condMutualInfo_le_condEntropy_sndThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional mutual information is at most `H(B|C)`.line 1150
LeanInfoTheory.Shannon.condEntropy_fstThirdMarginal_le_condEntropy_pairThirdLawTheoremLeanInfoTheory.Shannon.SemanticBridge.Theorems`H(A|C)` is at most the conditional joint entropy `H(A,B|C)`.line 1166
LeanInfoTheory.Shannon.condEntropy_sndThirdMarginal_le_condEntropy_pairThirdLawTheoremLeanInfoTheory.Shannon.SemanticBridge.Theorems`H(B|C)` is at most the conditional joint entropy `H(A,B|C)`.line 1182
LeanInfoTheory.Shannon.condEntropy_pairThirdLaw_le_condEntropy_fstThirdMarginal_add_condEntropy_sndThirdMarginalTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsConditional joint entropy is subadditive: `H(A,B|C) <= H(A|C) + H(B|C)`.line 1195
LeanInfoTheory.Shannon.condMutualInfoOf_le_condEntropyOf_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable conditional mutual information is at most `H(X|Z)`.line 1206
LeanInfoTheory.Shannon.condMutualInfoOf_le_condEntropyOf_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable conditional mutual information is at most `H(Y|Z)`.line 1221
LeanInfoTheory.Shannon.condEntropyOf_le_condEntropyOf_pairTheoremLeanInfoTheory.Shannon.SemanticBridge.Theorems`H(X|Z)` is at most the conditional joint entropy `H(X,Y|Z)`.line 1236
LeanInfoTheory.Shannon.condEntropyOf_le_condEntropyOf_pair_swapTheoremLeanInfoTheory.Shannon.SemanticBridge.Theorems`H(Y|Z)` is at most the conditional joint entropy `H(X,Y|Z)`.line 1252
LeanInfoTheory.Shannon.condEntropyOf_pair_le_condEntropyOf_add_condEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRandom-variable conditional joint entropy is subadditive.line 1268
LeanInfoTheory.Shannon.condMutualInfo_le_condEntropy_leftTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `I(A;B|C) <= H(A|C)`.line 1282
LeanInfoTheory.Shannon.condMutualInfo_le_condEntropy_rightTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsTextbook-facing PMF alias for `I(A;B|C) <= H(B|C)`.line 1290
LeanInfoTheory.Shannon.condEntropy_left_le_condEntropy_pairTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsLeft-oriented PMF alias for `H(A|C) <= H(A,B|C)`.line 1298
LeanInfoTheory.Shannon.condEntropy_right_le_condEntropy_pairTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRight-oriented PMF alias for `H(B|C) <= H(A,B|C)`.line 1306
LeanInfoTheory.Shannon.condEntropy_pair_le_add_condEntropyTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsShort PMF alias for conditional joint-entropy subadditivity.line 1314
LeanInfoTheory.Shannon.condEntropyOf_left_le_condEntropyOf_pairTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsLeft-oriented random-variable alias for `H(X|Z) <= H(X,Y|Z)`.line 1324
LeanInfoTheory.Shannon.condEntropyOf_right_le_condEntropyOf_pairTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsRight-oriented random-variable alias for `H(Y|Z) <= H(X,Y|Z)`.line 1333
LeanInfoTheory.Shannon.condEntropyOf_pair_le_add_condEntropyOfTheoremLeanInfoTheory.Shannon.SemanticBridge.TheoremsShort random-variable alias for conditional joint-entropy subadditivity.line 1342
LeanInfoTheory.Shannon.natsToBaseDefinitionLeanInfoTheory.Shannon.UnitsConvert a real-valued quantity measured in nats to base-`b` information units. For the usual information-theoretic interpretation the base must satisfy `1 < b`. The definition itself is total because `Real.log` and real division are total in Lean.line 46
LeanInfoTheory.Shannon.natsToBitsDefinitionLeanInfoTheory.Shannon.UnitsConvert a real-valued quantity measured in nats to bits, namely `x / Real.log 2`.line 50
LeanInfoTheory.Shannon.div_log_change_baseTheoremLeanInfoTheory.Shannon.UnitsChange a real quantity from logarithm base `b` to logarithm base `c`. If `x` is measured in nats, then `x / Real.log b` is its value in base-`b` units. Thus the theorem is the usual change-of-base identity `x_c = log_c(b) * x_b`.line 60
LeanInfoTheory.Shannon.negMulLog_div_logTheoremLeanInfoTheory.Shannon.UnitsA `Real.negMulLog` summand in base-`b` units.line 66
LeanInfoTheory.Shannon.entropy_div_logTheoremLeanInfoTheory.Shannon.UnitsFinite PMF entropy converted from nats to base-`b` units is the usual `-sum_x p(x) log_b p(x)` formula.line 75
LeanInfoTheory.Shannon.entropyOf_div_logTheoremLeanInfoTheory.Shannon.UnitsFinite-valued random-variable entropy converted from nats to base-`b` units.line 87

The machine-readable declaration index is available as declaration_index.json.