InformationTheory

Modules

422

Declarations

4,584

Lean

4.31.0

Modules

• InformationTheory
• InformationTheory.AsymptoticAsymptotic / exponent framework
• InformationTheory.FanoFano's inequality: a mathlib-current core formalization
• InformationTheory.Fano.BinaryJensenFinite-Finset Jensen for Real.binEntropy, plus algebraic helpers
• InformationTheory.Fano.CondEntropy3-variable joint and conditional entropy: chain rule + deterministic collapse
• InformationTheory.Fano.CoreFano core proof: error indicator + chain-rule glue (Markov form)
• InformationTheory.Fano.DPIData processing inequality (deterministic post-processing)
• InformationTheory.Fano.EntropySingle-variable Shannon entropy
• InformationTheory.Fano.MeasureFano's inequality: measure-theoretic form
• InformationTheory.Meta.EntryPoint
• InformationTheory.Polymatroid.BasicPolymatroid
• InformationTheory.Probability.MixtureMixing two measures at a clamped weight
• InformationTheory.Probability.SingletonMassSingleton masses of a measure on a finite type
• InformationTheory.Probability.TwoSidedExtension2-sided stationary extension μ_ℤ
• InformationTheory.Probability.TwoSidedExtension.Backward
• InformationTheory.Probability.TwoSidedExtension.CondExpMeasurePreserving
• InformationTheory.Probability.TwoSidedExtension.Core
• InformationTheory.Probability.TwoSidedExtension.LogCondIntegral
• InformationTheory.Probability.TwoSidedExtension.PastBlockJointLaw
• InformationTheory.Shannon.AEP.BasicAEP — Asymptotic Equipartition Property
• InformationTheory.Shannon.AEP.Basic.Achievability
• InformationTheory.Shannon.AEP.Basic.Converse
• InformationTheory.Shannon.AEP.Basic.Core
• InformationTheory.Shannon.AEP.RateAEP — rate-uniform form (via Chebyshev)
• InformationTheory.Shannon.AWGN.AchievabilityAWGN channel coding theorem — achievability
• InformationTheory.Shannon.AWGN.AchievabilityAEPAWGN achievability — continuous AEP engine (Chebyshev concentration)
• InformationTheory.Shannon.AWGN.AchievabilityCodeExistenceAWGN achievability assembly
• InformationTheory.Shannon.AWGN.AchievabilityCodebookThe random Gaussian codebook
• InformationTheory.Shannon.AWGN.AchievabilityExpurgationExpurgation, power-constraint witness, and code extraction
• InformationTheory.Shannon.AWGN.AchievabilityTypicalDecoderJoint-typicality decoder and the random-coding union bound
• InformationTheory.Shannon.AWGN.BasicAWGN channel capacity
• InformationTheory.Shannon.AWGN.BindConvolutionAWGN bind/convolution bridge
• InformationTheory.Shannon.AWGN.CapacityConverseMaxentAWGN single-letter capacity converse (Gaussian max-entropy)
• InformationTheory.Shannon.AWGN.ChannelMeasurabilityAWGN kernel measurability
• InformationTheory.Shannon.AWGN.ContChannelMIDecompContinuous-channel mutual-information chain rule
• InformationTheory.Shannon.AWGN.ConverseAWGN channel coding theorem: the converse
• InformationTheory.Shannon.AWGN.ConverseCapacityBoundAWGN channel-coding converse — Gaussian capacity bound and assembly
• InformationTheory.Shannon.AWGN.ConverseMIChainRuleConverse-side shared lemmas: integrability, MI chain rule, Markov factorization
• InformationTheory.Shannon.AWGN.ConverseMIChainRule.BlockMIMemoryless MI chain rule: block MI decomposition
• InformationTheory.Shannon.AWGN.ConverseMIChainRule.MarkovDeterministic-encoder Markov factorization
• InformationTheory.Shannon.AWGN.ConverseMIChainRule.PerLetterIntegrabilityConverse-side per-letter log-density integrability
• InformationTheory.Shannon.AWGN.ConverseMIChainRule.PerLetterMIPer-letter MI decomposition and continuous MI chain rule
• InformationTheory.Shannon.AWGN.ConverseMutualInfoFinitenessAWGN channel-coding converse — mutual-information finiteness and chain
• InformationTheory.Shannon.AWGN.JointlyTypicalSetAWGN jointly typical set
• InformationTheory.Shannon.AWGN.KLCapacityAndAEPContinuous Gaussian AEP and per-letter / n-fold KL identities
• InformationTheory.Shannon.AWGN.MIBridgeAWGN channel mutual information closed form
• InformationTheory.Shannon.AWGN.MIClosedFormAWGN Gaussian-input MI closed form
• InformationTheory.Shannon.AWGN.MainAWGN channel coding theorem
• InformationTheory.Shannon.AWGN.MutualInfoBridgeAWGN output marginal is Gaussian
• InformationTheory.Shannon.AWGN.MutualInfoDecompositionAWGN mutual-information decomposition
• InformationTheory.Shannon.AWGN.PerCodewordPowerConstraintPer-codeword power constraint
• InformationTheory.Shannon.ArithmeticCodingArithmetic Coding / Shannon-Fano-Elias (Cover-Thomas)
• InformationTheory.Shannon.BackwardFiltrationBackward filtration and tail σ-algebra
• InformationTheory.Shannon.BackwardMartingaleBackward martingale convergence theorem
• InformationTheory.Shannon.BirkhoffErgodicBirkhoff individual ergodic theorem via Garsia's maximal ergodic inequality
• InformationTheory.Shannon.BlockwiseChannel.CapacityLimitBlockwise channel capacity: the asymptotic limit form
• InformationTheory.Shannon.BlockwiseChannel.DefinitionBlockwise channel + capacity definitions
• InformationTheory.Shannon.BlockwiseChannel.MemorylessCapacityMemoryless blockwise capacity: the per-n equality
• InformationTheory.Shannon.BoolLawThe two-point law and the cost of a small mixing weight
• InformationTheory.Shannon.BrascampLiebBrascamp–Lieb inequality (combinatorial form) and hypercube product projection bound
• InformationTheory.Shannon.BridgeBridge: mutual information (KL form) ↔ conditional entropy
• InformationTheory.Shannon.BroadcastChannel.AchievabilityBroadcast channel — superposition achievability (inner bound)
• InformationTheory.Shannon.BroadcastChannel.Achievability.AssemblyBroadcast channel — superposition random-coding assembly and the achievability theorems
• InformationTheory.Shannon.BroadcastChannel.Achievability.ErrorAnalysisBroadcast channel — per-receiver error analysis
• InformationTheory.Shannon.BroadcastChannel.Achievability.SetupBroadcast channel — superposition achievability setup and infrastructure
• InformationTheory.Shannon.BroadcastChannel.BasicBroadcast channel — primitive definitions
• InformationTheory.Shannon.BroadcastChannel.ClassesBroadcast channel — comparison classes of the two receivers
• InformationTheory.Shannon.BroadcastChannel.ConverseDegraded broadcast channel — converse (outer bound)
• InformationTheory.Shannon.BroadcastChannel.ConverseGatewayDegraded broadcast channel — converse single-letterization
• InformationTheory.Shannon.BroadcastChannel.DegradedFromCodeBroadcast channel — the degraded converse at the ambient of a code
• InformationTheory.Shannon.BroadcastChannel.Marton.AchievabilityMarton's inner bound — achievability
• InformationTheory.Shannon.BroadcastChannel.Marton.BasicRate region of Marton's inner bound
• InformationTheory.Shannon.BroadcastChannel.Marton.CoveringMarton's mutual covering lemma
• InformationTheory.Shannon.BroadcastChannel.Marton.ErrorAnalysisMarton's inner bound — error analysis
• InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCoreMarton's inner bound — the conditional AEP for the transmitted pair
• InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCore.PrelimMarton's inner bound — coordinate laws shared by the two receivers
• InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCore.Receiver1Marton's inner bound — the conditional AEP for receiver 1
• InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCore.Receiver2Marton's inner bound — the conditional AEP for receiver 2
• InformationTheory.Shannon.BroadcastChannel.Marton.MutualCoveringSecond-moment core of the mutual covering lemma
• InformationTheory.Shannon.BroadcastChannel.Marton.SetupMarton's inner bound — five-variable ambient setup
• InformationTheory.Shannon.BroadcastChannel.MartonFullSupportBroadcast channel — Marton's inner bound without the auxiliary support hypotheses
• InformationTheory.Shannon.BroadcastChannel.MartonUnionBroadcast channel — Marton's inner bound as a union over auxiliary alphabets
• InformationTheory.Shannon.BroadcastChannel.OperationalBroadcast channel — operational capacity region
• InformationTheory.Shannon.BroadcastChannel.OuterBoundBroadcast channel — cooperative outer bound
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUVGeneral broadcast channel — the UV outer bound (Nair–El Gamal)
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.AssemblyBroadcast channel — the operational capacity region lies in the UV outer region
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.BridgeBroadcast channel — from a block code to its ambient law
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.GatewayGeneral broadcast channel — chain-rule gateway for the UV outer bound
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.MartonBridgeBroadcast channel — Marton's inner-bound law as a UV channel law
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.QuantizationBroadcast channel — truncating the countable auxiliary of the UV outer region
• InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.RegionBroadcast channel — the UV outer region as a subset of the plane
• InformationTheory.Shannon.BroadcastChannel.Superposition.AssemblyBroadcast channel — the UV outer region of a less noisy channel is achievable
• InformationTheory.Shannon.BroadcastChannel.Superposition.FullSupportBroadcast channel — perturbing an achievability pair to full support
• InformationTheory.Shannon.BroadcastChannel.Superposition.MoreCapableBroadcast channel — the capacity region of a more capable channel
• InformationTheory.Shannon.BroadcastChannel.Superposition.RegionBroadcast channel — the superposition inner bound
• InformationTheory.Shannon.BroadcastChannel.Superposition.TimeShareBroadcast channel — absorbing a time-sharing variable into the superposition cloud
• InformationTheory.Shannon.ChannelCoding.AchievabilityChannel coding achievability theorem
• InformationTheory.Shannon.ChannelCoding.Achievability.CoreChannel coding achievability — core definitions
• InformationTheory.Shannon.ChannelCoding.Achievability.MainChannel coding achievability — pigeonhole + main theorem
• InformationTheory.Shannon.ChannelCoding.Achievability.RandomCodebookChannel coding achievability — random codebook average bound
• InformationTheory.Shannon.ChannelCoding.BasicChannel coding theorem — primitive definitions
• InformationTheory.Shannon.ChannelCoding.CodeToAmbientFrom a block code to its ambient law
• InformationTheory.Shannon.ChannelCoding.ConverseChannel coding converse — n-variable i.i.d. form
• InformationTheory.Shannon.ChannelCoding.ConverseGeneralChannel coding converse — general input form, chain-rule decomposition
• InformationTheory.Shannon.ChannelCoding.ConverseMemorylessChannel coding converse — pure IsMemorylessChannel form
• InformationTheory.Shannon.ChannelCoding.ConverseMemorylessChainRuleChannel coding converse (general input) — memoryless per-summand bound
• InformationTheory.Shannon.ChannelCoding.ConverseMemorylessMarkovChannel coding converse — strong memoryless DMC variant
• InformationTheory.Shannon.ChannelCoding.FeedbackChannel coding feedback converse — chain-rule form
• InformationTheory.Shannon.ChannelCoding.FeedbackMemorylessFeedback channel coding converse — memoryless complete form
• InformationTheory.Shannon.ChannelCoding.MIDecompContinuous-channel mutual-information chain rule (generic body)
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremShannon noisy channel coding theorem — full form (Cover-Thomas)
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremGeneralShannon noisy channel coding theorem — smoothing infrastructure
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxErrorShannon noisy channel coding theorem — max-error achievability (umbrella)
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.OuterNOuter N construction — max-error closed form
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.PmfLogBoundsδ-asymptotic pmfLog bounds for the smooth channel
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.SeedLemmasSmooth input distribution and capacity lower bound construction
• InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.SmoothInstantiationAchievability at the smooth channel — closed-form N
• InformationTheory.Shannon.ChannelCoding.StrongConverseChannel coding strong converse — Verdú-Han single-shot lower bound
• InformationTheory.Shannon.ChannelCoding.StrongConverseAsymptoticChannel coding asymptotic strong converse (Wolfowitz)
• InformationTheory.Shannon.Chernoff.BasicChernoff information and the Hoeffding tradeoff exponent
• InformationTheory.Shannon.Chernoff.Converse
• InformationTheory.Shannon.Chernoff.NLetterZSumn-letter Chernoff Z-sum factorization
• InformationTheory.Shannon.CondEntropyMemorylessConditional entropy on Fin n under strong memoryless DMC
• InformationTheory.Shannon.CondKLIntegralConditional Kullback-Leibler divergence, integral form
• InformationTheory.Shannon.CondMIChainRuleConditional mutual-information chain rule over a Fin-prefix
• InformationTheory.Shannon.CondMutualInfoConditional mutual information and Markov chains
• InformationTheory.Shannon.CondMutualInfoMixtureAveraging an information slot over a countable mixture
• InformationTheory.Shannon.ConditionalAEPConditional asymptotic equipartition for independent non-identical products
• InformationTheory.Shannon.ConditionalMethodOfTypesConditional method of types — conditionalStronglyTypicalSlice_mass_ge
• InformationTheory.Shannon.ConditionalMethodOfTypes.CoreConditional method of types — Core
• InformationTheory.Shannon.ConditionalMethodOfTypes.MassConditional method of types — Mass assembly
• InformationTheory.Shannon.ConditionalMethodOfTypes.Mass.ConcentrationConditional method of types — entropy concentration
• InformationTheory.Shannon.ConditionalMethodOfTypes.Mass.SliceMassConditional method of types — slice mass lower bound
• InformationTheory.Shannon.ConverseSingle-shot Shannon channel coding converse
• InformationTheory.Shannon.Cramer.CramerCramér's theorem
• InformationTheory.Shannon.Cramer.InfinitePiTiltedChangeOfMeasureinfinitePi-tilted change-of-measure
• InformationTheory.Shannon.Cramer.LC2PhaseCCramér lower bound on the canonical infinitePi product
• InformationTheory.Shannon.Cramer.TiltedIIDCramér lower-bound discharge: i.i.d. plumbing
• InformationTheory.Shannon.Cramer.TiltedLLNCramér lower-bound extension: tilted-side law of large numbers
• InformationTheory.Shannon.CramerBoundaryUpstreamCramér boundary-closure upstream module
• InformationTheory.Shannon.CramerCltBoundaryClosureCramér / Chernoff CLT-boundary closure
• InformationTheory.Shannon.CramerGeneralLowerCramér lower bound — general i.i.d.
• InformationTheory.Shannon.CsiszarProjectionCsiszár I-projection and the Pythagorean inequality
• InformationTheory.Shannon.DPIData processing inequality for mutual information
• InformationTheory.Shannon.DeLaValleePoussinThe de la Vallée-Poussin criterion for uniform integrability
• InformationTheory.Shannon.DifferentialEntropyDifferential entropy and Gaussian max-entropy
• InformationTheory.Shannon.EPI.ApproxIdentityL1EPI G2 Layer 1 — L¹ convergence of the approximate identity
• InformationTheory.Shannon.EPI.Blachman.DensityEPI Blachman — explicit density route (S2 + S3, condExp-free)
• InformationTheory.Shannon.EPI.Blachman.GaussianDensityRouteGaussian density route for IsBlachmanConvReady / IsRegularDensityV2
• InformationTheory.Shannon.EPI.Blachman.GeneralDensityNon-Gaussian IsBlachmanConvReady producer — EPI A-5 precondition (4)
• InformationTheory.Shannon.EPI.Case1.ProducerMeasurabilityEPI Case-1 producer measurability bricks (Layer C closure, C-b route)
• InformationTheory.Shannon.EPI.Case1.RatioLimitEPI case-1 via ratio + scaling squeeze (entropic-CLT-free)
• InformationTheory.Shannon.EPI.Case1.RatioLimit.Assembly
• InformationTheory.Shannon.EPI.Case1.RatioLimit.PathRegular
• InformationTheory.Shannon.EPI.Case1.RatioLimit.Producer
• InformationTheory.Shannon.EPI.Case1.SmoothingLimitExplicit-density de Bruijn producer and explicit density-form EPI
• InformationTheory.Shannon.EPI.Case1.TwoTimeEPI case-1 sum frontier — two-time object skeleton
• InformationTheory.Shannon.EPI.Case1.TwoTime.CoreEPI case-1 two-time object — Core (§0)
• InformationTheory.Shannon.EPI.Case1.TwoTime.EntropyPowerInequalityEPI case-1 two-time object — entropy power inequality bridge (§4 terminal)
• InformationTheory.Shannon.EPI.Case1.TwoTime.GapDerivativeEPI case-1 two-time object — gap object and its derivative (§2–§3)
• InformationTheory.Shannon.EPI.Case1.TwoTime.MonotonicityAndSaturationEPI case-1 two-time object — endpoints, antitonicity, Gaussian saturation (§4)
• InformationTheory.Shannon.EPI.Case1.TwoTime.PathsEPI case-1 two-time object — matched-time path existence (§1)
• InformationTheory.Shannon.EPI.Conv.DensityConvolution density apparatus
• InformationTheory.Shannon.EPI.Conv.DensityAssocConvolution-density associativity + 4-fold interchange bridge (EPI A-5 precondition (3))
• InformationTheory.Shannon.EPI.Conv.DensityGaussianGatewayConvolution density gateway — pX integrable-only + Gaussian-kernel-smooth variant
• InformationTheory.Shannon.EPI.Conv.DensityNormalizationNormalization of the convolution density (EPI A-5 precondition (2))
• InformationTheory.Shannon.EPI.Conv.DensityRegularIsRegularDensityV2 (convDensityAdd pX g_t) producer — EPI A-5 precondition (1)
• InformationTheory.Shannon.EPI.Conv.DensitySecondDerivConvolution density — spatial 2nd derivative identification (STEP D bridge)
• InformationTheory.Shannon.EPI.DensityFormDensity-form entropy power inequality
• InformationTheory.Shannon.EPI.G2.BridgeDensityHelpersEPI G2 bridge — density-expansion + Fubini-marginal helpers (sub-gaps (b), (c))
• InformationTheory.Shannon.EPI.G2.ConvEntropyDensityEPI G2 — (β) density-only lower bound
• InformationTheory.Shannon.EPI.G2.ConvEntropyMonotoneEPI G2 — (β) Convolution does not decrease differential entropy
• InformationTheory.Shannon.EPI.G2.HeatFlowContinuityHeat-flow entropy-power continuity at the endpoint t = 0⁺
• InformationTheory.Shannon.EPI.G2.KLFatouLSCEPI G2 (α) upper bound — KL lower-semicontinuity via klFun-Fatou
• InformationTheory.Shannon.EPI.G2.KLVariationalLowerDonsker–Varadhan variational lower bound (easy direction)
• InformationTheory.Shannon.EPI.InfiniteVariance.CapstoneClassical entropy power inequality for infinite-variance sums — capstone
• InformationTheory.Shannon.EPI.InfiniteVariance.TruncationClassical entropy power inequality for absolutely continuous, infinite-variance sums
• InformationTheory.Shannon.EPI.InfiniteVariance.Truncation.Construction
• InformationTheory.Shannon.EPI.InfiniteVariance.Truncation.Convergence
• InformationTheory.Shannon.EPI.InfiniteVariance.Truncation.Density
• InformationTheory.Shannon.EPI.L3IntegrationEntropy power inequality — final integration
• InformationTheory.Shannon.EPI.NoiseExtensionEPI lift-and-transport: 3-noise lift machinery
• InformationTheory.Shannon.EPI.PlumbingEntropy Power Inequality — plumbing lemmas
• InformationTheory.Shannon.EPI.ScoreCrossTermOrthScore cross-term orthogonality (toward Blachman / Stam)
• InformationTheory.Shannon.EPI.Stam.ConditionalCauchySchwarzStam inequality Step 1 (score-convolution) + Step 2 (Cauchy-Schwarz) body
• InformationTheory.Shannon.EPI.Stam.DeBruijnConclusionStam → de Bruijn → EPI conclusion assembly
• InformationTheory.Shannon.EPI.Stam.EPIBridgeEntropy power inequality via the Stam inequality and de Bruijn integration
• InformationTheory.Shannon.EPI.Stam.FisherCouplingStam inequality body — Step 3 (Cauchy–Schwarz to symmetric Fisher coupling)
• InformationTheory.Shannon.EPI.Stam.InequalityStam inequality body discharge (Cauchy–Schwarz / convolution-score path)
• InformationTheory.Shannon.EPI.Stam.StandaloneStam's inequality — standalone density-level headline (Cover–Thomas)
• InformationTheory.Shannon.EPI.Stam.SupplyTwoTime
• InformationTheory.Shannon.EPI.Stam.ToBridgeStam → EPI: Csiszár ratio path-derivative cluster
• InformationTheory.Shannon.EPI.Unconditional.DispatchEntropy power inequality — case-1 dispatch
• InformationTheory.Shannon.EPI.Unconditional.DispatchFullEntropy power inequality — fully unconditional dispatch
• InformationTheory.Shannon.EPI.Unconditional.MixedCaseEntropy power inequality — singular and mixed cases
• InformationTheory.Shannon.EPI.Unconditional.TruncationLimitTruncation + monotone-limit route for gateway monotonicity
• InformationTheory.Shannon.EPI.Unconditional.TruncationLimit.CoreTruncationLimit — core part
• InformationTheory.Shannon.EPI.Unconditional.TruncationLimit.LimitTruncationLimit — limit part
• InformationTheory.Shannon.EPI.Unconditional.TruncationLimit.MonoTruncationLimit — monotonicity part
• InformationTheory.Shannon.EPI.Vitali.AEG2 Vitali witness — a.e. pointwise convergence of the entropy integrands (subsequence)
• InformationTheory.Shannon.EPI.Vitali.UIEPI G2 Gaussian max-entropy bound for the convolution density
• InformationTheory.Shannon.EPI.Vitali.UnifTightEPI G2 Vitali witness — second-moment helpers for the retired UnifTight (UT) route
• InformationTheory.Shannon.EntropyEntropy chain rule and conditioning monotonicity
• InformationTheory.Shannon.EntropyPower.ExtExtended entropy power
• InformationTheory.Shannon.EntropyPower.InequalityEntropy power inequality (Cover–Thomas)
• InformationTheory.Shannon.EntropyRateEntropy rate of a stationary process
• InformationTheory.Shannon.FisherConvBoundStam convolution Fisher information bound J(pX ∗ g_s) ≤ 1/s
• InformationTheory.Shannon.FisherDeBruijnGaussianFully-internal Gaussian de Bruijn witness
• InformationTheory.Shannon.FisherInfo.BasicFisher information density helpers
• InformationTheory.Shannon.FisherInfo.DeBruijnFisher information V2 — measure-keyed wrapper and de Bruijn identity
• InformationTheory.Shannon.FisherInfo.DeBruijnAssemblyPer-time de Bruijn identity — assembly
• InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Assembly
• InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Core
• InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Derivatives
• InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Domination
• InformationTheory.Shannon.FisherInfo.DeBruijnGeneralde Bruijn identity (V2)
• InformationTheory.Shannon.FisherInfo.DeBruijnHeatFlowFisher information V2 — de Bruijn heat flow
• InformationTheory.Shannon.FisherInfo.DeBruijnPerTimePer-time de Bruijn identity — analytic-core atoms
• InformationTheory.Shannon.FisherInfo.DeBruijnStandalonede Bruijn identity — standalone headlines (Cover–Thomas)
• InformationTheory.Shannon.FisherInfo.GaussianFisher information — Gaussian discharge
• InformationTheory.Shannon.FisherInfo.HeatFlowFisher information V2 — heat flow
• InformationTheory.Shannon.FisherInfo.OfDensityFisher information of a density
• InformationTheory.Shannon.Gambling.BasicKelly gambling and the doubling rate (Cover–Thomas)
• InformationTheory.Shannon.Gambling.OperationalSequencesOperational gambling over horse-race sequences (Cover–Thomas)
• InformationTheory.Shannon.Gambling.SideInformationGambling with side information (Cover–Thomas)
• InformationTheory.Shannon.GaussianPDFVarianceDerivativeGaussian PDF variance (time) derivative — de Bruijn FTC core
• InformationTheory.Shannon.GeneralDMC.BasicGeneral DMC capacity (limit form) — publish layer
• InformationTheory.Shannon.GeneralDMC.ExtensionGeneral DMC capacity — extension layer
• InformationTheory.Shannon.Han.BasicJoint entropy on Fin n, the n-variable chain rule, and Han's inequality
• InformationTheory.Shannon.Han.DHan's inequality — subset joint entropy
• InformationTheory.Shannon.Han.DAverageHan's inequality — subset average chain
• InformationTheory.Shannon.Han.DShearerHan's inequality — Shearer's inequality (integer covering form)
• InformationTheory.Shannon.Hoeffding.BoundaryMinimizerHoeffding tradeoff — sandwich body completion
• InformationTheory.Shannon.Hoeffding.LagrangeHoeffding tradeoff — Lagrange constraint-match via IVT
• InformationTheory.Shannon.Hoeffding.MinimizerAttainmentHoeffding I-projection minimizer attainment — IsHoeffdingTiltMinimal discharge
• InformationTheory.Shannon.Hoeffding.MinimizerExistenceHoeffding tradeoff — sandwich discharge
• InformationTheory.Shannon.Hoeffding.SandwichHoeffding tradeoff — rate boundedness
• InformationTheory.Shannon.Hoeffding.TiltHoeffding tradeoff — interior gradient body (Lagrange tilt)
• InformationTheory.Shannon.Hoeffding.TradeoffHoeffding tradeoff exponent — scaffolding and variational form
• InformationTheory.Shannon.Hoeffding.TradeoffExpHoeffding tradeoff — exponential-level redefinition
• InformationTheory.Shannon.Huffman.ExpectedLengthExpected length of the Huffman code
• InformationTheory.Shannon.Huffman.KraftSumKraft inequality for Huffman code lengths
• InformationTheory.Shannon.Huffman.LengthHuffman code lengths
• InformationTheory.Shannon.Huffman.OptimalityHuffman optimality — Cover–Thomas
• InformationTheory.Shannon.Huffman.StrongFormSwap normalization and Huffman optimality (Cover–Thomas)
• InformationTheory.Shannon.Huffman.SwapNormCompletionKraft completion: shorten a feasible code to a complete one
• InformationTheory.Shannon.Huffman.SwapNormProofThe pairing keystone of swap normalization
• InformationTheory.Shannon.HypercubeEdge.BoundaryBoolean hypercube edge-boundary bound
• InformationTheory.Shannon.HypercubeEdge.BoundarySharpHypercube edge-boundary entropy-sharp inequality
• InformationTheory.Shannon.IIDProductInput.Basici.i.d. ambient (μ, Xs, Ys) for channel coding achievability
• InformationTheory.Shannon.IIDProductInput.Jointi.i.d. ambient (μ, Xs, Ys) from a joint distribution (rate-distortion variant)
• InformationTheory.Shannon.KLDivContinuousKL divergence in vector form and its continuity
• InformationTheory.Shannon.Kolmogorov.CountingCounting and the existence of incompressible strings
• InformationTheory.Shannon.Kolmogorov.EntropyRateKolmogorov complexity converges to the entropy rate
• InformationTheory.Shannon.Kolmogorov.EntropyRateUpperA partial recursive type-class decoder for the entropy-rate upper bound
• InformationTheory.Shannon.Kolmogorov.IncompressibleIncompressible binary sequences obey the law of large numbers
• InformationTheory.Shannon.Kolmogorov.InvarianceInvariance and the literal upper bound
• InformationTheory.Shannon.Kolmogorov.LevinPrefix complexity and universal probability: the factor-two relation
• InformationTheory.Shannon.Kolmogorov.NoncomputableKolmogorov complexity is not computable
• InformationTheory.Shannon.Kolmogorov.OmegaChaitin's halting probability
• InformationTheory.Shannon.Kolmogorov.OmegaNoncomputableChaitin's constant is not computably approximable
• InformationTheory.Shannon.Kolmogorov.PrefixComputabilityComputability of the self-delimiting machine
• InformationTheory.Shannon.Kolmogorov.PrefixMachineA self-delimiting (prefix-free) universal machine for prefix complexity
• InformationTheory.Shannon.Kolmogorov.SufficientStatisticKolmogorov sufficient statistics and two-part descriptions
• InformationTheory.Shannon.Kolmogorov.UniversalMachineA length-additive universal machine for plain Kolmogorov complexity
• InformationTheory.Shannon.Kolmogorov.UniversalProbabilityThe universal probability of a natural number
• InformationTheory.Shannon.LZ78.AsymptoticOptimalityLZ78 greedy-parse encoding length + asymptotic-optimality bridge
• InformationTheory.Shannon.LZ78.AsymptoticOptimality.EncodingLengthLZ78 greedy encoding length + Cover-Thomas bit-length bounds (part 1/3)
• InformationTheory.Shannon.LZ78.AsymptoticOptimality.ParentBridgeAchievabilityLZ78 parent-bridge: Ziv achievability + asymptotic-optimality headline (part 3/3)
• InformationTheory.Shannon.LZ78.AsymptoticOptimality.ParentBridgeConverseLZ78 parent-bridge: converse a.s.-eventual lower bound (part 2/3)
• InformationTheory.Shannon.LZ78.BasicLempel–Ziv 78 asymptotic optimality
• InformationTheory.Shannon.LZ78.ConverseAsymptoticLZ78 converse — asymptotic body extension
• InformationTheory.Shannon.LZ78.ConverseUDObjectLZ78 converse UD-object
• InformationTheory.Shannon.LZ78.EmpiricalEntropyMeanLZ78 overhead control — empirical-entropy / mean bound
• InformationTheory.Shannon.LZ78.GreedyLongestPrefixLZ78 longest-prefix greedy parsing — distinct-phrase invariant
• InformationTheory.Shannon.LZ78.GreedyParsingLZ78 greedy parsing — per-phrase bit length
• InformationTheory.Shannon.LZ78.PhraseCountAsymptoticsLZ78 phrase-count asymptotic envelope (IsBigO bound)
• InformationTheory.Shannon.LZ78.PhraseCountingLZ78 distinct-phrase counting bound — c · log c ≤ K·n
• InformationTheory.Shannon.LZ78.ZivAchievabilityCompositionLZ78 achievability composition: threading + (k-state, length) grouping
• InformationTheory.Shannon.LZ78.ZivCondContextLZ78 conditional-context sub-distribution (node-context route)
• InformationTheory.Shannon.LZ78.ZivCondGroupingLZ78 conditional (k-state, length) grouping bridge
• InformationTheory.Shannon.LZ78.ZivEntropyBridgeLZ78 Ziv-inequality entropy bridge — foundational lemmas
• InformationTheory.Shannon.LZ78.ZivInequalityLZ78 Ziv's inequality — combinatorial counting layer
• InformationTheory.Shannon.LZ78.ZivLengthGroupingLZ78 length-grouping Jensen inequality
• InformationTheory.Shannon.LZ78.ZivMeasureBridgeLZ78 length-grouping measure bridge — per-length sub-distribution + log-sum
• InformationTheory.Shannon.LZ78.ZivThreadingLZ78 threading: per-phrase negLogQk decomposition (foundation)
• InformationTheory.Shannon.LoomisWhitneyLoomis–Whitney inequality (information-theoretic proof)
• InformationTheory.Shannon.LpPointwiseLifting an L² class to a genuine pointwise representative
• InformationTheory.Shannon.MIChainRuleMutual information chain rule (n-variable) and i.i.d. corollary
• InformationTheory.Shannon.MaxEntropy.BasicMaximum entropy (Gibbs inequality)
• InformationTheory.Shannon.MaxEntropy.ConstrainedConstrained maximum entropy (Cover–Thomas)
• InformationTheory.Shannon.MaxEntropy.ConstrainedKKTConstrained Maximum Entropy — Lagrange / KKT perspective
• InformationTheory.Shannon.McMillanKraftBridgeMcMillan → Kraft → Gibbs converse bridge (symbol-code level)
• InformationTheory.Shannon.MeasurePiTiltedFactorizationFinite Measure.pi tilt factorization
• InformationTheory.Shannon.MinkowskiDetMinkowski determinant inequality (Cover-Thomas)
• InformationTheory.Shannon.MultipleAccess.AchievabilityMultiple access channel — achievability codebook, decoder, and Bonferroni bound
• InformationTheory.Shannon.MultipleAccess.Achievability.CodebookMultiple access channel — codebook, decoder, and Bonferroni decomposition
• InformationTheory.Shannon.MultipleAccess.Achievability.RandomCodingMultiple access channel — two-codebook random-coding average and achievability
• InformationTheory.Shannon.MultipleAccess.AchievabilityCoreMultiple access channel — achievability analytic core
• InformationTheory.Shannon.MultipleAccess.BasicMultiple access channel — primitive definitions
• InformationTheory.Shannon.MultipleAccess.ConverseMultiple access channel — converse (outer bound)
• InformationTheory.Shannon.MultipleAccess.IIDAmbienti.i.d. ambient measure for the multiple access channel
• InformationTheory.Shannon.MultipleAccess.JointTypicalityMultiple access channel — three-way jointly typical set
• InformationTheory.Shannon.MultipleAccess.ReconciliationMultiple access channel — converse/achievability reconciliation bridge
• InformationTheory.Shannon.MultipleAccess.TimeSharingMultiple access channel — time-sharing achievability (full convex-hull form)
• InformationTheory.Shannon.MultipleAccess.TimeSharingConverseMultiple access channel — time-sharing converse (convex-geometry gateway)
• InformationTheory.Shannon.MultipleAccess.TimeSharingConverse.AssemblyMultiple access channel — time-sharing converse and the capacity region
• InformationTheory.Shannon.MultipleAccess.TimeSharingConverse.BridgeMultiple access channel — time-sharing converse, geometric gateway and measure bridge
• InformationTheory.Shannon.MultivariateDiffEntropyMultivariate differential entropy and subadditivity
• InformationTheory.Shannon.MutualInfoMutual information via KL divergence
• InformationTheory.Shannon.MutualInfoFiniteRangeMutual information against a variable of finite range
• InformationTheory.Shannon.MutualInfoReencodingInvariance of an information slot under a re-encoding of one of its variables
• InformationTheory.Shannon.NormalizedSincWhittaker-Shannon sampling (partial, Cover-Thomas)
• InformationTheory.Shannon.ParallelGaussian.BasicParallel Gaussian channels and water-filling
• InformationTheory.Shannon.ParallelGaussian.ConverseParallel Gaussian converse (correlated input)
• InformationTheory.Shannon.ParallelGaussian.Converse.Core
• InformationTheory.Shannon.ParallelGaussian.Converse.MixtureDensity
• InformationTheory.Shannon.ParallelGaussian.Converse.Regularity
• InformationTheory.Shannon.ParallelGaussian.KKTWater-filling KKT level and optimality
• InformationTheory.Shannon.ParallelGaussian.PerCoordParallel Gaussian capacity equals the water-filling sum
• InformationTheory.Shannon.ParallelGaussian.PerCoordRegularityParallel Gaussian capacity: regularity bundle and hypothesis-minimal headline
• InformationTheory.Shannon.PiShared Pi-type plumbing for Shannon information theory
• InformationTheory.Shannon.Pinsker.BasicPinsker's inequality (total variation and Kullback–Leibler divergence)
• InformationTheory.Shannon.Pinsker.SharpSharp Pinsker inequality (constant 1/√2)
• InformationTheory.Shannon.PolymatroidPolymatroid axioms for joint entropy
• InformationTheory.Shannon.Portfolio.BasicLog-optimal portfolios (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.OperationalSequencesOperational log-optimal portfolios over i.i.d. markets (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.SideInformationLog-optimal portfolios with side information (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.StationaryMarketLog-optimal portfolios over stationary ergodic markets (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.StationaryWinftyMeasurable selection of a log-optimal portfolio (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.StationaryWinftyAEPGrowing-memory W_∞ AEP for stationary markets (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.StationaryWinftyConcreteConcrete two-sided market instantiation of the growing-memory W_∞ AEP (Cover–Thomas)
• InformationTheory.Shannon.Portfolio.UniversalCover's universal portfolio (Cover–Thomas)
• InformationTheory.Shannon.RateDistortion.AchievabilityRate-distortion achievability — structure and pmf-direct R(D)
• InformationTheory.Shannon.RateDistortion.AchievabilityAmbientMeasureRate-distortion achievability — i.i.d. ambient measure instantiation
• InformationTheory.Shannon.RateDistortion.AchievabilityAsymptoticFailureDecayRate-distortion achievability — asymptotic decay and distortion decomposition
• InformationTheory.Shannon.RateDistortion.AchievabilityCodebookMatchProbabilityRate-distortion achievability — codebook-level match probability
• InformationTheory.Shannon.RateDistortion.AchievabilityGeneralSourceRate-distortion achievability — general (arbitrary) source
• InformationTheory.Shannon.RateDistortion.AchievabilityJointStrongTypicalityRate-distortion achievability — joint strong-typicality apparatus
• InformationTheory.Shannon.RateDistortion.AchievabilityJointTypicalEncoderRate-distortion achievability — joint-typical lossy encoder + distortion typical set
• InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicalityRate-distortion achievability — assembly (strong-typicality variant)
• InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicality.FailureTendstoZeroRate-distortion achievability (strong-typicality variant) — failure probability tends to zero
• InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicality.SupportingBoundsRate-distortion achievability (strong-typicality variant) — supporting bounds
• InformationTheory.Shannon.RateDistortion.AchievabilityUnconditionalRate-distortion achievability — strong-typical ⊆ distortion-typical inclusion
• InformationTheory.Shannon.RateDistortion.ConverseRate-distortion converse (single-shot)
• InformationTheory.Shannon.RateDistortion.ConverseMonotoneRate-distortion converse (specified-distortion form)
• InformationTheory.Shannon.RateDistortion.ConverseNLetterRate-distortion converse (n-letter form)
• InformationTheory.Shannon.RateDistortion.ConvexityRate-distortion convexity
• InformationTheory.Shannon.RelayCutsetRelay channel — cut-set outer bound (structure + single-letterization)
• InformationTheory.Shannon.SMB.AlgoetCoverSMB Algoet–Cover sandwich
• InformationTheory.Shannon.SMB.AlgoetCover.Boundedness
• InformationTheory.Shannon.SMB.AlgoetCover.KMarkovApproximation
• InformationTheory.Shannon.SMB.AlgoetCover.LiminfSMB Algoet–Cover liminf direction and hypothesis-free capstone
• InformationTheory.Shannon.SMB.AlgoetCover.Limsup
• InformationTheory.Shannon.SMB.AlgoetCover.MarkovLikelihoodRatioLikelihood ratio of the k-Markov approximation
• InformationTheory.Shannon.SMB.AlgoetCover.TwoSidedRatio
• InformationTheory.Shannon.SMB.ChainRuleSMB chain rule decomposition
• InformationTheory.Shannon.SMB.McMillanBreimanShannon-McMillan-Breiman theorem (sandwich form)
• InformationTheory.Shannon.Sanov.BasicSanov's theorem — type class probability upper bound (A form)
• InformationTheory.Shannon.Sanov.LDPSanov's theorem — LDP upper bound (B form)
• InformationTheory.Shannon.Sanov.LiminfBoundSanov LDP liminf lower bound
• InformationTheory.Shannon.Sanov.MultinomialLowerBoundMultinomial lower bound (Stirling-free)
• InformationTheory.Shannon.Sanov.RoundedTypeSequenceRounded type sequence (achievable type index)
• InformationTheory.Shannon.Sanov.TendstoSandwichSanov LDP equality form (Tendsto sandwich)
• InformationTheory.Shannon.ShannonCode.BasicShannon code (per-symbol prefix code achievability)
• InformationTheory.Shannon.ShannonCode.KraftReverseKraft inequality converse: existence of prefix codes
• InformationTheory.Shannon.ShannonHartley.AchievabilityContinuous-time Shannon-Hartley: achievability (Cover-Thomas)
• InformationTheory.Shannon.ShannonHartley.BasicBandlimited Channel / Shannon-Hartley formula
• InformationTheory.Shannon.ShannonHartley.ConverseShannon-Hartley converse — the operational parallel-Gaussian converse (equal-noise form)
• InformationTheory.Shannon.ShannonHartley.ConverseCountCount domination for the Shannon–Hartley converse
• InformationTheory.Shannon.ShannonHartley.ConverseFinalContinuous-time Shannon-Hartley: converse assembly and the identity
• InformationTheory.Shannon.ShannonHartley.MainContinuous-time Shannon-Hartley: headline theorems
• InformationTheory.Shannon.ShannonHartley.OperationalContinuous-time Shannon-Hartley operational capacity
• InformationTheory.Shannon.ShannonHartley.PreequalizerPre-equalizer: bounded-below endomorphisms are invertible with norm control
• InformationTheory.Shannon.ShannonHartley.RotationShannon–Hartley converse — isotropic-Gaussian rotation invariance
• InformationTheory.Shannon.ShannonHartley.WaterfillWater-filling arithmetic for the Shannon-Hartley converse
• InformationTheory.Shannon.SlepianWolf.AchievabilitySlepian–Wolf achievability (corner point of the sum bound)
• InformationTheory.Shannon.SlepianWolf.BasicSlepian–Wolf single-shot converse
• InformationTheory.Shannon.SlepianWolf.BinningSlepian–Wolf random binning machinery
• InformationTheory.Shannon.SlepianWolf.ConditionalTypicalSliceSlepian–Wolf conditional typical slice
• InformationTheory.Shannon.SlepianWolf.FullRateRegionSlepian–Wolf full rate region — error event decomposition
• InformationTheory.Shannon.SlepianWolf.FullRateRegion.AliasBound
• InformationTheory.Shannon.SlepianWolf.FullRateRegion.Core
• InformationTheory.Shannon.SlepianWolf.FullRateRegion.PairBound
• InformationTheory.Shannon.StamGaussianBoundStam convex Fisher bound — Gaussian instance
• InformationTheory.Shannon.Stationary.BasicStationary processes
• InformationTheory.Shannon.Stationary.KernelStationary-process telescoping layer (LZ78 blockRV factorization)
• InformationTheory.Shannon.Stein.AchievabilityStein's lemma: achievability
• InformationTheory.Shannon.Stein.ConverseStein's lemma: converse
• InformationTheory.Shannon.Stein.OptimalExponentStein's lemma: the optimal type-II exponent
• InformationTheory.Shannon.StrongSteinStrong Stein's lemma — convergence to KL divergence
• InformationTheory.Shannon.StrongTypicalityStrong typicality (Cover-Thomas)
• InformationTheory.Shannon.SufficientStatisticSufficient statistics and mutual information (Cover-Thomas)
• InformationTheory.Shannon.TimeBandLimitingThe time-and-band-limiting operator on L²(ℝ;ℂ)
• InformationTheory.Shannon.TimeBandLimiting.CountTime-and-band-limiting operator — the two-sided eigenvalue count and achievability
• InformationTheory.Shannon.TimeBandLimiting.EnumerationTime-and-band-limiting operator — the decreasing eigenvalue enumeration
• InformationTheory.Shannon.TimeBandLimiting.OperatorThe time-and-band-limiting operator on L²(ℝ;ℂ) — the operator itself
• InformationTheory.Shannon.TimeBandLimiting.SecondMomentTime-and-band-limiting operator — the window deficit and second moment
• InformationTheory.Shannon.TimeBandLimiting.TraceBoundTime-and-band-limiting operator — the trace bound and spectral gap
• InformationTheory.Shannon.TypeClassLowerBoundType-class size lower bound (Cover-Thomas)
• InformationTheory.Shannon.TypedRVTyped random variable API
• InformationTheory.Shannon.WhittakerShannonWhittaker–Shannon sampling theorem (Fourier-series route, Cover–Thomas)
• InformationTheory.Shannon.WynerZiv.AchievabilityWyner–Ziv operational achievability (binning + covering)
• InformationTheory.Shannon.WynerZiv.Achievability.ChosenWordWyner–Ziv achievability — covering chosen-word typicality and the joint lossy code
• InformationTheory.Shannon.WynerZiv.Achievability.ConcentrationWyner–Ziv achievability — inner concentration sub-lemmas for the Markov-lemma covering bound
• InformationTheory.Shannon.WynerZiv.Achievability.CoveringWyner–Ziv achievability — covering + binning construction
• InformationTheory.Shannon.WynerZiv.Achievability.DecompositionWyner–Ziv achievability — Steps 3–7 distortion decomposition and pmf-side product bounds
• InformationTheory.Shannon.WynerZiv.Achievability.HeadlineWyner–Ziv achievability — per-slack good codes and the operational achievability headline
• InformationTheory.Shannon.WynerZiv.Achievability.MarkovCoreWyner–Ziv achievability — the Markov core
• InformationTheory.Shannon.WynerZiv.Achievability.MassBoundWyner–Ziv achievability — source→ambient AEP mass transport and entropy helpers
• InformationTheory.Shannon.WynerZiv.Achievability.SourceTransportWyner–Ziv achievability — source transport and distortion bridge
• InformationTheory.Shannon.WynerZiv.BasicWyner–Ziv lossy distributed coding
• InformationTheory.Shannon.WynerZiv.ConditionalEntropyConvexityWyner–Ziv conditional-entropy-difference convexity
• InformationTheory.Shannon.WynerZiv.ConverseWyner–Ziv converse (operational lower bound on the rate)
• InformationTheory.Shannon.WynerZiv.Converse.HeadlineWyner–Ziv converse — endpoint continuity and the operational headline
• InformationTheory.Shannon.WynerZiv.Converse.PrelimWyner–Ziv converse — preliminaries (n-letter bound, pmf→measure, factorizable Markov chain)
• InformationTheory.Shannon.WynerZiv.Converse.SingleLetterWyner–Ziv converse — single-letterization
• InformationTheory.Shannon.WynerZiv.ConverseGatewayWyner–Ziv converse — heterogeneous Csiszár sum identity (gateway probe)
• InformationTheory.Shannon.WynerZiv.FactorizableRateWyner–Ziv convexity under the factorization predicate
• InformationTheory.Shannon.WynerZiv.ObjectiveConvexityWyner–Ziv objective convexity (Cover–Thomas)
• InformationTheory.Shannon.WynerZiv.OperationalWyner–Ziv operational achievability predicate
• InformationTheory.Shannon.WynerZiv.RateMonotonicityWyner–Ziv rate monotonicity and affine plumbing