Prove2Me

Lemma 23: scalar power quotient estimate

Open
QAlgorithms.Papers.Independent.Intakethird100.P19.powerQuotient_bound

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

prove2quantum

For positive real numbers x≠yx\ne y and r∈(−1,0)∪(0,1)r\in(-1,0)\cup(0,1),

1rxr−yrx−y≤(xy)r−1.\frac1r\frac{x^r-y^r}{x-y}\le(\sqrt{xy})^{r-1}.

This is a bound on a scalar divided difference of a real power.

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 23, PDF p.29: scalar quotient bound; every denominator is guarded. -/
theorem powerQuotient_bound (x y r : ℝ) (hx : 0 < x) (hy : 0 < y) (hne : x ≠ y)
    (hr : (-1 < r ∧ r < 0) ∨ (0 < r ∧ r < 1)) :
    (1 / r) * ((Real.rpow x r - Real.rpow y r) / (x - y)) ≤
      Real.rpow (Real.sqrt (x * y)) (r - 1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

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

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

For positive real numbers x,yx,y with x≠yx\ne y, and a real number rr satisfying either −1<r<0-1<r<0 or 0<r<10<r<1, one has

1r xr−yrx−y≤(xy)r−1,\frac1r\,\frac{x^r-y^r}{x-y} \le \bigl(\sqrt{xy}\bigr)^{r-1},

where all powers are real powers. Either ordering of xx and yy is allowed; the hypotheses exclude zero denominators and exclude r=−1,0,1r=-1,0,1.

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