InformationTheory.Shannon.Hoeffding.MinimizerExistence

Imports 13

Hoeffding tradeoff — sandwich discharge #

This file publishes the constructive full-support minimizer of klDivPmf · P₂ on the constraint set and the boundary achievability inequality.

Approach — constructive 3-case minimizer #

exists_hoeffding_minimizer_full_support supplies an explicit full-support minimizer Qstar of klDivPmf · P₂ on the constraint set, branching on alpha:

alpha = 0 : Qstar = P₁ (singleton constraint set)
0 < alpha ≤ klDivPmf P₂ P₁ : Qstar = hoeffdingTilt P₁ P₂ lam (IVT tilt)
klDivPmf P₂ P₁ ≤ alpha : Qstar = P₂ (boundary collapse)

All three cases are constructive, so Qstar full support is constructive — the abstract log-singularity gradient argument is avoided.

Constructive full-support minimizer (3-case) #

theorem

InformationTheory.Shannon.HoeffdingMinimizerExistence.exists_hoeffding_minimizer_full_support

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) :

∃ Qstar ∈ Chernoff.hoeffdingConstraintSet P₁ alpha, Chernoff.hoeffdingE2 P₁ P₂ alpha = CsiszarProjection.klDivPmf Qstar P₂ ∧ ∀ (a : α), 0 < Qstar a

Constructive 3-case minimizer: an explicit full-support Qstar realising hoeffdingE2 P₁ P₂ alpha = klDivPmf Qstar P₂, with Qstar ∈ K.

Used by

Achievability `E2 ≤ liminf rate` on the boundary regime #

The achievability inequality hoeffdingE2 P₁ P₂ alpha ≤ liminf rate holds unconditionally on the boundary regime klDivPmf P₂ P₁ ≤ alpha, where hoeffdingE2 = 0 (hoeffdingE2_eq_zero_at_alpha_ge_kl) and the inequality reduces to 0 ≤ liminf rate, i.e. the rate is non-negative (steinTypeII ≤ 1 ⇒ log ≤ 0). Outside the boundary it is not generally true — see the analysis below (it fails at alpha = 0, where E₂(0) = D(P₁‖P₂) > 0 = liminf rate).

theorem

InformationTheory.Shannon.HoeffdingMinimizerExistence.hoeffding_tradeoff_achievability_at_boundary

source

Chernoff.hoeffdingE2 P₁ P₂ alpha ≤ Filter.liminf (fun (n : ℕ) => -(1 / ↑n) * Real.log (HoeffdingTradeoff.steinTypeII_at_level_pmf P₁ P₂ n alpha)) Filter.atTop

achievability at the boundary (klDivPmf P₂ P₁ ≤ alpha, fully unconditional): there hoeffdingE2 = 0 ≤ liminf rate, since the rate is non-negative.

Used by

The fixed-`alpha` rate does not target the Hoeffding tradeoff curve #

A fixed-alpha Tendsto rate → hoeffdingE2 P₁ P₂ alpha does not hold: steinTypeII_at_level_pmf bakes in a constant Type-I level alpha, whereas the Hoeffding tradeoff curve E₂(alpha) is the limit only in the exponential-level regime alpha_n = exp(-n r). The fixed-alpha rate -(1/n) log steinTypeII_at_level_pmf converges to D(P₁‖P₂), not E₂(alpha). Two concrete contradictions:

alpha = 0: with full-support P₁, the only Type-I-exact-0 test is s = univ (every other Finset has ∑ ∏ P₁ < 1), so steinTypeII_at_level_pmf P₁ P₂ n 0 = 1 and rate n ≡ 0. But hoeffdingE2 P₁ P₂ 0 = klDivPmf P₁ P₂ = D(P₁‖P₂) > 0 in general. So rate → 0 ≠ E₂(0).
0 < alpha < 1: steinTypeII_at_level_pmf P₁ P₂ n alpha coincides with steinOptimalBeta (pmfToMeasure P₁) (pmfToMeasure P₂) n alpha (the pmf and measure β-sets agree on the finite alphabet), so by Stein's lemma rate n → D(P₁‖P₂) = E₂(0) > E₂(alpha).

Consequences for the two variational inequalities:

achievability hoeffdingE2 alpha ≤ liminf rate: holds whenever E₂(alpha) ≤ liminf rate. On the boundary klDivPmf P₂ P₁ ≤ alpha we have E₂(alpha) = 0 ≤ liminf rate unconditionally (hoeffding_tradeoff_achievability_at_boundary above). At alpha = 0 it is false (E₂(0) = D > 0 = liminf rate).
converse limsup rate ≤ hoeffdingE2 alpha: would require limsup rate ≤ E₂(alpha), contradicted at every alpha by the limits above.

The genuine statement of the tradeoff is the exponential-level hoeffding_tradeoff_exp (Hoeffding/TradeoffExp.lean).