ChannelCapacity.Capacity #
Capacity and generic existence/uniqueness packaging for maximizing mutual information.
noncomputable def
ChannelCapacity.channelCapacity
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
:
Shannon channel capacity as the supremum over all priors.
Equations
- ChannelCapacity.channelCapacity k = sSup (Set.range fun (p : MeasureTheory.ProbabilityMeasure α) => ChannelCapacity.mutualInformation p k)
Instances For
def
ChannelCapacity.IsCapacityAchievingPrior
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
(p : MeasureTheory.ProbabilityMeasure α)
:
A prior achieves capacity if it attains the supremum.
Equations
Instances For
theorem
ChannelCapacity.channelCapacity_eq_of_isMaxOn_univ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
{p : MeasureTheory.ProbabilityMeasure α}
(hp : IsMaxOn (fun (q : MeasureTheory.ProbabilityMeasure α) => mutualInformation q k) Set.univ p)
:
theorem
ChannelCapacity.exists_isMaxOn_mutualInformation
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
[TopologicalSpace (MeasureTheory.ProbabilityMeasure α)]
(hNonempty : Set.univ.Nonempty)
(hCompact : IsCompact Set.univ)
(hUsc : UpperSemicontinuous fun (p : MeasureTheory.ProbabilityMeasure α) => mutualInformation p k)
:
∃ (p : MeasureTheory.ProbabilityMeasure α),
IsMaxOn (fun (q : MeasureTheory.ProbabilityMeasure α) => mutualInformation q k) Set.univ p
theorem
ChannelCapacity.exists_capacity_achieving_prior
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
[TopologicalSpace (MeasureTheory.ProbabilityMeasure α)]
(hNonempty : Set.univ.Nonempty)
(hCompact : IsCompact Set.univ)
(hUsc : UpperSemicontinuous fun (p : MeasureTheory.ProbabilityMeasure α) => mutualInformation p k)
:
∃ (p : MeasureTheory.ProbabilityMeasure α), IsCapacityAchievingPrior k p
theorem
ChannelCapacity.exists_unique_capacity_achieving_prior
{α : Type u_3}
{β : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
(h : Kernel.InjectivePriorPushforward k)
(hWC : Kernel.WellConditionedForCapacity k)
[TopologicalSpace (MeasureTheory.ProbabilityMeasure α)]
(hNonempty : Set.univ.Nonempty)
(hCompact : IsCompact Set.univ)
(hUsc : UpperSemicontinuous fun (p : MeasureTheory.ProbabilityMeasure α) => mutualInformation p k)
: