InformationTheory

InformationTheory.Shannon.Hoeffding.TradeoffExp

source

Imports 10

Hoeffding tradeoff — exponential-level redefinition #

Unlike the constant-α steinTypeII_at_level_pmf, the operational quantity here is defined at the exponential level — the acceptance region is the KL-sublevel set of empirical types E_r n = {c | klDivIndex c n P₁ ≤ r} — and the resulting Type-II error converges to hoeffdingE2 P₁ P₂ r. The headline hoeffding_tradeoff_exp holds on the interior 0 < r < klDivPmf P₂ P₁.

Implementation notes #

The two directions are proved separately:

  • the converse (limsup) via sanov_ldp_upper_bound on the non-perturbed minimizer Qstar;
  • the achievability (liminf) via sanov_ldp_lower_bound_pointwise on a perturbation Qstar_ε = (1-ε)·Qstar + ε·P₁, followed by ε → 0.

The subtlety driving the perturbation is the active-boundary obstruction: the interior minimizer Qstar lies on the active boundary klDivPmf Qstar P₁ = r, so its rounded type converges to the boundary of the closed sublevel set E_r n = {klDivIndex ≤ r} and is not provably eventually inside. Enlarging E_r with a rounding margin would restore achievability but break the minimizer premise (a margin point may beat Qstar), so the two requirements conflict at the active constraint. Pushing Qstar slightly toward P₁ lands strictly inside the constraint (by convexity of klDivPmf · P₁ and klDivPmf P₁ P₁ = 0), restoring strict-interior eventual membership; the per-perturbation achievability bound is then carried to the limit by ε → 0 continuity.

E_r acceptance region + steinTypeII_exp definition #

noncomputable def

InformationTheory.Shannon.HoeffdingTradeoffExp.E_r

source
{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] (P₁ : α → ℝ) (hP₁_nn : ∀ (a : α), 0 ≤ P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (n : ℕ) (r : ℝ) :
Finset (TypeCountIndex α n)

Exponential-level acceptance region: valid empirical types (∑ c = n) whose KL divergence from P₁ is within r (a closed KL-sublevel set, indexed by TypeCountIndex). The ∑ c = n clause restricts to genuine empirical pmfs c/n; types with ∑ c ≠ n have an empty type class (typeClassByCount_empty_of_sum_ne) so the acceptance region is unchanged.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Used by
      noncomputable def

      InformationTheory.Shannon.HoeffdingTradeoffExp.steinTypeII_exp

      source
      {α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] (P₁ P₂ : α → ℝ) (hP₁_nn : ∀ (a : α), 0 ≤ P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_nn : ∀ (a : α), 0 ≤ P₂ a) (hP₂_sum : ∑ a : α, P₂ a = 1) (n : ℕ) (r : ℝ) :
      ℝ

      Type-II error of the exponential-level test: the P₂ⁿ mass of the acceptance region ⋃_{c ∈ E_r} T_c.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Used by
          theorem

          InformationTheory.Shannon.HoeffdingTradeoffExp.mem_E_r_iff

          source
          {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ : α → ℝ) (hP₁_nn : ∀ (a : α), 0 ≤ P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (n : ℕ) (r : ℝ) (c : TypeCountIndex α n) :
          c ∈ E_r P₁ hP₁_nn hP₁_sum n r ↔ 0 < n ∧ ∑ a : α, ↑(c a) = n ∧ klDivIndex (fun (a : α) => ↑(c a)) n (HoeffdingTradeoff.pmfToMeasure P₁ hP₁_nn hP₁_sum) ≤ r
          Used by

            KL bridges (count-0-tolerant) #

            theorem

            InformationTheory.Shannon.HoeffdingTradeoffExp.klDivPmf_eq_log_diff_sum_of_Q_pos

            source
            {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {P Q : α → ℝ} (hP_nn : ∀ (a : α), 0 ≤ P a) (hP_sum : ∑ a : α, P a = 1) (hQ_sum : ∑ a : α, Q a = 1) (hQ_pos : ∀ (a : α), 0 < Q a) :
            CsiszarProjection.klDivPmf P Q = ∑ a : α, P a * (Real.log (P a) - Real.log (Q a))

            klDivPmf log-diff form tolerant of count-0 atoms in P: requires only Q full support (and both sum to 1), not P full support. The P a = 0 term matches on both sides (Q a vs 0 + Q a - 0).

            Used by
              theorem

              InformationTheory.Shannon.HoeffdingTradeoffExp.klDivIndex_eq_klDivPmf_empirical

              source
              {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) (hQ_pos : ∀ (a : α), 0 < Q.real {a}) (hQ_sum : ∑ a : α, Q.real {a} = 1) {n : ℕ} (hn : 0 < n) {c : α → ℕ} (hc_sum : ∑ a : α, c a = n) :
              klDivIndex c n Q = CsiszarProjection.klDivPmf (fun (a : α) => ↑(c a) / ↑n) fun (a : α) => Q.real {a}

              klDivIndex as klDivPmf of the empirical pmf (count-0 tolerant): for ∑ c = n, n > 0, Q full support, klDivIndex c n Q = klDivPmf (c · / n) (Q.real ∘ singleton).

              Used by

                h_in_E from rounded-type KL convergence #

                theorem

                InformationTheory.Shannon.HoeffdingTradeoffExp.roundedTypeIndex_mem_E_r_eventually

                source
                {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) {Qstar : α → ℝ} (hQs_sum : ∑ a : α, Qstar a = 1) (hQs_nn : ∀ (a : α), 0 ≤ Qstar a) {r : ℝ} (h_strict : CsiszarProjection.klDivPmf Qstar P₁ < r) :
                ∀ᶠ (n : ℕ) in Filter.atTop, roundedTypeIndex Qstar n ∈ E_r P₁ ⋯ hP₁_sum n r

                Eventually accepted: the rounded type of a strict-interior Qstar (klDivPmf Qstar P₁ < r) lands in E_r n for all large n.

                Used by

                  Perturbation toward P₁ #

                  noncomputable def

                  InformationTheory.Shannon.HoeffdingTradeoffExp.Qstar_perturb

                  source
                  {α : Type u_1} (Qstar P₁ : α → ℝ) (ε : ℝ) :
                  α → ℝ

                  Perturbed minimizer Qstar_ε := (1-ε)·Qstar + ε·P₁.

                  Equations
                  Instances For
                    Used by
                      theorem

                      InformationTheory.Shannon.HoeffdingTradeoffExp.Qstar_perturb_nonneg

                      source
                      {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Qstar P₁ : α → ℝ} (hQs_nn : ∀ (a : α), 0 ≤ Qstar a) (hP₁_nn : ∀ (a : α), 0 ≤ P₁ a) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (a : α) :
                      0 ≤ Qstar_perturb Qstar P₁ ε a
                      Used by
                        theorem

                        InformationTheory.Shannon.HoeffdingTradeoffExp.Qstar_perturb_sum

                        source
                        {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Qstar P₁ : α → ℝ} (hQs_sum : ∑ a : α, Qstar a = 1) (hP₁_sum : ∑ a : α, P₁ a = 1) (ε : ℝ) :
                        ∑ a : α, Qstar_perturb Qstar P₁ ε a = 1
                        Used by
                          theorem

                          InformationTheory.Shannon.HoeffdingTradeoffExp.klDivPmf_perturb_lt

                          source
                          {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) {Qstar : α → ℝ} (hQs_sum : ∑ a : α, Qstar a = 1) (hQs_nn : ∀ (a : α), 0 ≤ Qstar a) {r : ℝ} (hr_pos : 0 < r) (h_le : CsiszarProjection.klDivPmf Qstar P₁ ≤ r) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
                          CsiszarProjection.klDivPmf (Qstar_perturb Qstar P₁ ε) P₁ < r

                          Strict interior of the perturbation: by convexity of klDivPmf · P₁ (klDivPmf_strictConvexOn_left) plus klDivPmf P₁ P₁ = 0, a tiny push toward P₁ strictly lowers the constraint value below the active value klDivPmf Qstar P₁ ≤ r.

                          Used by
                            theorem

                            InformationTheory.Shannon.HoeffdingTradeoffExp.klDivPmf_perturb_tendsto

                            source
                            {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₂_pos : ∀ (a : α), 0 < P₂ a) {Qstar : α → ℝ} :
                            Filter.Tendsto (fun (ε : ℝ) => CsiszarProjection.klDivPmf (Qstar_perturb Qstar P₁ ε) P₂) (nhdsWithin 0 (Set.Ioi 0)) (nhds (CsiszarProjection.klDivPmf Qstar P₂))

                            ε-continuity of klDivPmf Qstar_ε P₂: as ε → 0, the perturbed KL divergence converges to klDivPmf Qstar P₂ (continuity of klDivPmf · P₂).

                            Used by

                              h_minimizer premise #

                              theorem

                              InformationTheory.Shannon.HoeffdingTradeoffExp.hoeffding_exp_minimizer

                              source
                              {α : Type u_1} [Fintype α] [DecidableEq α] [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) {r : ℝ} (_h_r_pos : 0 < r) {Qstar : α → ℝ} (hQs_mem : Qstar ∈ Chernoff.hoeffdingConstraintSet P₁ r) (hQs_pos : ∀ (a : α), 0 < Qstar a) (hQs_min : Chernoff.hoeffdingE2 P₁ P₂ r = CsiszarProjection.klDivPmf Qstar P₂) (n : ℕ) (c : TypeCountIndex α n) :
                              c ∈ E_r P₁ ⋯ hP₁_sum n r → (klDivSumForm_ofVec Qstar fun (a : α) => (HoeffdingTradeoff.pmfToMeasure P₂ ⋯ hP₂_sum).real {a}) ≤ klDivIndex (fun (a : α) => ↑(c a)) n (HoeffdingTradeoff.pmfToMeasure P₂ ⋯ hP₂_sum)

                              Minimizer premise: for every c ∈ E_r n, the minimizer value klDivSumForm_ofVec Qstar (P₂.real ∘ singleton) lower-bounds klDivIndex c n P₂. Holds for the strict-interior Qstar.

                              Used by

                                Achievability via perturbation #

                                theorem

                                InformationTheory.Shannon.HoeffdingTradeoffExp.hoeffding_exp_liminf_perturb

                                source
                                {α : Type u_1} [Fintype α] [DecidableEq α] [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) {r : ℝ} (h_r_pos : 0 < r) {Qstar : α → ℝ} (hQs_sum : ∑ a : α, Qstar a = 1) (hQs_nn : ∀ (a : α), 0 ≤ Qstar a) (h_le : CsiszarProjection.klDivPmf Qstar P₁ ≤ r) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
                                -CsiszarProjection.klDivPmf (Qstar_perturb Qstar P₁ ε) P₂ ≤ Filter.liminf (fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.pi fun (x : Fin n) => HoeffdingTradeoff.pmfToMeasure P₂ ⋯ hP₂_sum) (⋃ c ∈ E_r P₁ ⋯ hP₁_sum n r, typeClassByCount fun (a : α) => ↑(c a))).toReal) Filter.atTop

                                Achievability rate bound at perturbation level ε: for the strictly interior perturbed minimizer Qstar_ε, -klDivPmf Qstar_ε P₂ ≤ liminf (rate).

                                Used by

                                  Helpers for the headline proof #

                                  Headline #

                                  theorem

                                  InformationTheory.Shannon.HoeffdingTradeoffExp.hoeffding_tradeoff_exp

                                  source
                                  {α : Type u_1} [Fintype α] [DecidableEq α] [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) {r : ℝ} (h_r_pos : 0 < r) (_h_r_lt : r < CsiszarProjection.klDivPmf P₂ P₁) :
                                  Filter.Tendsto (fun (n : ℕ) => -(1 / ↑n) * Real.log (steinTypeII_exp P₁ P₂ ⋯ hP₁_sum ⋯ hP₂_sum n r)) Filter.atTop (nhds (Chernoff.hoeffdingE2 P₁ P₂ r))

                                  Hoeffding's tradeoff (exponential level, interior): the optimal Type-II error exponent of the exponential-level test converges to hoeffdingE2 P₁ P₂ r on the interior 0 < r < klDivPmf P₂ P₁.

                                  The active-boundary obstruction — the realizing minimizer Qstar sits on the active boundary klDivPmf Qstar P₁ = r, so its rounded type straddles the closed sublevel set E_r n = {klDivIndex ≤ r} — is resolved by a perturbation argument (see the module-level implementation notes).

                                  Used by