Prove2Me

Lemma 24: off-diagonal Renyi quotient estimate

Open
QAlgorithms.Papers.Independent.Intakethird100.P19.renyiQuotient_bound

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For p,q∈(0,1]p,q\in(0,1] with p≠qp\ne q, and α∈(0,1)∪(1,2)\alpha\in(0,1)\cup(1,2),

pq1−αp(1−α)/α−q(1−α)/αp1/α−q1/α≤1.\frac{\sqrt{pq}}{1-\alpha}\frac{p^{(1-\alpha)/\alpha}-q^{(1-\alpha)/\alpha}}{p^{1/\alpha}-q^{1/\alpha}}\le1.

This is the off-diagonal form of the estimate used in Lemma 22.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19
Formal statement
noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- Lemma 24, PDF p.29: the off-diagonal quotient, with alpha=2 excluded. -/
theorem renyiQuotient_bound (alpha p q : ℝ)
    (ha : (0 < alpha ∧ alpha < 1) ∨ (1 < alpha ∧ alpha < 2))
    (hp : 0 < p) (hp1 : p ≤ 1) (hq : 0 < q) (hq1 : q ≤ 1) (hne : p ≠ q) :
    Real.sqrt (p * q) / (1 - alpha) *
      ((Real.rpow p ((1 - alpha) / alpha) - Real.rpow q ((1 - alpha) / alpha)) /
        (Real.rpow p (1 / alpha) - Real.rpow q (1 / alpha))) ≤ 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end
Source
Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 29, Lemma 24
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For real numbers α,p,q\alpha,p,q satisfying either 0<α<10<\alpha<1 or 1<α<21<\alpha<2, with 0<p≤10<p\le1, 0<q≤10<q\le1, and p≠qp\ne q, one has

pq1−αp(1−α)/α−q(1−α)/αp1/α−q1/α≤1.\frac{\sqrt{pq}}{1-\alpha} \frac{p^{(1-\alpha)/\alpha}-q^{(1-\alpha)/\alpha}} {p^{1/\alpha}-q^{1/\alpha}} \le1.

All powers are real powers. The assumptions allow either ordering of p,qp,q, make the displayed denominators nonzero, and exclude α=0,1,2\alpha=0,1,2.

Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph