ChannelCapacity.Finite

Finite-alphabet capacity-achieving prior uniqueness.

This file specializes the general development to finite measurable alphabets. In that setting, Shannon entropy gives an explicit formula for mutual information, so continuity and strict concavity can be proved internally without passing abstract topology or semicontinuity hypotheses through the public theorem statement.

noncomputable def ChannelCapacity.ProbabilityMeasure.entropy {α : Type u_1} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.ProbabilityMeasure α) : ℝ

Shannon entropy on a finite measurable alphabet, in nats.

Equations

• ChannelCapacity.ProbabilityMeasure.entropy μ = ∑ a : α, (↑μ {a}).toReal.negMulLog

def ChannelCapacity.Kernel.RowMatrixFullRank {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) : Prop

A concrete finite non-degeneracy condition: the row matrix has trivial kernel over ℝ.

Equations

• ChannelCapacity.Kernel.RowMatrixFullRank k = Function.Injective fun (w : α → ℝ) (b : β) => ∑ a : α, w a * ((k a) {b}).toReal

theorem ChannelCapacity.toMeasure_eq_count_withDensity {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.ProbabilityMeasure α) [Countable α] : ↑μ = MeasureTheory.Measure.count.withDensity fun (a : α) => ↑μ {a}

theorem ChannelCapacity.rnDeriv_count_ae {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.ProbabilityMeasure α) [Countable α] : (↑μ).rnDeriv MeasureTheory.Measure.count =ᵐ[MeasureTheory.Measure.count] fun (a : α) => ↑μ {a}

theorem ChannelCapacity.klFun_singletonMass {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.ProbabilityMeasure α) (a : α) : InformationTheory.klFun (↑μ {a}).toReal = 1 - (↑μ {a}).toReal - (↑μ {a}).toReal.negMulLog

theorem ChannelCapacity.toReal_klDiv_count {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.ProbabilityMeasure α) : (InformationTheory.klDiv (↑μ) MeasureTheory.Measure.count).toReal = ↑(Fintype.card α) - 1 - ProbabilityMeasure.entropy μ

theorem ChannelCapacity.sum_toReal_singletonMass {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.ProbabilityMeasure α) : ∑ a : α, (↑μ {a}).toReal = 1

noncomputable def ChannelCapacity.Kernel.rowProbabilityMeasure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (a : α) : MeasureTheory.ProbabilityMeasure β

The probability measure associated to a kernel row.

Equations

• ChannelCapacity.Kernel.rowProbabilityMeasure k a = ⟨k a, ⋯⟩

noncomputable def ChannelCapacity.Kernel.rowEntropy {α : Type u_1} {β : Type u_2} [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (a : α) : ℝ

Row entropy for a finite Markov kernel.

Equations

• ChannelCapacity.Kernel.rowEntropy k a = ChannelCapacity.ProbabilityMeasure.entropy (ChannelCapacity.Kernel.rowProbabilityMeasure k a)

noncomputable def ChannelCapacity.conditionalEntropy {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.ProbabilityMeasure α) (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] : ℝ

Conditional output entropy, linear in the prior.

Equations

• ChannelCapacity.conditionalEntropy p k = ∑ a : α, (↑p {a}).toReal * ChannelCapacity.Kernel.rowEntropy k a

theorem ChannelCapacity.Kernel.toReal_klDiv_count_eq_card_sub_one_sub_rowEntropy {α : Type u_1} {β : Type u_2} [Fintype β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (a : α) : (InformationTheory.klDiv (k a) MeasureTheory.Measure.count).toReal = ↑(Fintype.card β) - 1 - rowEntropy k a

The KL divergence of a kernel row against counting measure is the usual finite entropy expression.

theorem ChannelCapacity.weighted_toReal_klDiv_count_eq_card_sub_one_sub_conditionalEntropy {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) : ∑ a : α, (↑p {a}).toReal * (InformationTheory.klDiv (k a) MeasureTheory.Measure.count).toReal = ↑(Fintype.card β) - 1 - conditionalEntropy p k

Averaging the row KL divergences against counting measure recovers the conditional entropy.

theorem ChannelCapacity.convexCombination_toReal_apply {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (p q : MeasureTheory.ProbabilityMeasure α) (t : NNReal) (ht : t ≤ 1) (a : α) : (↑(ProbabilityMeasure.convexCombination p q t ht) {a}).toReal = ↑t * (↑p {a}).toReal + (1 - ↑t) * (↑q {a}).toReal

theorem ChannelCapacity.conditionalEntropy_convexCombination {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] (p q : MeasureTheory.ProbabilityMeasure α) (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (t : NNReal) (ht : t ≤ 1) : conditionalEntropy (ProbabilityMeasure.convexCombination p q t ht) k = ↑t * conditionalEntropy p k + (1 - ↑t) * conditionalEntropy q k

theorem ChannelCapacity.absolutelyContinuous_count {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.ProbabilityMeasure α) [Countable α] : (↑μ).AbsolutelyContinuous MeasureTheory.Measure.count

theorem ChannelCapacity.outputPrior_apply_singleton {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) (b : β) : ↑(outputPrior k p) {b} = ∑ a : α, ↑p {a} * (k a) {b}

theorem ChannelCapacity.toReal_outputPrior_apply_singleton {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) (b : β) : (↑(outputPrior k p) {b}).toReal = ∑ a : α, (↑p {a}).toReal * ((k a) {b}).toReal

theorem ChannelCapacity.klDiv_count_ne_top {β : Type u_2} [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.ProbabilityMeasure β) [Finite β] : InformationTheory.klDiv (↑μ) MeasureTheory.Measure.count ≠ ⊤

theorem ChannelCapacity.joint_klDiv_count_ne_top {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] [Finite α] [Finite β] (p : MeasureTheory.ProbabilityMeasure α) : InformationTheory.klDiv (↑(jointLaw k p)) ((↑p).compProd (ProbabilityTheory.Kernel.const α MeasureTheory.Measure.count)) ≠ ⊤

theorem ChannelCapacity.toReal_joint_klDiv_count {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] [Finite β] (p : MeasureTheory.ProbabilityMeasure α) : (InformationTheory.klDiv (↑(jointLaw k p)) ((↑p).compProd (ProbabilityTheory.Kernel.const α MeasureTheory.Measure.count))).toReal = ∑ a : α, (↑p {a}).toReal * (InformationTheory.klDiv (k a) MeasureTheory.Measure.count).toReal

theorem ChannelCapacity.mutualInformation_eq_entropy_outputPrior_sub_conditionalEntropy {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] [Finite β] (p : MeasureTheory.ProbabilityMeasure α) : mutualInformation p k = ProbabilityMeasure.entropy (outputPrior k p) - conditionalEntropy p k

theorem ChannelCapacity.entropy_strictlyConcave {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p q : MeasureTheory.ProbabilityMeasure α) (h_ne : p ≠ q) (t : NNReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : ProbabilityMeasure.entropy (ProbabilityMeasure.convexCombination p q t ⋯) > ↑t * ProbabilityMeasure.entropy p + (1 - ↑t) * ProbabilityMeasure.entropy q

theorem ChannelCapacity.Kernel.injectivePriorPushforward_of_rowMatrixFullRank {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (hRank : RowMatrixFullRank k) : InjectivePriorPushforward k

theorem ChannelCapacity.Kernel.mutualInformation_strictlyConcave_of_rowMatrixFullRank {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Finite β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (hRank : RowMatrixFullRank k) (p q : MeasureTheory.ProbabilityMeasure α) (_h_ne : p ≠ q) (t : NNReal) (_ht_pos : 0 < t) (ht_lt_one : t < 1) : mutualInformation (ProbabilityMeasure.convexCombination p q t ⋯) k > ↑t * mutualInformation p k + (1 - ↑t) * mutualInformation q k

noncomputable def ChannelCapacity.singletonIndicatorContinuousMap {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (a : α) : C(α, ℝ)

The indicator of the singleton {a} as a continuous bundled map, using that α is discrete.

Equations

• ChannelCapacity.singletonIndicatorContinuousMap a = { toFun := {a}.indicator fun (x : α) => 1, continuous_toFun := ⋯ }

theorem ChannelCapacity.continuous_toReal_apply_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace α] [DiscreteTopology α] [BorelSpace α] [CompactSpace α] (a : α) : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => (↑p {a}).toReal

theorem ChannelCapacity.continuous_entropy {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace α] [DiscreteTopology α] [BorelSpace α] [CompactSpace α] : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => ProbabilityMeasure.entropy p

theorem ChannelCapacity.ProbabilityMeasure.integral_eq_sum_singletonMass {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.ProbabilityMeasure α) (f : α → ℝ) : ∫ (a : α), f a ∂↑μ = ∑ a : α, (↑μ {a}).toReal * f a

theorem ChannelCapacity.continuous_outputPrior_toReal_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [TopologicalSpace α] [DiscreteTopology α] [BorelSpace α] [CompactSpace α] [Finite α] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (b : β) : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => (↑(outputPrior k p) {b}).toReal

theorem ChannelCapacity.continuous_outputPrior {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] [BorelSpace α] [BorelSpace β] [CompactSpace α] [CompactSpace β] [Finite α] [Finite β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => outputPrior k p

theorem ChannelCapacity.continuous_outputEntropy {α : Type u_1} {β : Type u_2} [Fintype β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [TopologicalSpace α] [DiscreteTopology α] [BorelSpace α] [CompactSpace α] [Finite α] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => ProbabilityMeasure.entropy (outputPrior k p)

theorem ChannelCapacity.continuous_conditionalEntropy {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [TopologicalSpace α] [DiscreteTopology α] [BorelSpace α] [CompactSpace α] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => conditionalEntropy p k

theorem ChannelCapacity.continuous_mutualInformation_of_finite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [TopologicalSpace α] [DiscreteTopology α] [BorelSpace α] [CompactSpace α] [Finite α] [Finite β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] : Continuous fun (p : MeasureTheory.ProbabilityMeasure α) => mutualInformation p k

theorem ChannelCapacity.exists_unique_capacity_achieving_prior_of_finite {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Finite β] [Nonempty α] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (hRank : Kernel.RowMatrixFullRank k) : ∃! p : MeasureTheory.ProbabilityMeasure α, mutualInformation p k = channelCapacity k

Finite-alphabet capacity theorem with all hypotheses discharged internally. The general measure-theoretic theorem remains available separately; this theorem is the concrete upstream-ready specialization using the canonical weak topology on probability measures over finite discrete alphabets.