InformationTheory

InformationTheory.Shannon.Hoeffding.Sandwich

source

Imports 5

Hoeffding tradeoff — rate boundedness #

This file publishes the boundedness lemmas for the fixed-alpha Type-II rate sequence -(1/n) log (steinTypeII_at_level_pmf P₁ P₂ n alpha). They are unconditional facts about the rate sequence, and hoeffding_rate_isBoundedUnder_le is consumed by hoeffding_tradeoff_achievability_at_boundary (Hoeffding/MinimizerExistence.lean).

The fixed-alpha rate converges to D(P₁‖P₂), not to the Hoeffding tradeoff curve E₂(alpha); the genuine statement of the tradeoff is hoeffding_tradeoff_exp at the exponential level (Hoeffding/TradeoffExp.lean).

What this file publishes #

  • hoeffding_rate_isBoundedUnder_ge: the rate sequence -(1/n) log steinTypeII_at_level_pmf is bounded below (by 0) along atTop, derived from steinTypeII_at_level_pmf_le_one + Real.log_nonpos.

  • hoeffding_rate_isBoundedUnder_le: the rate sequence is bounded above by M := -log p₂_min + |log(1 - alpha)| along atTop, derived from a lower bound steinTypeII ≥ (1 - alpha) · p₂_min^n obtained by Type I constraint + minimum P₂ atom (under alpha < 1, which avoids the log 0 corner case).

The pmf form α → ℝ is kept throughout.

IsBoundedUnder (· ≥ ·): rate bounded below #

theorem

InformationTheory.Shannon.HoeffdingSandwich.hoeffding_rate_isBoundedUnder_ge

source
{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) (hP₂_nn : ∀ (a : α), 0 ≤ P₂ a) {alpha : ℝ} (h_alpha_nn : 0 ≤ alpha) :
Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => -(1 / ↑n) * Real.log (HoeffdingTradeoff.steinTypeII_at_level_pmf P₁ P₂ n alpha)

The rate sequence -(1/n) log (steinTypeII_at_level_pmf P₁ P₂ n alpha) is bounded below by 0 along atTop.

Used by

    IsBoundedUnder (· ≤ ·): rate bounded above #

    theorem

    InformationTheory.Shannon.HoeffdingSandwich.steinTypeII_at_level_pmf_ge_pow_pmin

    source
    {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) {alpha : ℝ} (h_alpha_nn : 0 ≤ alpha) (_h_alpha_lt : alpha < 1) (n : ℕ) {a₀ : α} (ha₀ : ∀ (a : α), P₂ a₀ ≤ P₂ a) :
    (1 - alpha) * P₂ a₀ ^ n ≤ HoeffdingTradeoff.steinTypeII_at_level_pmf P₁ P₂ n alpha

    Lower bound on steinTypeII_at_level_pmf when alpha < 1 under full support P₁, P₂ > 0: (1 - alpha) · (P₂ a₀)^n ≤ steinTypeII, where a₀ is a minimal P₂ atom.

    Used by
      theorem

      InformationTheory.Shannon.HoeffdingSandwich.hoeffding_rate_isBoundedUnder_le

      source
      {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) {alpha : ℝ} (h_alpha_nn : 0 ≤ alpha) (h_alpha_lt : alpha < 1) :
      Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => -(1 / ↑n) * Real.log (HoeffdingTradeoff.steinTypeII_at_level_pmf P₁ P₂ n alpha)

      The rate sequence is bounded above along atTop under full support + alpha < 1. The uniform upper bound is M := -log p₂_min - log(1 - alpha) / n, which is bounded by -log p₂_min + |log(1 - alpha)| for n ≥ 1.

      Used by