InformationTheory

InformationTheory.Shannon.AEP.Basic.Core

source

Imports 15

I.i.d. sequence and block joint random variable #

def

InformationTheory.Shannon.jointRV

source
{Ω : Type u_1} {α : Type u_2} (Xs : ℕ → Ω → α) (n : ℕ) :
Ω → Fin n → α

Block joint random variable: jointRV Xs n ω = (Xs 0 ω, Xs 1 ω, …, Xs (n-1) ω).

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.jointRV_apply

      source
      @[simp]
      {Ω : Type u_1} {α : Type u_2} (Xs : ℕ → Ω → α) (n : ℕ) (ω : Ω) (i : Fin n) :
      jointRV Xs n ω i = Xs (↑i) ω
      Used by
        theorem

        InformationTheory.Shannon.measurable_jointRV

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (n : ℕ) :
        Measurable (jointRV Xs n)
        Used by

          Probability AEP #

          The per-symbol log-likelihood is −Real.log ((μ.map (Xs 0)).real {Xs i ω}). It is factored through the alphabet-side function pmfLog μ Xs : α → ℝ so that logLikelihood μ Xs i ω = pmfLog μ Xs (Xs i ω). This shape lets IdentDistrib (Xs i) (Xs 0) and IndepFun (Xs i) (Xs j) lift to the logLikelihood sequence by composition with the (always-measurable, finite-domain) pmfLog.

          noncomputable def

          InformationTheory.Shannon.pmfLog

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) :
          α → ℝ

          Alphabet-side −log p(x) function (independent of i).

          Equations
          Instances For
            Used by
              theorem

              InformationTheory.Shannon.measurable_pmfLog

              source
              {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) :
              Measurable (pmfLog μ Xs)
              Used by
                noncomputable def

                InformationTheory.Shannon.logLikelihood

                source
                {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (i : ℕ) :
                Ω → ℝ

                Per-symbol log-likelihood: (−log P(Xs i ω)).

                Equations
                Instances For
                  Used by
                    theorem

                    InformationTheory.Shannon.logLikelihood_eq_comp

                    source
                    {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (i : ℕ) :
                    logLikelihood μ Xs i = pmfLog μ Xs ∘ Xs i
                    Used by
                      theorem

                      InformationTheory.Shannon.measurable_logLikelihood

                      source
                      {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (i : ℕ) :
                      Measurable (logLikelihood μ Xs i)
                      Used by
                        theorem

                        InformationTheory.Shannon.integrable_logLikelihood

                        source
                        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (i : ℕ) :
                        MeasureTheory.Integrable (logLikelihood μ Xs i) μ
                        Used by
                          theorem

                          InformationTheory.Shannon.integral_logLikelihood_zero

                          source
                          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) :
                          ∫ (ω : Ω), logLikelihood μ Xs 0 ω ∂μ = entropy μ (Xs 0)

                          ∫ logLikelihood μ Xs 0 ∂μ = entropy μ (Xs 0).

                          Used by
                            theorem

                            InformationTheory.Shannon.identDistrib_logLikelihood

                            source
                            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (i : ℕ) :
                            ProbabilityTheory.IdentDistrib (logLikelihood μ Xs i) (logLikelihood μ Xs 0) μ μ
                            Used by
                              theorem

                              InformationTheory.Shannon.indepFun_logLikelihood

                              source
                              {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) :
                              Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (logLikelihood μ Xs i) (logLikelihood μ Xs j) μ
                              Used by
                                theorem

                                InformationTheory.Shannon.aep_ae

                                source
                                {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) :
                                ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, logLikelihood μ Xs i ω) / ↑n) Filter.atTop (nhds (entropy μ (Xs 0)))

                                Asymptotic equipartition property (almost-sure form): for an i.i.d. discrete sequence Xs : ℕ → Ω → α with finite alphabet α, the empirical entropy estimator (1/n) ∑ i, (−log P(Xs i ω)) converges almost surely to the entropy H(Xs 0).

                                Used by
                                  theorem

                                  InformationTheory.Shannon.aep_inProbability

                                  source
                                  {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) {ε : ℝ} (hε : 0 < ε) :
                                  Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | ε ≤ |(∑ i ∈ Finset.range n, logLikelihood μ Xs i ω) / ↑n - entropy μ (Xs 0)|}) Filter.atTop (nhds 0)

                                  Asymptotic equipartition property (in probability): the empirical entropy estimator converges to entropy μ (Xs 0) in probability.

                                  Used by

                                    Typical set T_ε^n #

                                    noncomputable def

                                    InformationTheory.Shannon.typicalSet

                                    source
                                    {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε : ℝ) :
                                    Set (Fin n → α)

                                    Typical set: blocks x : Fin n → α whose empirical entropy is within ε of the true entropy H(Xs 0).

                                    Equations
                                    Instances For
                                      Used by
                                        theorem

                                        InformationTheory.Shannon.mem_typicalSet_iff

                                        source
                                        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε : ℝ) (x : Fin n → α) :
                                        x ∈ typicalSet μ Xs n ε ↔ |(∑ i : Fin n, pmfLog μ Xs (x i)) / ↑n - entropy μ (Xs 0)| < ε
                                        Used by
                                          theorem

                                          InformationTheory.Shannon.measurableSet_typicalSet

                                          source
                                          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε : ℝ) :
                                          MeasurableSet (typicalSet μ Xs n ε)

                                          Measurability of the typical set.

                                          Used by
                                            theorem

                                            InformationTheory.Shannon.typicalSet_card_le

                                            source
                                            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (n : ℕ) {ε : ℝ} (_hε : 0 < ε) :
                                            ↑⋯.toFinset.card ≤ Real.exp (↑n * (entropy μ (Xs 0) + ε))

                                            Size bound: |T_ε^n| ≤ exp (n · (H + ε)). The bound is stated with Real.exp rather than 2^x to avoid the log 2 plumbing; the textbook form follows by re-basing the logarithm.

                                            The full-support hypothesis hpos is required because, under the Mathlib Real.log 0 = 0 convention, a typical block containing an out-of-support point cannot be evaluated by the sum (for P(x_i) = 0 we get pmfLog x i = 0, so exp(-∑ pmfLog) is strictly larger than P^n(x) = 0 and fails as a lower bound), so [∀ x, P(x) > 0] is taken as an extra hypothesis.

                                            Used by
                                              theorem

                                              InformationTheory.Shannon.typicalSet_prob_tendsto_one

                                              source
                                              {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) {ε : ℝ} (hε : 0 < ε) :
                                              Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | jointRV Xs n ω ∈ typicalSet μ Xs n ε}) Filter.atTop (nhds 1)

                                              Typicality probability: P(jointRV Xs n ∈ T_ε^n) → 1.

                                              See also aep_inProbability.

                                              Used by