Hoeffding I-projection minimizer attainment — IsHoeffdingTiltMinimal discharge #

Hoeffding/Lagrange.lean discharged the mem half of IsHoeffdingLagrangeHyp from the IVT and reduced the realises half to the strictly-primitive predicate

  `IsHoeffdingTiltMinimal P₁ P₂ α λ`
    := `IsMinOn (klDivPmf · P₂) (hoeffdingConstraintSet P₁ α) (hoeffdingTilt P₁ P₂ λ)`,

the Csiszár I-projection minimality of the exponential tilt. This file discharges that minimality fully, for the interior regime 0 < λ ≤ 1 with the IVT constraint-match klDivPmf (tilt) P₁ = α.

Approach #

The discharge is the exponential-family Pythagorean identity, derived from the log-linearity of the tilt and a per-coordinate algebraic identity that holds even at zero atoms (so the minimality extends to the whole constraint set K, boundary included).

The key per-coordinate fact, valid for R > 0 and all Q ≥ 0 (including Q = 0, where 0 · log 0 = 0):

  `R · klFun (Q / R) = Q · log Q - Q · log R + (R - Q)`.

Summing this against the three references P₂, P₁, T = hoeffdingTilt P₁ P₂ λ with weights λ, 1 - λ, -1 makes the Q log Q terms cancel (coefficients λ + (1-λ) - 1 = 0) and the Q log R terms collapse via the tilt's constant-log-ratio identity log T - (1-λ) log P₁ - λ log P₂ = -log Z (hoeffdingTilt_log_ratio_const) into the flat term Q · (-log Z). Summing over the simplex (∑ Q = 1) gives the master identity

  `λ · D(Q‖P₂) + (1-λ) · D(Q‖P₁) - D(Q‖T) = -log Z`        (∀ Q ∈ stdSimplex).

Specialising to Q = T (D(T‖T)=0) and subtracting yields the Pythagorean difference

  `λ (D(Q‖P₂) - D(T‖P₂)) + (1-λ)(D(Q‖P₁) - D(T‖P₁)) = D(Q‖T) ≥ 0`.

For Q ∈ K the constraint gives D(Q‖P₁) ≤ α = D(T‖P₁), so the (1-λ)·(…) term is ≤ 0 (using 1-λ ≥ 0); hence λ (D(Q‖P₂) - D(T‖P₂)) ≥ 0, and with λ > 0 we get D(T‖P₂) ≤ D(Q‖P₂) — exactly IsMinOn.

What this file publishes #

• klFun_ref_mul — per-coordinate R·klFun(Q/R) = Q logQ - Q logR + (R-Q), valid at Q = 0.
• klDivPmf_eq_entropyCross_sum — D(Q‖R) = ∑ (Q logQ - Q logR + R - Q).
• hoeffdingTilt_kl_master — the master identity (∀ Q ∈ stdSimplex).
• hoeffdingTilt_kl_pythagoras_diff — the Pythagorean difference identity.
• isHoeffdingTiltMinimal_of_constraint_eq — the IsHoeffdingTiltMinimal discharge from 0 < λ, λ ≤ 1, and the constraint-match equality.
• isHoeffdingLagrangeHyp_of_constraint_eq — full IsHoeffdingLagrangeHyp with both halves now constructive (no minimality hypothesis carried).
• exists_isHoeffdingLagrangeHyp_interior — interior existence: IVT supplies the λ ∈ (0,1], minimality is discharged in-file.

Per-coordinate klFun identity (valid at zero atoms) #

klDivPmf cross-entropy sum form (no full support) #

Master exponential-family identity #

Pythagorean difference identity #

IsHoeffdingTiltMinimal discharge #

Constructive IsHoeffdingLagrangeHyp (both halves) #

Interior existence (IVT + discharged minimality) #