InformationTheory.Shannon.Hoeffding.BoundaryMinimizer

Imports 5

Hoeffding tradeoff — sandwich body completion #

This file publishes the IsHoeffdingMinimizerFullSupport predicate plus the boundary full-support discharges (α = 0 and α ≥ klDivPmf P₂ P₁) used by the constructive minimizer of Hoeffding/MinimizerExistence.lean and the exponential-level closure hoeffding_tradeoff_exp (Hoeffding/TradeoffExp.lean).

The fixed-alpha rate targets D(P₁‖P₂), not the Hoeffding tradeoff curve E₂(alpha); the genuine statement is hoeffding_tradeoff_exp.

Structure #

The full-support predicate IsHoeffdingMinimizerFullSupport wraps the claim ∀ a, 0 < Qstar a so downstream lemmas take a single named assumption. The general-alpha discharge of this predicate (full support of any Csiszár-Pythagoras minimizer of klDivPmf · P₂ on K) requires a log-singularity gradient argument and is supplied externally via the constructive minimizer.

For boundary values of α the full-support claim is fully discharged from existing Mathlib + InformationTheory API:

α = 0: klDivPmf Q P₁ ≤ 0 combined with klDivPmf_nonneg forces klDivPmf Q P₁ = 0. By klDivPmf_eq_zero_iff_pmf, Q = P₁. Hence the sole K-element is P₁, full-support by hP₁_pos.
α ≥ klDivPmf P₂ P₁: P₂ ∈ K (constraint satisfied). Combined with hoeffdingE2_nonneg and klDivPmf P₂ P₂ = 0, the infimum is 0 and Qstar = P₂ realises it with full support by hP₂_pos. (Different minimizers may exist, but a full-support one is always available.)

What this file publishes #

IsHoeffdingMinimizerFullSupport (Prop predicate, abbrev form): wraps the claim ∀ a, 0 < Qstar a.
hoeffdingE2_minimizer_at_boundary_alpha_zero (full discharge): at α = 0, every Qstar ∈ K (with K = {P₁} in this case) is full-support, i.e. IsHoeffdingMinimizerFullSupport holds for any such Qstar.
hoeffdingE2_minimizer_at_boundary_alpha_ge_kl (full discharge, witness form): at α ≥ klDivPmf P₂ P₁, the witness Qstar := P₂ realises the minimum and is full-support.
hoeffding_minimizer_ge_via_predicate: variant of hoeffding_minimizer_ge taking IsHoeffdingMinimizerFullSupport instead of raw hQs_pos.

IsHoeffdingMinimizerFullSupport is a thin alias (definitional unfolding to ∀ a, 0 < Qstar a); callers construct it either from a raw pointwise positivity proof or from the boundary discharges above. The boundary discharges assume hP₁_pos / hP₂_pos (full-support source pmfs); the α = 0 case additionally needs klDivPmf_eq_zero_iff_pmf from MaxEntropy/Constrained.lean.

Full-support predicate #

def

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.IsHoeffdingMinimizerFullSupport

source

{α : Type u_1} (Qstar : α → ℝ) :

Prop

The claim ∀ a, 0 < Qstar a wrapped as a Prop so downstream lemmas can take a single named assumption instead of an unstructured ∀ a, 0 < Qstar a.

The general-α discharge of this predicate (any minimizer of klDivPmf · P₂ on hoeffdingConstraintSet P₁ alpha) requires a HasDerivAt + Real.log singularity computation on the directional derivative of klDivPmf · P₂ at a 0-atom.

For boundary values of α (namely α = 0 and α ≥ klDivPmf P₂ P₁), the predicate is fully discharged from existing Mathlib + InformationTheory API.

Equations

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.IsHoeffdingMinimizerFullSupport Qstar = ∀ (a : α), 0 < Qstar a

Instances For

Used by

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.IsHoeffdingMinimizerFullSupport.of_pos

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Qstar : α → ℝ} (h : ∀ (a : α), 0 < Qstar a) :

IsHoeffdingMinimizerFullSupport Qstar

Trivial direct constructor from raw pointwise positivity.

Used by

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.IsHoeffdingMinimizerFullSupport.pos

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Qstar : α → ℝ} (h : IsHoeffdingMinimizerFullSupport Qstar) (a : α) :

0 < Qstar a

Trivial direct destructor to raw pointwise positivity.

Used by

Boundary full discharge #

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.hoeffdingConstraintSet_eq_singleton_at_alpha_zero

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) :

Chernoff.hoeffdingConstraintSet P₁ 0 = {P₁}

Boundary α = 0 full discharge: at α = 0, every Q ∈ hoeffdingConstraintSet P₁ 0 equals P₁.

klDivPmf Q P₁ ≤ 0 (constraint) + klDivPmf_nonneg ⇒ klDivPmf Q P₁ = 0. By klDivPmf_eq_zero_iff_pmf (full-support P₁), Q = P₁.

Used by

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.P₂_mem_hoeffdingConstraintSet

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₂_sum : ∑ a : α, P₂ a = 1) {alpha : ℝ} (h_alpha_ge : CsiszarProjection.klDivPmf P₂ P₁ ≤ alpha) :

P₂ ∈ Chernoff.hoeffdingConstraintSet P₁ alpha

Boundary α ≥ klDivPmf P₂ P₁ full discharge: when α is at least klDivPmf P₂ P₁, then P₂ ∈ hoeffdingConstraintSet P₁ alpha.

Used by

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.hoeffdingE2_eq_zero_at_alpha_ge_kl

source

Chernoff.hoeffdingE2 P₁ P₂ alpha = 0

E2 collapse: when α ≥ klDivPmf P₂ P₁, the hoeffdingE2 value equals 0, since P₂ itself realises the minimum.

Used by

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.hoeffdingE2_minimizer_at_boundary_alpha_ge_kl

source

∃ Qstar ∈ Chernoff.hoeffdingConstraintSet P₁ alpha, Chernoff.hoeffdingE2 P₁ P₂ alpha = CsiszarProjection.klDivPmf Qstar P₂ ∧ IsHoeffdingMinimizerFullSupport Qstar

Predicate form, witness: at α ≥ klDivPmf P₂ P₁, the witness Qstar := P₂ lies in K, realises hoeffdingE2 = klDivPmf P₂ P₂ = 0, and is full-support (by hP₂_pos).

Used by

Pythagoras-based minimizer integration via predicate #

theorem

InformationTheory.Shannon.HoeffdingBoundaryMinimizer.hoeffding_minimizer_ge_via_predicate

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 : α → ℝ} (hQs_mem : Qstar ∈ Chernoff.hoeffdingConstraintSet P₁ alpha) (hQs_full : IsHoeffdingMinimizerFullSupport Qstar) (hQs_min : Chernoff.hoeffdingE2 P₁ P₂ alpha = CsiszarProjection.klDivPmf Qstar P₂) {P : α → ℝ} (hP_mem : P ∈ Chernoff.hoeffdingConstraintSet P₁ alpha) (hP_pos : ∀ (a : α), 0 < P a) :

CsiszarProjection.klDivPmf Qstar P₂ ≤ CsiszarProjection.klDivPmf P P₂

hoeffding_minimizer_ge via predicate: variant of HoeffdingTradeoff.hoeffding_minimizer_ge taking IsHoeffdingMinimizerFullSupport instead of raw hQs_pos.

Used by