InformationTheory

InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.PmfLogBounds

source

Imports 10

δ-asymptotic pmfLog bounds for the smooth channel #

Part file split from ShannonTheoremMaxError. Provides pointwise pmfLog bounds for iidXs, iidYs, and jointSequence under iidAmbientMeasure p (Channel.smooth W δ), and analytic lemmas exists_N_log_sq_le_n / exists_N_log_sq_plus_const_le_n.

Pointwise pmfLog bounds and analytic growth lemmas #

theorem

InformationTheory.Shannon.ChannelCoding.pmfLog_iidXs_const_in_smooth

source
{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) (a : α) :
pmfLog (iidAmbientMeasure p (W.smooth δ)) iidXs a = pmfLog (iidAmbientMeasure p W) iidXs a

The pmfLog of iidXs is independent of W and δ, since the marginal is always p.

Used by
    theorem

    InformationTheory.Shannon.ChannelCoding.pmfLog_iidYs_bound_smooth

    source
    {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) (b : β) :
    |pmfLog (iidAmbientMeasure p (W.smooth δ)) iidYs b| ≤ Real.log (↑(Fintype.card β) / δ)

    |pmfLog (iidAmbientMeasure p (Channel.smooth W δ)) iidYs b| ≤ log(|β|/δ), via the output lower bound (W_smooth δ a).real {b} ≥ δ/|β|.

    Used by
      theorem

      InformationTheory.Shannon.ChannelCoding.pmfLog_jointSequence_bound_smooth

      source
      {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] {p_min : ℝ} (hp_min_pos : 0 < p_min) (hp_min_le : ∀ (a : α), p_min ≤ p.real {a}) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) (ab : α × β) :
      |pmfLog (iidAmbientMeasure p (W.smooth δ)) (jointSequence iidXs iidYs) ab| ≤ Real.log (↑(Fintype.card α) * ↑(Fintype.card β) / (p_min * δ))

      |pmfLog (iidAmbientMeasure p (Channel.smooth W δ)) (jointSequence iidXs iidYs) (a,b)| ≤ log(|α|·|β| / (p_min · δ)).

      Used by
        theorem

        InformationTheory.Shannon.ChannelCoding.exists_N_log_sq_le_n

        source
        (C : ℝ) (hC : 0 < C) :
        ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → C * Real.log (↑n + 1) ^ 2 + 1 ≤ ↑n

        For any C > 0, there exists N such that C · (log (n+1))² + 1 ≤ n for all n ≥ N.

        Used by
          theorem

          InformationTheory.Shannon.ChannelCoding.exists_N_log_sq_plus_const_le_n

          source
          (C D : ℝ) (hC : 0 < C) :
          ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → C * Real.log (↑n + 1) ^ 2 + D ≤ ↑n

          For any C > 0 and constant D, there exists N such that C * (log(n+1))² + D ≤ n for all n ≥ N.

          Used by