This paper develops systematic approaches to obtain -divergence inequalities, dealing with pairs of probability measures defined on arbitrary alphabets. Functional domination is one such approach, where special emphasis is placed on finding the best possible constant upper bounding a ratio of -divergences. Another approach used for the derivation of bounds among -divergences relies on moment inequalities and the logarithmic-convexity property, which results in tight bounds on the relative entropy and Bhattacharyya distance in terms of divergences. A rich variety of bounds are shown to hold under boundedness assumptions on the relative information. Special attention is devoted to the total variation distance and its relation to the relative information and relative entropy, including "reverse Pinsker inequalities," as well as on the divergence, which generalizes the total variation distance. Pinsker's inequality is extended for this type of -divergence, a result which leads to an inequality linking the relative entropy and relative information spectrum. Integral expressions of the Rényi divergence in terms of the relative information spectrum are derived, leading to bounds on the Rényi divergence in terms of either the variational distance or relative entropy.
This mission is the statement-level formalization of -divergence Inequalities (arXiv:1508.00335v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
66 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: Functional domination: Df<=kappa_bar Dg, and if f and g are differentiable at 1 with both derivatives zero, the supremal ratio equals kappa_bar (Theorem 1, PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
noncomputable section
open MeasureTheory Set Filter
open scoped ENNReal NNReal Topology BigOperators ProbabilityTheory
namespace QAlgorithms.Papers.Independent.Intakenext100.P28
universe u
attribute [local instance] Classical.propDecidable
/-- Theorem 1: Functional domination: Df<=kappa_bar Dg, and if f and g are differentiable at 1 with both derivatives zero, the supremal ratio equals kappa_bar. Sason--Verdu, arXiv:1508.00335v7, PDF p.13. -/
theorem functional_domination
(f g : ℝ → ℝ) (hf : Generator f) (hg : PositiveGenerator g)
{A : Type u} [MeasurableSpace A] (P Q : Measure A)
[IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hPQ : P ≪ Q) :
fDiv f P Q ≤ (functionalConstant f g : EReal) * fDiv g P Q ∧
((HasDerivAt f 0 1 ∧ HasDerivAt g 0 1) →
Sharp (nDiv f) (nDiv g) acPairs (functionalConstant f g)) := by sorry
end QAlgorithms.Papers.Independent.Intakenext100.P28
end
Let be convex on , normalized at 1, with for . Put , allowing . For every probability pair ,
If both derivatives at 1 exist and vanish, is the least universal multiplicative coefficient over all measurable alphabets and probability pairs. This best-constant formulation avoids undefined infinite quotients and retains both parts of Theorem 1.
No submissions yet on this mission's goal. Log in and be the first to prove it.