ChannelCapacity.Basic

Measure-theoretic primitives for Shannon mutual information over a Markov kernel.

This file keeps the surface small:

• ProbabilityMeasure.convexCombination
• jointLaw
• outputPrior
• independentJointLaw
• mutualInformation

The mutual information is defined directly from Mathlib's klDiv.

ProbabilityMeasure.convexCombination is the one deliberate local primitive here. Mathlib already has the corresponding affine structure on measures, but not yet on the subtype of probability measures, so this file provides the subtype-level wrapper needed by the strict-concavity and finite uniqueness arguments.

noncomputable def ProbabilityMeasure.convexCombination {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (t : NNReal) (ht : t ≤ 1) : MeasureTheory.ProbabilityMeasure Ω

Convex combination of two probability measures.

This is a subtype-level wrapper around convex combinations of measures. It exists because Mathlib does not currently provide an affine-space structure on ProbabilityMeasure Ω.

Equations

• ProbabilityMeasure.convexCombination μ ν t ht = ⟨t • ↑μ + (1 - t) • ↑ν, ⋯⟩

@[simp]

theorem ProbabilityMeasure.convexCombination_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (t : NNReal) (ht : t ≤ 1) : ↑(convexCombination μ ν t ht) = t • ↑μ + (1 - t) • ↑ν

theorem ProbabilityMeasure.convexCombination_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (t : NNReal) (ht : t ≤ 1) {s : Set Ω} (_hs : MeasurableSet s) : ↑(convexCombination μ ν t ht) s = ↑t * ↑μ s + ↑(1 - t) * ↑ν s

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

The output prior induced by pushing a prior through a Markov kernel.

Equations

• ChannelCapacity.outputPrior k p = ⟨(↑p).bind ⇑k, ⋯⟩

@[simp]

theorem ChannelCapacity.outputPrior_toMeasure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) : ↑(outputPrior k p) = (↑p).bind ⇑k

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

The joint law p ⊗ k on α × β.

Equations

• ChannelCapacity.jointLaw k p = ⟨(↑p).compProd k, ⋯⟩

@[simp]

theorem ChannelCapacity.jointLaw_toMeasure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) : ↑(jointLaw k p) = (↑p).compProd k

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

The independent coupling with the same input prior and induced output prior.

Equations

• ChannelCapacity.independentJointLaw k p = ⟨(↑p).compProd (ProbabilityTheory.Kernel.const α ↑(ChannelCapacity.outputPrior k p)), ⋯⟩

@[simp]

theorem ChannelCapacity.independentJointLaw_toMeasure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) : ↑(independentJointLaw k p) = (↑p).compProd (ProbabilityTheory.Kernel.const α ↑(outputPrior k p))

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

Shannon mutual information between an input prior and a Markov kernel.

Equations

• ChannelCapacity.mutualInformation p k = (InformationTheory.klDiv ↑(ChannelCapacity.jointLaw k p) ↑(ChannelCapacity.independentJointLaw k p)).toReal