ChannelCapacity.NonDegeneracy

Correct non-degeneracy conditions for uniqueness in the prior variable.

• Kernel.priorPushforward
• Kernel.InjectivePriorPushforward
• Kernel.RowSeparating

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

The output prior map p ↦ Σ_x p(x) k(x, ·).

Equations

• ChannelCapacity.Kernel.priorPushforward k p = ChannelCapacity.outputPrior k p

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

Pairwise-distinct rows of a kernel. This is weaker than injective prior pushforward.

Equations

• ChannelCapacity.Kernel.RowSeparating k = ∀ ⦃a a' : α⦄, a ≠ a' → k a ≠ k a'

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

The correct non-degeneracy hypothesis for uniqueness in the prior variable.

Equations

• ChannelCapacity.Kernel.InjectivePriorPushforward k = Function.Injective (ChannelCapacity.Kernel.priorPushforward k)

def ChannelCapacity.Kernel.OutputMarginalReference {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.Measure β) : Prop

Reference measures needed by the strict-concavity proof: output marginals of priors that dominate the given prior.

Equations

• ChannelCapacity.Kernel.OutputMarginalReference k p ν = ∃ (q : MeasureTheory.ProbabilityMeasure α), (↑p).AbsolutelyContinuous ↑q ∧ ν = ↑(ChannelCapacity.outputPrior k q)

structure ChannelCapacity.Kernel.WellConditionedForCapacity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] : Prop

Measure-theoretic non-degeneracy bundle for the capacity theorem. Each prior's rows are absolutely continuous with respect to the induced output marginal, and the joint KL divergence is finite against the output-marginal references used in the strict-concavity argument. The chain-rule field is the extra bridge needed for strict concavity: it isolates the positive output-marginal correction term against an arbitrary dominating reference.

• hRowAC (p : MeasureTheory.ProbabilityMeasure α) : ∀ᵐ (x : α) ∂↑p, (k x).AbsolutelyContinuous ↑(outputPrior k p)
• hFiniteRefKL (p : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.Measure β) : OutputMarginalReference k p ν → InformationTheory.klDiv ((↑p).compProd k) ((↑p).compProd (ProbabilityTheory.Kernel.const α ν)) ≠ ⊤
• hChainRule (p : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.Measure β) : 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)) ν

@[simp]

theorem ChannelCapacity.Kernel.priorPushforward_dirac {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (a : α) : priorPushforward k (MeasureTheory.diracProba a) = ⟨k a, ⋯⟩

theorem ChannelCapacity.Kernel.priorPushforward_convexCombination {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p q : MeasureTheory.ProbabilityMeasure α) (t : NNReal) (ht : t ≤ 1) : priorPushforward k (ProbabilityMeasure.convexCombination p q t ht) = ProbabilityMeasure.convexCombination (priorPushforward k p) (priorPushforward k q) t ht

@[simp]

theorem ChannelCapacity.Kernel.priorPushforward_id {α : Type u_1} [MeasurableSpace α] (p : MeasureTheory.ProbabilityMeasure α) : priorPushforward ProbabilityTheory.Kernel.id p = p

theorem ChannelCapacity.Kernel.id_injectivePriorPushforward {α : Type u_1} [MeasurableSpace α] : InjectivePriorPushforward ProbabilityTheory.Kernel.id

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