InformationTheory

InformationTheory.Shannon.Hoeffding.Tilt

source

Imports 3

Hoeffding tradeoff — interior gradient body (Lagrange tilt) #

For the interior regime 0 < α < klDivPmf P₂ P₁, the Csiszár I-projection of P₂ onto the constraint set K(α) is the one-parameter exponential tilt

  `Qstar a = c(λ) · P₁ a ^ (1 - λ) · P₂ a ^ λ`,

which is exactly Chernoff.chernoffMediator P₁ P₂ λ. This file reuses that family (no new definition) and proves its defining gradient property:

  `log (Qstar a) - (1 - λ) · log (P₁ a) - λ · log (P₂ a)`  is constant in a
  (it equals `-log Z(λ)`).

This is the Lagrange first-order condition ∇[D(Q‖P₂) + μ D(Q‖P₁)] = const: the log-likelihood ratio of the tilt against the geometric mean of P₁, P₂ is flat across the alphabet. The constant-log-ratio identity is a pure-algebra fact about rpow.

The interior characterization decomposes into two sub-predicates:

  • IsKLGradientHyp P₁ P₂ alpha lam Qstar — discharged for the tilt Qstar = chernoffMediator P₁ P₂ lam: the constant-log-ratio stationarity above, plus full support and Qstar ∈ stdSimplex.

  • IsHoeffdingLagrangeHyp P₁ P₂ alpha lam — the tilt at lam matches the constraint (klDivPmf (tilt) P₁ ≤ alpha) and realises the infimum (hoeffdingE2 = klDivPmf (tilt) P₂). The existence of a lam ∈ (0,1) solving klDivPmf (tilt) P₁ = alpha is the implicit-function step (monotonicity of λ ↦ klDivPmf T_λ P₁).

What this file publishes #

Closed-form Lagrange minimizer (chernoffMediator alias) #

noncomputable def

InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt

source
{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) (lam : ℝ) :
α → ℝ

Closed-form Lagrange / KKT minimizer of klDivPmf · P₂ on K(α): the exponential tilt Qstar a = P₁ a ^ (1-λ) · P₂ a ^ λ / Z(λ).

This is definitionally Chernoff.chernoffMediator P₁ P₂ lam; we expose it under the Hoeffding name so the interior characterization reads in terms of the tradeoff problem rather than the Chernoff bound.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt_eq_chernoffMediator

      source
      {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (lam : ℝ) :
      hoeffdingTilt P₁ P₂ lam = Chernoff.chernoffMediator P₁ P₂ lam
      Used by
        theorem

        InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt_pos

        source
        {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) (a : α) :
        0 < hoeffdingTilt P₁ P₂ lam a

        The tilt is positive under full support.

        Used by
          theorem

          InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt_sum_eq_one

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

          The tilt sums to 1.

          Used by
            theorem

            InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt_mem_stdSimplex

            source
            {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) :
            hoeffdingTilt P₁ P₂ lam ∈ stdSimplex ℝ α

            The tilt lies in the simplex.

            Used by

              Lagrange gradient identity (constant log-ratio) #

              theorem

              InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt_log_ratio_const

              source
              {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) (a : α) :
              Real.log (hoeffdingTilt P₁ P₂ lam a) - (1 - lam) * Real.log (P₁ a) - lam * Real.log (P₂ a) = -Real.log (Chernoff.chernoffZSum P₁ P₂ lam)

              Lagrange gradient stationarity (constant log-ratio): for the tilt Qstar = hoeffdingTilt P₁ P₂ lam, the log-likelihood combination

              `log (Qstar a) - (1 - lam) · log (P₁ a) - lam · log (P₂ a)`

              is constant in a (it equals -log Z(λ)). This is the Csiszár Lagrange first-order condition ∇[D(·‖P₂) + μ D(·‖P₁)] = const; the explicit constant makes the stationarity dischargeable as pure rpow algebra.

              Used by
                theorem

                InformationTheory.Shannon.HoeffdingTilt.hoeffdingTilt_log_ratio_eq

                source
                {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) (a b : α) :
                Real.log (hoeffdingTilt P₁ P₂ lam a) - (1 - lam) * Real.log (P₁ a) - lam * Real.log (P₂ a) = Real.log (hoeffdingTilt P₁ P₂ lam b) - (1 - lam) * Real.log (P₁ b) - lam * Real.log (P₂ b)

                Pairwise flatness: a corollary stating that the log-ratio combination agrees at any two points a, b. This is the gradient condition in the form "∇ is constant", convenient for the KKT consumer.

                Used by

                  Gradient sub-predicate (IsKLGradientHyp) #

                  structure

                  InformationTheory.Shannon.HoeffdingTilt.IsKLGradientHyp

                  source
                  {α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) (alpha lam : ℝ) (Qstar : α → ℝ) :
                  Prop

                  KL gradient sub-predicate: bundles the constant-log-ratio gradient stationarity at parameter lam together with full support and simplex membership of Qstar.

                  The alpha argument is kept for interface symmetry with the interior predicates (the gradient condition itself does not depend on alpha).

                  • pos(a : α) : 0 < Qstar a

                    Qstar is full support.

                  • sum_one : ∑ a : α, Qstar a = 1

                    Qstar is a pmf.

                  • log_ratio_const(a b : α) : Real.log (Qstar a) - (1 - lam) * Real.log (P₁ a) - lam * Real.log (P₂ a) = Real.log (Qstar b) - (1 - lam) * Real.log (P₁ b) - lam * Real.log (P₂ b)

                    Constant log-ratio gradient stationarity: the log-likelihood combination is flat across the alphabet.

                  Instances For
                    Used by
                      theorem

                      InformationTheory.Shannon.HoeffdingTilt.isKLGradientHyp_tilt

                      source
                      {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (alpha lam : ℝ) :
                      IsKLGradientHyp P₁ P₂ alpha lam (hoeffdingTilt P₁ P₂ lam)

                      Gradient discharge for the tilt family: the closed-form tilt hoeffdingTilt P₁ P₂ lam satisfies IsKLGradientHyp (no hypothesis on alpha).

                      Used by

                        Lagrange constraint-match sub-predicate #

                        structure

                        InformationTheory.Shannon.HoeffdingTilt.IsHoeffdingLagrangeHyp

                        source
                        {α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) (alpha lam : ℝ) :
                        Prop

                        Lagrange constraint-match sub-predicate: at parameter lam, the tilt hoeffdingTilt P₁ P₂ lam lies in the constraint set K(α) and realises the infimum hoeffdingE2 P₁ P₂ alpha.

                        The membership half is the constraint klDivPmf (tilt) P₁ ≤ alpha; the realises half is the infimum-attainment. Existence of a lam ∈ (0,1) with klDivPmf (tilt) P₁ = alpha is the implicit-function / monotonicity step (λ ↦ klDivPmf T_λ P₁ increasing from 0 at λ=0 to klDivPmf P₂ P₁ at λ=1), kept as the single remaining analytic hypothesis.

                        @audit:retract-candidate(load-bearing-predicate) — the hypothesis-form layer has no in-tree consumers. Producer-side constructors (isHoeffdingLagrangeHyp_of_minimal, exists_isHoeffdingLagrangeHyp_of_minimal, isHoeffdingLagrangeHyp_of_constraint_eq, exists_isHoeffdingLagrangeHyp_interior) remain constructive.

                        Instances For
                          Used by

                            Full-support flag via Lagrange tilt #

                            theorem

                            InformationTheory.Shannon.HoeffdingTilt.isHoeffdingMinimizerFullSupport_of_lagrange

                            source
                            {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) :
                            HoeffdingBoundaryMinimizer.IsHoeffdingMinimizerFullSupport (hoeffdingTilt P₁ P₂ lam)

                            Tilt is full support: the closed-form tilt minimizer satisfies the IsHoeffdingMinimizerFullSupport predicate. This is purely constructive — hoeffdingTilt_pos discharges full support directly from hP₁_pos / hP₂_pos, so no Lagrange hypothesis is needed.

                            Used by