Documentation

LeanPool.ChannelCapacity.DischargedExample

ChannelCapacity.DischargedExample #

Worked example for the discharged capacity theorem.

This file builds a concrete positive full-rank Fin 2 → Fin 2 channel with counting-measure reference, instantiates Kernel.ContinuousPositiveDensity, and applies exists_unique_capacity_achieving_prior_discharged.

source
noncomputable def ChannelCapacity.DischargedExample.twoByTwoRowPMF :
Fin 2 → PMF (Fin 2)

The two rows of the 2 × 2 channel as probability mass functions on Fin 2 (mass 3/4 on the matching output, 1/4 on the other).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def ChannelCapacity.DischargedExample.twoByTwoRows (i : Fin 2) :
    MeasureTheory.ProbabilityMeasure (Fin 2)

    The two channel rows as probability measures on Fin 2.

    Equations
    Instances For
      source
      @[simp]
      theorem ChannelCapacity.DischargedExample.twoByTwoRows_apply_singleton (i j : Fin 2) :
      ↑(twoByTwoRows i) {j} = (twoByTwoRowPMF i) j
      source
      noncomputable def ChannelCapacity.DischargedExample.twoByTwoKernel :
      ProbabilityTheory.Kernel (Fin 2) (Fin 2)

      The 2 × 2 Markov kernel whose rows are twoByTwoRows.

      Equations
      Instances For
        source
        @[simp]
        theorem ChannelCapacity.DischargedExample.twoByTwoKernel_apply (i : Fin 2) :
        twoByTwoKernel i = ↑(twoByTwoRows i)
        source
        theorem ChannelCapacity.DischargedExample.twoByTwoKernel_apply_singleton (i j : Fin 2) :
        (twoByTwoKernel i) {j} = (twoByTwoRowPMF i) j
        source
        instance ChannelCapacity.DischargedExample.twoByTwoKernel_isMarkov :
        ProbabilityTheory.IsMarkovKernel twoByTwoKernel
        source
        noncomputable def ChannelCapacity.DischargedExample.twoByTwoDensity (i j : Fin 2) :
        NNReal

        The density of twoByTwoKernel with respect to the counting measure: 3/4 on the diagonal and 1/4 off it.

        Equations
        Instances For
          source
          @[simp]
          theorem ChannelCapacity.DischargedExample.twoByTwoDensity_apply (i j : Fin 2) :
          ↑(twoByTwoDensity i j) = (twoByTwoRowPMF i) j
          source
          theorem ChannelCapacity.DischargedExample.twoByTwo_rowMatrixFullRank :
          Kernel.RowMatrixFullRank twoByTwoKernel
          source
          theorem ChannelCapacity.DischargedExample.twoByTwo_injectivePriorPushforward :
          Kernel.InjectivePriorPushforward twoByTwoKernel
          source
          noncomputable def ChannelCapacity.DischargedExample.twoByTwoContinuousPositiveDensity :
          Kernel.ContinuousPositiveDensity twoByTwoKernel MeasureTheory.Measure.count

          The ContinuousPositiveDensity witness for twoByTwoKernel over the counting measure.

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