ChannelCapacity.Counterexample

A finite counterexample showing that row separation does not imply injective prior pushforward.

noncomputable def ChannelCapacity.Counterexample.asProbabilityMeasure {α : Type u_1} [MeasurableSpace α] (p : PMF α) : MeasureTheory.ProbabilityMeasure α

The probability measure induced by a probability mass function.

Equations

• ChannelCapacity.Counterexample.asProbabilityMeasure p = ⟨p.toMeasure, ⋯⟩

noncomputable def ChannelCapacity.Counterexample.uniformTriple {α : Type u_1} [MeasurableSpace α] (a b c : α) : MeasureTheory.ProbabilityMeasure α

The uniform probability measure supported on the three points a, b, and c.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ChannelCapacity.Counterexample.rowPMF : Fin 6 → PMF (Fin 3)

The six rows of the channel, one for each permutation of the values 1/2, 1/3, 1/6, as probability mass functions on Fin 3.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ChannelCapacity.Counterexample.permutationRows : Fin 6 → MeasureTheory.ProbabilityMeasure (Fin 3)

The six channel rows as probability measures on Fin 3.

Equations

• ChannelCapacity.Counterexample.permutationRows i = ChannelCapacity.Counterexample.asProbabilityMeasure (ChannelCapacity.Counterexample.rowPMF i)

@[simp]

theorem ChannelCapacity.Counterexample.permutationRows_apply_singleton (i : Fin 6) (y : Fin 3) : ↑(permutationRows i) {y} = (rowPMF i) y

noncomputable def ChannelCapacity.Counterexample.permutationKernel : ProbabilityTheory.Kernel (Fin 6) (Fin 3)

The Markov kernel Fin 6 → Fin 3 whose rows are the six permutation rows.

Equations

• ChannelCapacity.Counterexample.permutationKernel = ProbabilityTheory.Kernel.ofFunOfCountable fun (i : Fin 6) => ↑(ChannelCapacity.Counterexample.permutationRows i)

@[simp]

theorem ChannelCapacity.Counterexample.permutationKernel_apply (i : Fin 6) : permutationKernel i = (rowPMF i).toMeasure

theorem ChannelCapacity.Counterexample.permutationKernel_apply_singleton (i : Fin 6) (y : Fin 3) : (permutationKernel i) {y} = (rowPMF i) y

instance ChannelCapacity.Counterexample.permutationKernel_isMarkov : ProbabilityTheory.IsMarkovKernel permutationKernel

noncomputable def ChannelCapacity.Counterexample.prior₁ : MeasureTheory.ProbabilityMeasure (Fin 6)

The first prior: uniform on the inputs {0, 3, 4}.

Equations

• ChannelCapacity.Counterexample.prior₁ = ChannelCapacity.Counterexample.uniformTriple 0 3 4

noncomputable def ChannelCapacity.Counterexample.prior₂ : MeasureTheory.ProbabilityMeasure (Fin 6)

The second prior: uniform on the inputs {1, 2, 5}.

Equations

• ChannelCapacity.Counterexample.prior₂ = ChannelCapacity.Counterexample.uniformTriple 1 2 5

noncomputable def ChannelCapacity.Counterexample.uniformOutput : MeasureTheory.ProbabilityMeasure (Fin 3)

The uniform distribution on the output alphabet Fin 3.

Equations

• ChannelCapacity.Counterexample.uniformOutput = ChannelCapacity.Counterexample.uniformTriple 0 1 2

def ChannelCapacity.Counterexample.rowCode : Fin 6 → Fin 3 → ℚ

The rational values of each channel row, matching rowPMF entrywise.

Equations

• ChannelCapacity.Counterexample.rowCode 0 0 = 1 / 2
• ChannelCapacity.Counterexample.rowCode 0 1 = 1 / 3
• ChannelCapacity.Counterexample.rowCode 0 x✝ = 1 / 6
• ChannelCapacity.Counterexample.rowCode 1 0 = 1 / 2
• ChannelCapacity.Counterexample.rowCode 1 1 = 1 / 6
• ChannelCapacity.Counterexample.rowCode 1 x✝ = 1 / 3
• ChannelCapacity.Counterexample.rowCode 2 0 = 1 / 3
• ChannelCapacity.Counterexample.rowCode 2 1 = 1 / 2
• ChannelCapacity.Counterexample.rowCode 2 x✝ = 1 / 6
• ChannelCapacity.Counterexample.rowCode 3 0 = 1 / 6
• ChannelCapacity.Counterexample.rowCode 3 1 = 1 / 2
• ChannelCapacity.Counterexample.rowCode 3 x✝ = 1 / 3
• ChannelCapacity.Counterexample.rowCode 4 0 = 1 / 3
• ChannelCapacity.Counterexample.rowCode 4 1 = 1 / 6
• ChannelCapacity.Counterexample.rowCode 4 x✝ = 1 / 2
• ChannelCapacity.Counterexample.rowCode x✝ 0 = 1 / 6
• ChannelCapacity.Counterexample.rowCode x✝ 1 = 1 / 3
• ChannelCapacity.Counterexample.rowCode x✝¹ x✝ = 1 / 2

theorem ChannelCapacity.Counterexample.rowCode_injective : Function.Injective rowCode

def ChannelCapacity.Counterexample.prior₁Code : Fin 6 → ℚ

The rational weight vector of prior₁: mass 1/3 on each of 0, 3, 4.

Equations

• ChannelCapacity.Counterexample.prior₁Code 0 = 1 / 3
• ChannelCapacity.Counterexample.prior₁Code 3 = 1 / 3
• ChannelCapacity.Counterexample.prior₁Code 4 = 1 / 3
• ChannelCapacity.Counterexample.prior₁Code x✝ = 0

def ChannelCapacity.Counterexample.prior₂Code : Fin 6 → ℚ

The rational weight vector of prior₂: mass 1/3 on each of 1, 2, 5.

Equations

• ChannelCapacity.Counterexample.prior₂Code 1 = 1 / 3
• ChannelCapacity.Counterexample.prior₂Code 2 = 1 / 3
• ChannelCapacity.Counterexample.prior₂Code 5 = 1 / 3
• ChannelCapacity.Counterexample.prior₂Code x✝ = 0

def ChannelCapacity.Counterexample.outputCode (w : Fin 6 → ℚ) : Fin 3 → ℚ

The output weight vector obtained by pushing an input weight vector w through rowCode.

Equations

• ChannelCapacity.Counterexample.outputCode w y = ∑ x : Fin 6, w x * ChannelCapacity.Counterexample.rowCode x y

theorem ChannelCapacity.Counterexample.priorCode_counterexample : prior₁Code ≠ prior₂Code ∧ outputCode prior₁Code = outputCode prior₂Code

theorem ChannelCapacity.Counterexample.prior_ne : prior₁ ≠ prior₂

theorem ChannelCapacity.Counterexample.pushforward_prior₁ : Kernel.priorPushforward permutationKernel prior₁ = uniformOutput

theorem ChannelCapacity.Counterexample.pushforward_prior₂ : Kernel.priorPushforward permutationKernel prior₂ = uniformOutput

theorem ChannelCapacity.Counterexample.permutationKernel_not_injectivePriorPushforward : ¬Kernel.InjectivePriorPushforward permutationKernel

theorem ChannelCapacity.Counterexample.rowPMF_injective : Function.Injective rowPMF

noncomputable def ChannelCapacity.Counterexample.Toy.identityKernel : ProbabilityTheory.Kernel (Fin 3) (Fin 3)

The identity kernel on Fin 3, used as a positive control with injective pushforward.

Equations

• ChannelCapacity.Counterexample.Toy.identityKernel = ProbabilityTheory.Kernel.id

instance ChannelCapacity.Counterexample.Toy.instIsMarkovKernelFinOfNatNatIdentityKernel : ProbabilityTheory.IsMarkovKernel identityKernel