Definitions for The Uncertainty Relation for Smooth Entropies

Definition

QAlgorithms_Papers_Independent_Intakethird100_P24

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

prove2quantum

The objects the formalized statements of The Uncertainty Relation for Smooth Entropies (arXiv:1009.2015) are stated in. Each was checked against the paper by a blind read-back and a moderator.

squaredOverlap: PDF p.1, equation (2): the SQUARED largest-singular-value overlap of two finite POVMs. Nonempty outcome sets make this a genuine finite maximum.
incompatibilityBits: PDF p.1, equation (2): q = log₂(1/c) = -log₂(c). For POVMs on a nonzero finite space, c is positive, so log at zero is unused.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Papers_Independent_Information100_P67
import Definitions.Def_QAlgorithms_Papers_Independent_Dependency50_P35

/-!
Tomamichel--Renner, arXiv:1009.2015v3, PDF pp.1--4.
The two paper imports are pinned accepted library modules: their actual entropy
and measurement definitions are reused, without assuming their theorems.
All logarithms are in bits. The order form preserves the subnormalized zero
endpoint where the printed additive expression has opposite infinities.
The QKD sketches are inventoried as source ambiguities in HARD.md and GAPS.json.
Compilation is pending the separate mechanical handoff.
-/

noncomputable section

open scoped BigOperators ComplexConjugate Matrix ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P24

open QAlgorithms.Papers.Independent.Information100.P67
  (IsSubnormalized conditionalMinEntropy conditionalMaxEntropy
   smoothConditionalMinEntropy smoothConditionalMaxEntropyExtended)
open QAlgorithms.Papers.Independent.Dependency50.P35 (measured)

/-- PDF p.1, equation (2): the SQUARED largest-singular-value overlap of two
finite POVMs. Nonempty outcome sets make this a genuine finite maximum. -/
def squaredOverlap {A X Z : Type} [Fintype A] [DecidableEq A]
    [Fintype X] [Nonempty X] [Fintype Z] [Nonempty Z]
    (M : X → Matrix A A ℂ) (N : Z → Matrix A A ℂ) : ℝ :=
  Finset.univ.sup' Finset.univ_nonempty
    (fun xz : X × Z => specNorm (cfc Real.sqrt (M xz.1) * cfc Real.sqrt (N xz.2)) ^ 2)

/-- PDF p.1, equation (2): q = log₂(1/c) = -log₂(c).
For POVMs on a nonzero finite space, c is positive, so log at zero is unused. -/
def incompatibilityBits {A X Z : Type} [Fintype A] [DecidableEq A]
    [Fintype X] [Nonempty X] [Fintype Z] [Nonempty Z]
    (M : X → Matrix A A ℂ) (N : Z → Matrix A A ℂ) : ℝ :=
  -Real.logb 2 (squaredOverlap M N)

example {A : Type} [Fintype A] [DecidableEq A] (M N : Matrix A A ℂ) :
    squaredOverlap (fun _ : Unit => M) (fun _ : Unit => N) =
      specNorm (cfc Real.sqrt M * cfc Real.sqrt N) ^ 2 := by
  simp [squaredOverlap]

example {A X Z : Type} [Fintype A] [DecidableEq A]
    [Fintype X] [Nonempty X] [Fintype Z] [Nonempty Z]
    (M : X → Matrix A A ℂ) (N : Z → Matrix A A ℂ)
    (h : squaredOverlap M N = 1) : incompatibilityBits M N = 0 := by
  simp [incompatibilityBits, h]

end QAlgorithms.Papers.Independent.Intakethird100.P24

Source

The Uncertainty Relation for Smooth Entropies, arXiv:1009.2015v3, https://arxiv.org/abs/1009.2015v3

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P24.incompatibilityBits`

For any finite set $A$ with decidable equality, finite nonempty sets $X,Z$ , and arbitrary families $M_x,N_z\in\mathbb C^{A\times A}$ , this defines

-\log_2\!\left( \max_{x\in X,\ z\in Z} \left\|f(M_x)f(N_z)\right\|_{\mathrm{op}}^2 \right), \qquad f(t)=\sqrt t,

using real continuous functional calculus and the Euclidean operator norm. No positivity, Hermitian, or measurement assumptions are required; the functional calculus gives zero on non-Hermitian matrices, and the real square root maps negative eigenvalues to zero on Hermitian matrices. The logarithm is the total real logarithm, so a zero maximum gives the value zero, rather than an infinite value. In particular, $A$ is allowed to be empty, which gives value zero.

`QAlgorithms.Papers.Independent.Intakethird100.P24.squaredOverlap`

For any finite set $A$ with decidable equality, finite nonempty sets $X,Z$ , and arbitrary families of complex matrices $M_x,N_z\in\mathbb C^{A\times A}$ , this defines the real number

c(M,N)=\max_{x\in X,\ z\in Z} \left\|f(M_x)f(N_z)\right\|_{\mathrm{op}}^2, \qquad f(t)=\sqrt t,

where $f(H)$ is the real continuous functional calculus applied to $H$ , and $\|\cdot\|_{\mathrm{op}}$ is the operator norm for Euclidean norms. No positivity, Hermitian, or measurement assumptions are imposed on these matrices: this uses the total functional-calculus operation, which gives zero for a non-Hermitian matrix; on a Hermitian matrix, it applies the real square root to its eigenvalues, with negative eigenvalues mapped to zero. The set $A$ may be empty, in which case the value is zero; the maximum is always over a nonempty set because $X$ and $Z$ are nonempty.

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