InformationTheory

InformationTheory.Shannon.Hoeffding.Lagrange

source

Imports 4

Hoeffding tradeoff — Lagrange constraint-match via IVT #

The interior Csiszár characterization IsHoeffdingLagrangeHyp (Hoeffding/Tilt.lean) is a structure with two fields:

  • mem — the tilt at lam lies in the constraint set K(α) (klDivPmf (tilt) P₁ ≤ alpha);
  • realises — the tilt at lam realises the infimum (hoeffdingE2 = klDivPmf (tilt) P₂).

The companion gradient sub-predicate IsKLGradientHyp is discharged in Hoeffding/Tilt.lean (isKLGradientHyp_tilt). This file discharges the mem half — the constraint-match — from the Intermediate Value Theorem, and reduces the remaining realises half to a strictly-more-primitive minimality predicate IsHoeffdingTiltMinimal (the Csiszár I-projection minimality), with the bridge IsHoeffdingTiltMinimal → realises fully discharged.

Approach #

The constraint functional along the tilt family is

  `g(λ) := klDivPmf (hoeffdingTilt P₁ P₂ λ) P₁`.

At the endpoints the tilt collapses to the data distributions (chernoffMediator_lam_zero/one):

  `g(0) = klDivPmf P₁ P₁ = 0`,   `g(1) = klDivPmf P₂ P₁`.

g is continuous on [0,1] (the mediator is a continuous rpow/Z-quotient, klFun is continuous, finite-sum). By intermediate_value_Icc, for every alpha ∈ [0, klDivPmf P₂ P₁] there is a λ ∈ [0,1] with g(λ) = alpha. That λ makes the tilt land exactly on the constraint boundary, discharging the mem field (with equality, hence ≤ alpha). This is the genuine implicit- function / monotonicity content of the interior characterization.

The realises field is the Csiszár-projection infimum-attainment. It is not derivable from IVT; it requires that the tilt minimises klDivPmf · P₂ over K(α). We expose this as the primitive IsHoeffdingTiltMinimal (an IsMinOn flag, real content — not defeq to realises) and discharge the bridge IsHoeffdingTiltMinimal → (hoeffdingE2 = klDivPmf tilt P₂) via the sInf characterisation (le_csInf + csInf_le). Supplying the minimality flag + IVT then assembles a full IsHoeffdingLagrangeHyp.

What this file publishes #

Remaining content #

The standalone discharge of IsHoeffdingTiltMinimal (the I-projection minimality of the explicit tilt, i.e. the first-order/gradient KKT argument) is the analytic content carried as the primitive through isHoeffdingLagrangeHyp_of_minimal. The mem half is fully constructive.

Continuity of the constraint functional g(λ) = klDivPmf T_λ P₁ #

theorem

InformationTheory.Shannon.HoeffdingLagrange.chernoffMediator_continuous_lam

source
{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (a : α) :
Continuous fun (lam : ℝ) => Chernoff.chernoffMediator P₁ P₂ lam a

The Chernoff mediator coordinate λ ↦ T_λ(a) is continuous in λ (a continuous rpow numerator divided by the strictly-positive continuous Z).

Used by
    theorem

    InformationTheory.Shannon.HoeffdingLagrange.hoeffdingTilt_continuous_kl_P₁

    source
    {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) :
    Continuous fun (lam : ℝ) => CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ lam) P₁

    The constraint functional g(λ) := klDivPmf (hoeffdingTilt P₁ P₂ λ) P₁ is continuous in λ on all of ℝ.

    Used by

      Endpoint values of g #

      theorem

      InformationTheory.Shannon.HoeffdingLagrange.hoeffdingTilt_kl_P₁_lam_zero

      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) :
      CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ 0) P₁ = 0

      g(0) = klDivPmf P₁ P₁ = 0.

      Used by
        theorem

        InformationTheory.Shannon.HoeffdingLagrange.hoeffdingTilt_kl_P₁_lam_one

        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) :
        CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ 1) P₁ = CsiszarProjection.klDivPmf P₂ P₁

        g(1) = klDivPmf P₂ P₁.

        Used by

          IVT constraint-match #

          theorem

          InformationTheory.Shannon.HoeffdingLagrange.exists_lam_hoeffdingTilt_kl_eq

          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_le : alpha ≤ CsiszarProjection.klDivPmf P₂ P₁) :
          ∃ lam ∈ Set.Icc 0 1, CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ lam) P₁ = alpha

          IVT constraint-match: for any alpha ∈ [0, klDivPmf P₂ P₁] there is a tilt parameter lam ∈ [0,1] whose tilt hits the Type-I constraint exactly: klDivPmf (hoeffdingTilt P₁ P₂ lam) P₁ = alpha.

          Used by

            mem from a constraint-match #

            theorem

            InformationTheory.Shannon.HoeffdingLagrange.hoeffdingTilt_mem_constraintSet_of_kl_eq

            source
            {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) {alpha lam : ℝ} (h_kl : CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ lam) P₁ = alpha) :
            HoeffdingTilt.hoeffdingTilt P₁ P₂ lam ∈ Chernoff.hoeffdingConstraintSet P₁ alpha

            A tilt parameter hitting the constraint with equality lands in the constraint set K(α) (membership = simplex + KL = alpha ≤ alpha).

            Used by

              Primitive minimality predicate + bridge to realises #

              def

              InformationTheory.Shannon.HoeffdingLagrange.IsHoeffdingTiltMinimal

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

              Primitive tilt-minimality (Csiszár I-projection): the tilt at lam minimises klDivPmf · P₂ over the constraint set K(α). This carries genuine content (an IsMinOn over all of K), distinct from the sInf-form hoeffdingE2 = klDivPmf tilt P₂ of IsHoeffdingLagrangeHyp.realises.

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

                  InformationTheory.Shannon.HoeffdingLagrange.isHoeffdingTiltMinimal_realises

                  source
                  {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₂_pos : ∀ (a : α), 0 < P₂ a) {alpha lam : ℝ} (h_mem : HoeffdingTilt.hoeffdingTilt P₁ P₂ lam ∈ Chernoff.hoeffdingConstraintSet P₁ alpha) (h_min : IsHoeffdingTiltMinimal P₁ P₂ alpha lam) :
                  Chernoff.hoeffdingE2 P₁ P₂ alpha = CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ lam) P₂

                  Bridge (minimal ⇒ realises): when the tilt at lam lies in K(α) and minimises klDivPmf · P₂ on K(α), it realises the infimum hoeffdingE2 P₁ P₂ alpha. Discharged via the sInf characterisation.

                  Used by

                    Assemble IsHoeffdingLagrangeHyp #

                    theorem

                    InformationTheory.Shannon.HoeffdingLagrange.isHoeffdingLagrangeHyp_of_minimal

                    source
                    {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) {alpha lam : ℝ} (h_kl : CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ lam) P₁ = alpha) (h_min : IsHoeffdingTiltMinimal P₁ P₂ alpha lam) :
                    HoeffdingTilt.IsHoeffdingLagrangeHyp P₁ P₂ alpha lam

                    Assemble Lagrange hypothesis: from an IVT constraint-match (mem, klDivPmf tilt P₁ = alpha) and the minimality primitive, build a full IsHoeffdingLagrangeHyp. The mem half is constructive; only minimality is carried.

                    Used by
                      theorem

                      InformationTheory.Shannon.HoeffdingLagrange.exists_isHoeffdingLagrangeHyp_of_minimal

                      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_le : alpha ≤ CsiszarProjection.klDivPmf P₂ P₁) (h_min : ∀ lam ∈ Set.Icc 0 1, CsiszarProjection.klDivPmf (HoeffdingTilt.hoeffdingTilt P₁ P₂ lam) P₁ = alpha → IsHoeffdingTiltMinimal P₁ P₂ alpha lam) :
                      ∃ lam ∈ Set.Icc 0 1, HoeffdingTilt.IsHoeffdingLagrangeHyp P₁ P₂ alpha lam

                      Existence form: IVT supplies a lam ∈ [0,1] matching the constraint; together with the minimality primitive at that lam, a full IsHoeffdingLagrangeHyp exists. The minimality hypothesis is quantified over the (otherwise unknown) IVT witness.

                      Used by