Monotonicity and positive interior derivative of the raw profiles

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.profile_monotonicity

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

prove2quantum

Fix an integer $d\ge2$ . Let $q_d$ be the minimum constrained Schmidt tangle at overlap $F$ , and let $c_d=\sqrt{q_d}$ . Both functions are nondecreasing on $[1/d,1]$ , and $q_d(1/d)=c_d(1/d)=0$ . For every $F\in(1/d,1)$ , with $\gamma_d(F)=\sqrt{F/d}+\sqrt{(d-1)(1-F)/d}$ and $\delta_d(F)=\sqrt{F/d}-\sqrt{(1-F)/(d(d-1))}$ ,

q_d'(F)=4\sqrt{d/F}\,\gamma_d(F)\delta_d(F)\bigl(\gamma_d(F)+\delta_d(F)\bigr)>0.

The derivative assertion is restricted to the interior; it does not apply a total two-sided derivative to a singular endpoint formula.

This monotonicity is the profile property used to simplify the arbitrary-state fidelity bound.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P21

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P21

open scoped Matrix ComplexConjugate

open Filter

open QAlgorithms

open QAlgorithms.Papers.Independent.Information100.P03
  (PureEnsemble convexRoof pureConcurrence concurrence SchmidtData schmidtVector)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF pp.9--10, (3.35): both raw profiles are monotone on the closed domain;
the displayed positive derivative is asserted only in its open interior. -/
theorem profile_monotonicity (d : ℕ) (hd : 2 ≤ d) :
    MonotoneOn (constrainedSchmidtTangle d) (Set.Icc (1 / (d : ℝ)) 1) ∧
    MonotoneOn (rawC d) (Set.Icc (1 / (d : ℝ)) 1) ∧
    constrainedSchmidtTangle d (1 / (d : ℝ)) = 0 ∧ rawC d (1 / (d : ℝ)) = 0 ∧
    ∀ F ∈ Set.Ioo (1 / (d : ℝ)) 1,
      HasDerivAt (constrainedSchmidtTangle d)
        (4 * Real.sqrt ((d : ℝ) / F) * minimizingLargeAmplitude d F * minimizingSmallAmplitude d F *
          (minimizingLargeAmplitude d F + minimizingSmallAmplitude d F)) F ∧
      0 < 4 * Real.sqrt ((d : ℝ) / F) * minimizingLargeAmplitude d F * minimizingSmallAmplitude d F *
        (minimizingLargeAmplitude d F + minimizingSmallAmplitude d F) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 10, §3.3, (3.35): monotonicity of the raw profiles

Read-back

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

For every natural number $d\ge2$ , define $P_d(F)$ as the infimum of $2(1-\sum_{i=0}^{d-1}\mu_i^2)$ over real vectors satisfying $\mu_i\ge0$ , $\sum_i\mu_i=1$ , and $\sum_i\sqrt{\mu_i}=\sqrt{dF}$ , put $r_d(F)=\sqrt{P_d(F)}$ , and define

a_d(F)=\sqrt{\frac Fd}+\sqrt{\frac{(d-1)(1-F)}d}, \qquad b_d(F)=\sqrt{\frac Fd}-\sqrt{\frac{1-F}{d(d-1)}}.

Both $P_d$ and $r_d$ are nondecreasing on the closed interval $[1/d,1]$ : whenever $x,y$ belong to that interval and $x\le y$ , their respective values at $x$ are no larger than at $y$ . They satisfy $P_d(1/d)=r_d(1/d)=0$ . For every $F$ in the open interval $(1/d,1)$ , the function $P_d$ , considered as a function on all real numbers, has derivative

P_d'(F)=4\sqrt{\frac dF}\,a_d(F)b_d(F)\bigl(a_d(F)+b_d(F)\bigr),

and this displayed derivative value is strictly positive. No derivative assertion is made at either endpoint.

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