ChannelCapacity.Discharged

Concrete density-regularity hypotheses for discharging the generic capacity theorem.

This module introduces Kernel.ContinuousPositiveDensity, a compact-Polish channel class whose rows admit a common strictly positive jointly continuous density. For that class it discharges the abstract WellConditionedForCapacity bundle (hRowAC, hFiniteRefKL, and hChainRule) and the compactness side of the ambient maximization argument, then derives the top-level theorem exists_unique_capacity_achieving_prior_discharged with no external bundle hypotheses.

Currently, upper semicontinuity of p ↦ mutualInformation p k is carried as a field of the concrete class rather than derived from the density hypotheses alone. The intended follow-up is a general theorem upperSemicontinuous_mutualInformation_of_continuousPositiveDensity proved from the density assumptions plus compactness of α × β.

The worked example lives in ChannelCapacity.DischargedExample: a positive full-rank Fin 2 channel with counting-measure reference, an explicit ContinuousPositiveDensity inhabitant, and a concrete application of exists_unique_capacity_achieving_prior_discharged.

structure ChannelCapacity.Kernel.ContinuousPositiveDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] (k : ProbabilityTheory.Kernel α β) (ν : MeasureTheory.Measure β) [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] : Type (max u_1 u_2)

A concrete compact-Polish regularity class for a Markov kernel: all rows have a common density with respect to ν, this density is jointly continuous, it is strictly positive, and the induced mutual-information functional is upper semicontinuous on priors.

• density : α → β → NNReal

  The common density of every row of k with respect to ν.

• continuous_density : Continuous (Function.uncurry self.density)
• eq_withDensity (a : α) : k a = ν.withDensity fun (b : β) => ↑(self.density a b)
• density_pos (a : α) (b : β) : 0 < self.density a b
• mutualInformation_usc : UpperSemicontinuous fun (p : MeasureTheory.ProbabilityMeasure α) => mutualInformation p k

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.row_eq_withDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) (a : α) : k a = ν.withDensity fun (b : β) => ↑(h.density a b)

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.row_absolutelyContinuous_ref {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) (a : α) : (k a).AbsolutelyContinuous ν

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.density_ne_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) (a : α) (b : β) : h.density a b ≠ 0

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.density_ennreal_pos {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) (a : α) (b : β) : 0 < ↑(h.density a b)

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.density_ennreal_ne_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) (a : α) (b : β) : ↑(h.density a b) ≠ 0

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.upperSemicontinuous_mutualInformation {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) : UpperSemicontinuous fun (p : MeasureTheory.ProbabilityMeasure α) => mutualInformation p k

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.exists_uniform_density_bounds {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] [CompactSpace β] [Nonempty α] [Nonempty β] (h : ContinuousPositiveDensity k ν) : ∃ (c : NNReal) (C : NNReal), 0 < c ∧ ∀ (a : α) (b : β), c ≤ h.density a b ∧ h.density a b ≤ C

A strictly positive jointly continuous density on a compact product has a positive uniform lower bound and a finite uniform upper bound.

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.klFun_le_sq_add_one {x B : ℝ} (hx : 0 ≤ x) (hB : x ≤ B) : InformationTheory.klFun x ≤ B ^ 2 + 1

noncomputable def ChannelCapacity.Kernel.ContinuousPositiveDensity.outputDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) : β → ENNReal

The density of the output prior outputPrior k p with respect to ν, given as the p-average of the row densities.

Equations

• h.outputDensity p b = ∫⁻ (a : α), ↑(h.density a b) ∂↑p

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.aemeasurable_outputDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [PolishSpace α] [PolishSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) : AEMeasurable (h.outputDensity p) ν

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.outputPrior_eq_withDensity_outputDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [PolishSpace α] [PolishSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) : ↑(outputPrior k p) = ν.withDensity (h.outputDensity p)

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.outputDensity_pos {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) (b : β) : 0 < h.outputDensity p b

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.ae_row_absolutelyContinuous_outputPrior {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] [PolishSpace α] [PolishSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) : ∀ᵐ (a : α) ∂↑p, (k a).AbsolutelyContinuous ↑(outputPrior k p)

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.row_absolutelyContinuous_outputPrior {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] [PolishSpace α] [PolishSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) (a : α) : (k a).AbsolutelyContinuous ↑(outputPrior k p)

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.row_klDiv_le_outputPrior_bound {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] [CompactSpace β] [PolishSpace α] [PolishSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) : ∃ (B : ENNReal), B ≠ ⊤ ∧ ∀ (a : α), InformationTheory.klDiv (k a) ↑(outputPrior k p) ≤ B

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.hFiniteRefKL_of_continuousPositiveDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] [CompactSpace β] [PolishSpace α] [PolishSpace β] [BorelSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) (p : MeasureTheory.ProbabilityMeasure α) (ν' : MeasureTheory.Measure β) (hRef : OutputMarginalReference k p ν') : InformationTheory.klDiv ((↑p).compProd k) ((↑p).compProd (ProbabilityTheory.Kernel.const α ν')) ≠ ⊤

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.hChainRule_of_outputMarginalReference {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [PolishSpace α] [BorelSpace α] (p : MeasureTheory.ProbabilityMeasure α) (ν' : MeasureTheory.Measure β) (hRef : OutputMarginalReference k p ν') : InformationTheory.klDiv (↑(jointLaw k p)) ((↑p).compProd (ProbabilityTheory.Kernel.const α ν')) = InformationTheory.klDiv ↑(jointLaw k p) ↑(independentJointLaw k p) + InformationTheory.klDiv (↑(outputPrior k p)) ν'

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.wellConditionedForCapacity_of_continuousPositiveDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] {k : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel k] [OpensMeasurableSpace α] {ν : MeasureTheory.Measure β} [CompactSpace α] [CompactSpace β] [PolishSpace α] [PolishSpace β] [BorelSpace α] [BorelSpace β] [OpensMeasurableSpace β] [MeasureTheory.IsFiniteMeasure ν] (h : ContinuousPositiveDensity k ν) : WellConditionedForCapacity k

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.univ_nonempty_probabilityMeasure {α : Type u_1} [MeasurableSpace α] [Nonempty α] : Set.univ.Nonempty

theorem ChannelCapacity.Kernel.ContinuousPositiveDensity.isCompact_univ_probabilityMeasure {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [CompactSpace α] [PolishSpace α] [BorelSpace α] : IsCompact Set.univ

theorem ChannelCapacity.exists_unique_capacity_achieving_prior_discharged {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [CompactSpace β] [PolishSpace α] [PolishSpace β] [BorelSpace α] [BorelSpace β] [OpensMeasurableSpace α] [OpensMeasurableSpace β] [MeasurableSpace.CountableOrCountablyGenerated α β] [Nonempty α] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (ν : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure ν] (hDensity : Kernel.ContinuousPositiveDensity k ν) (hInj : Kernel.InjectivePriorPushforward k) : ∃! p : MeasureTheory.ProbabilityMeasure α, mutualInformation p k = channelCapacity k