Discover · Prove2Me

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

On the Douglas–Rachford Algorithm for Solving Possibly Inconsistent Optimization Problems: The Primal Shadows Converge Weakly, and in Value, to a Solution of the Normal ProblemResearch Paper

Motivation

The Douglas–Rachford algorithm is one of the most widely used splitting methods for minimizing a sum $f + g$ of two convex functions, or more generally for finding a zero of a sum $A + B$ of two maximally monotone operators. It touches each summand only through its proximal mapping (resolvent), which is why it underlies ADMM and a large share of first-order solvers in signal processing, statistics and operations research.

Its convergence theory is classical in the consistent case, when $A + B$ has a zero: then the shadow sequence $J_A T^n x$ , the sequence actually used as the approximate solution, converges weakly to a zero of $A + B$ (Lions and Mercier 1979; Svaiter 2011). In practice, however, problems are frequently inconsistent: the constraint sets do not meet, or $\operatorname{dom} f \cap \operatorname{dom} g = \varnothing$ , so that $\min f + g$ has no solution in the usual sense. Then the governing sequence $T^n x$ diverges, and the question is what the shadows do. Infeasibility detection in ADMM-based conic solvers (Banjac, Goulart, Stellato and Boyd 2019; Liu, Ryu and Yin 2019) is one place where this question arises.

Timeline (as recounted in §1.2 of the paper).

2004: Bauschke, Combettes and Luke treat two closed convex sets $U, V$ : the shadows $P_U T^n x$ are bounded and their weak cluster points minimize $\iota_U + \iota_V(\cdot - v)$ .
2014: Bauschke, Hare and Moursi set up a static framework for generalized solutions of inconsistent monotone inclusions, the normal problem.
2016: the same authors relate $\operatorname{ran}(\mathrm{Id} - T)$ to the domains and ranges of $A$ and $B$ .
2016: Bauschke and Moursi prove strong convergence, with linear rates, for two closed affine subspaces; with Dao, one affine subspace and one closed convex set; and, via a new Fejér monotonicity principle, full weak convergence of the shadows for two closed convex sets.
2020: Bauschke and Moursi treat $f = \iota_U$ for a closed linear subspace $U$ and general $g \in \Gamma_0(X)$ , under the assumption $v_R = 0$ .
This paper (arXiv 2021; Mathematics of Operations Research 2024): weak and value convergence of the shadows for two general $f, g \in \Gamma_0(X)$ , and $v_R = 0$ shown to be necessary.

Setting

Let $X$ be a real Hilbert space and $A, B : X \rightrightarrows X$ maximally monotone operators. The resolvent of $A$ is $J_A = (\mathrm{Id} + A)^{-1}$ , a single-valued map on all of $X$ ; $R_A = 2J_A - \mathrm{Id}$ is the reflected resolvent, and $J_{A^{-1}} = \mathrm{Id} - J_A$ . The Douglas–Rachford operator is

T = \mathrm{Id} - J_A + J_B R_A .

The minimal displacement vector of $T$ is $v = P_{\overline{\operatorname{ran}}(\mathrm{Id} - T)}(0)$ , the element of least norm in the closure of $\operatorname{ran}(\mathrm{Id}-T)$ . With $D = \operatorname{dom}A - \operatorname{dom}B$ and $R = \operatorname{ran}A + \operatorname{ran}B$ , put $v_D = P_{\overline D}(0)$ and $v_R = P_{\overline R}(0)$ . The paper works under the standing assumption

\overline{\operatorname{ran}}(\mathrm{Id} - T) = \overline{D \cap R} = \overline{D} \cap \overline{R}, \tag{12}

which holds automatically in finite dimensions for subdifferential operators. The normal problem is to find $x$ with $0 \in -v + Ax + B(x - v)$ ; its solution set is $Z$ .

In the optimization setting, $f, g \in \Gamma_0(X)$ are proper, convex and lower semicontinuous with values in $]-\infty, +\infty]$ , $(A, B) = (\partial f, \partial g)$ , the resolvents become the proximal mappings $P_f, P_g$ , and $T = \mathrm{Id} - P_f + P_g R_f$ . The normal problem becomes $\min_x f(x) + g(x - v)$ , which may have solutions even when $\operatorname{dom} f \cap \operatorname{dom} g = \varnothing$ . The primal shadows are $P_f T^n x$ and $P_g R_f T^n x$ .

Formalization targets

Goal: Theorem 6.9

Let $f, g \in \Gamma_0(X)$ , assume (12), and suppose that $0 \in \operatorname{dom} f^* + \operatorname{dom} g^*$ , that $v \in \operatorname{ran}(\mathrm{Id} - T)$ and that $\operatorname{zer}(\partial f + \partial g(\cdot - v)) \neq \varnothing$ . Let $\mu = \min_x (f(x) + g(x - v))$ and $x \in X$ . Then there is $\bar z$ such that

P_f T^n x \rightharpoonup \bar z,\qquad P_g R_f T^n x \rightharpoonup \bar z - v,

$\bar z$ minimizes $f + g(\cdot - v)$ and $\bar z - v$ minimizes $f(\cdot + v) + g$ , and

f(P_f T^n x) + g(P_g R_f T^n x) \to f(\bar z) + g(\bar z - v) = \mu,

with $f(P_f T^n x) \to f(\bar z)$ and $g(P_g R_f T^n x) \to g(\bar z - v)$ .

Milestones

The milestones follow the paper's chain: the resolvent identities (Lemma 2.2) and Proposition 2.7; the splitting $v = v_D + v_R$ (Proposition 3.3); the static results on $\operatorname{Fix}(v + T)$ and $Z$ (Lemma 4.1, Proposition 4.2, Theorem 4.3); the orbit dynamics (Proposition 5.3, Theorem 5.5, Corollary 5.7); and §6: $v_R = 0$ from the conjugate condition, $Z$ as the minimizers of the normal problem (Proposition 6.2), the prox lemma and value estimate (Lemma 6.3, Proposition 6.4), and convergence in value and weakly (Propositions 6.5, 6.6).

Significance

The result. Theorem 6.9 says that running the Douglas–Rachford algorithm on an inconsistent convex problem is still meaningful: the computed shadows converge to a solution of the normal problem, the closest consistent shift of the original problem, and the objective values converge to its optimal value. Practitioners can thus run the method without first deciding feasibility. The static results of §§3–4 (the location of $v_D$ , $v_R$ , the description of $Z$ when $v_R = 0$ ) are general facts about pairs of maximally monotone operators and are reusable outside the algorithm.

Formalizing it. The theorem is proved on paper; no part of it is machine-checked. A formalization would be the first verified convergence result for a splitting method in the inconsistent case, and it requires a library of Hilbert-space monotone operator theory (resolvents, Minty's theorem, Fejér monotonicity, Opial-type arguments, the Brøndsted–Rockafellar theorem) that Mathlib currently lacks.

Difficulty

When $v \neq 0$ the governing sequence $T^n x$ diverges, roughly like $-nv$ , so the Fejér monotonicity argument of the consistent case, which rests on a fixed point of $T$ , has nothing to anchor to: $T$ has no fixed points. The natural first idea, to apply the consistent theory to the shifted pair $(-v + A, B(\cdot - v))$ , does not by itself say anything about the shadows of the original iteration, and in general the primal shadows need not even be bounded (by Theorem 5.5 of the paper, when $\operatorname{Fix}(v + T) \neq \varnothing$ they are bounded exactly when $v_R = 0$ ). Identifying weak cluster points as minimizers requires an asymptotic value estimate rather than a fixed-point characterization, and the uniqueness of the weak limit needs a Fejér-type property in the product space $X \times X$ . Lower semicontinuity gives only $\liminf$ bounds on $f$ and $g$ separately, so convergence of each value is a separate claim.

Formalization scope

$X$ is a real inner product space with CompleteSpace X. Operators are X → Set X; maximal monotonicity and resolvents come from published definitions. Resolvents and proximal maps are maps J : X → X characterized by $x - Jx \in A(Jx)$ for all $x$ , which is $J = (\mathrm{Id} + A)^{-1}$ ; $J_{A^{-1}}$ and $P_{f^*}$ are written $\mathrm{Id} - J_A$ and $\mathrm{Id} - P_f$ , by the inverse resolvent identity. The projections $v, v_D, v_R$ are least-norm points of the respective closures. Functions are X → EReal in the published class $\Gamma_0$ ; the subdifferential is empty off the domain; every inequality is stated as an EReal sum, without extended-real subtraction. $\mu$ is the EReal infimum of $f + g(\cdot - v)$ . Weak convergence is $\langle u_n, w\rangle \to \langle z, w\rangle$ for all $w$ . Norms on $X \times X$ are written $\|a\|^2 + \|b\|^2$ .

Restored hypotheses and corrections, disclosed on every item: the standing assumption (12) of p. 6 is an explicit hypothesis of every statement from §3 on; the §6 statements carry the section's standing assumptions ( $v_R = 0$ , and $Z \neq \varnothing$ from (74) on). The page prints $\mu := \min_x (f(x + v) - g(x))$ in Theorem 6.9; the statement uses $\min_x(f(x) + g(x - v))$ , as in Proposition 6.5 and §1.1. The goal does not assume $v_R = 0$ , $Z \neq \varnothing$ or boundedness of the shadows: these are consequences, and a version assuming them, or leaving the proximal maps or $v$ unconstrained, would trivialize the statement.

The development needs Minty's theorem, the Brøndsted–Rockafellar density $\overline{\operatorname{dom}} f^* = \overline{\operatorname{ran}} \partial f$ , closedness and convexity of $\overline{\operatorname{ran}}(\mathrm{Id} - T)$ , Opial's lemma, and maximal monotonicity of subdifferentials of $\Gamma_0$ functions. These are reusable throughout convex analysis and are welcome as separate contributions. Corollary 6.10 (dual shadows), Proposition 6.7 and the examples are not part of the mission.

Selected references

H. H. Bauschke and W. M. Moursi, On the Douglas–Rachford algorithm for solving possibly inconsistent optimization problems, Mathematics of Operations Research, 2024; preprint arXiv:2106.11547v1 (2021), the version formalized here. https://arxiv.org/abs/2106.11547
H. H. Bauschke, P. L. Combettes and D. R. Luke, Finding best approximation pairs relative to two closed convex sets in Hilbert spaces, Journal of Approximation Theory 127 (2004), 178–192.
H. H. Bauschke, W. L. Hare and W. M. Moursi, Generalized solutions for the sum of two maximally monotone operators, SIAM Journal on Control and Optimization 52 (2014), 1034–1047.
H. H. Bauschke, W. L. Hare and W. M. Moursi, On the range of the Douglas–Rachford operator, Mathematics of Operations Research 41 (2016), 884–897.
H. H. Bauschke and W. M. Moursi, On the Douglas–Rachford algorithm, Mathematical Programming (Series A) 164 (2017), 263–284.
H. H. Bauschke and W. M. Moursi, On the behaviour of the Douglas–Rachford algorithm for minimizing a convex function subject to a linear constraint, SIAM Journal on Optimization 30 (2020), 2559–2576.
W. M. Moursi, The Douglas–Rachford operator in the possibly inconsistent case: static properties and dynamic behaviour, Ph.D. thesis, University of British Columbia, 2016. https://doi.org/10.14288/1.0340501
P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM Journal on Numerical Analysis 16 (1979), 964–979.
B. F. Svaiter, On weak convergence of the Douglas–Rachford method, SIAM Journal on Control and Optimization 49 (2011), 280–287.
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd edition, Springer, 2017.

21 thms2 active usersReviewed

Quantum Information·Captain: Goku

Remarks on Cyclotomic and Degenerate Cyclotomic BMW AlgebrasResearch Paper

Motivation

We relate the structure of cyclotomic and degenerate cyclotomic BMW algebras, for arbitrary parameter values, to that for admissible parameter values. In particular, we show that these algebras are cellular. We characterize those parameter sets for affine BMW algebras over an algebraically closed field that permit the algebras to have non--trivial cyclotomic quotients.

This mission is the statement-level formalization of Remarks on Cyclotomic and Degenerate Cyclotomic BMW Algebras (arXiv:1011.3284v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Cellularity of all cyclotomic BMW algebras over fields (Corollary 6.5 (abstract main result), PDF p. 17). 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.

Deferred results

15 results of the paper are not stated yet, because the library lacks an interface they need:

Unnumbered universal integral system and base change (3.8)–(3.9): Integral generic scalar extension and H-identification (hard)
Proposition 3.7: Diagram-to-presentation map and the r-regular indexed monomial family (hard)
Corollary 3.10: Specified r-regular monomial basis (hard)
Unnumbered trichotomy after Assumption 5.1: Actual Hecke presentation and canonical contraction quotient (hard)
Lemma 5.4: Canonical root-truncation homomorphism theta (hard)
Lemma 5.9: Homogeneous principal-symbol annihilation, rather than printed p0 (source-ambiguity)
Proposition 5.11: Multiplicative restriction of the particular theta to nonunital ideals (hard)
Theorem 5.12: Canonical consecutive-level homomorphisms for both actual towers (hard)
Lemma 6.3: Ambient-action cellular ideal and descended involution on the actual quotient (hard)
Theorem 6.4: Canonical tower maps under Assumption 5.1 (hard)
Corollary 6.6: Simple representations and factorization through specific Hecke/BMW quotients (hard)
Remark 7.6 (equivalence of (7.2) and (7.3)): Canonical negative compression polynomials and formal product factors (hard)
Lemma 7.7: Canonical negative compression coefficients (hard)
Lemma 7.8: Bilateral rational expansions, inversion, regularity and values at zero/infinity (hard)
Theorem 7.9: Complete four-condition ordinary rationality interface (hard)

Selected references

Remarks on Cyclotomic and Degenerate Cyclotomic BMW Algebras, arXiv:1011.3284v3, https://arxiv.org/abs/1011.3284v3

20 thms2 active usersReviewed

Completed

Functional Analysis Partial Differential Equations Symplectic Geometry·Captain: Mazecto

Lectures on Symplectic Field Theory VI: Elliptic Regularity and Compactness of Pseudoholomorphic MapsTextbook

Motivation

A pseudoholomorphic map from a planar domain $U\subseteq\mathbb{C}$ into an almost complex manifold solves the nonlinear Cauchy–Riemann equation

\bar\partial_Ju=\partial_su+J(u)\,\partial_tu=0,\qquad z=s+it.

These maps are the basic objects of Gromov's theory of holomorphic curves, of Floer homology and of symplectic field theory. Two analytic facts about them are used everywhere: solutions of low regularity are automatically smooth, and families with a uniform bound on the first derivative are precompact in $C^\infty_{\mathrm{loc}}$ . A third fact, unique continuation, says that a solution is determined near a point by its derivatives there.

This mission formalizes these results locally, for maps from discs into a finite-dimensional real vector space with an almost complex structure defined on an open subset, following C. Wendl, Lectures on Symplectic Field Theory, Lecture 2 (§ 2.4–2.5) and Proposition 9.1. Mathlib has no Sobolev spaces of weakly differentiable maps, no almost complex structures and no pseudoholomorphic maps. The definitions build on the $W^{k,p}$ norm of the DbarRegularity mission.

Setting

Target. $E$ is a finite-dimensional real vector space and $O\subseteq E$ is open. A smooth almost complex structure on $O$ is a $C^\infty$ map $J:O\to\operatorname{End}_{\mathbb{R}}(E)$ with $J(x)^2=-\mathrm{Id}$ . Allowing an open subset rather than all of $E$ covers, for example, symplectizations of contact-type hypersurfaces.
Domain. $U\subseteq\mathbb{C}$ is open, usually the open unit disc $D$ ; $\partial_su$ and $\partial_tu$ are the derivatives in the directions $1$ and $i$ .
$J$ -holomorphic maps. $u$ is $J$ -holomorphic on $U$ if it is differentiable there with $\partial_su+J(u)\partial_tu=0$ .
Weak solutions. $u$ is a $W^{1,p}_{\mathrm{loc}}$ solution if it is continuous with values in $O$ , has weak partial derivatives that lie with $u$ in $L^p$ of every compact subset of $U$ , and satisfies the equation almost everywhere.
Convergence. $C^\infty_{\mathrm{loc}}$ convergence on an open set means uniform convergence of all derivatives on every compact subset.

Formalization targets

Goal: compactness of pseudoholomorphic discs

Let $J_\nu\to J$ in $C^\infty_{\mathrm{loc}}$ be smooth almost complex structures on $O$ and let $K_0\subseteq O$ be compact. Every sequence of $J_\nu$ -holomorphic $C^1$ maps $u_\nu:D\to K_0$ with $\sup_\nu\sup_D\|Du_\nu\|<\infty$ has a subsequence converging in $C^\infty_{\mathrm{loc}}$ on $D$ to a smooth $J$ -holomorphic map $D\to K_0$ (Wendl, Proposition 9.1).

Milestones

Regularity of weak solutions. For $p>2$ , a continuous $W^{1,p}_{\mathrm{loc}}$ solution of $\partial_su+J(u)\partial_tu=0$ on an open $U$ is $C^\infty$ on $U$ (Theorem 2.22 (1)).
Uniform interior bounds. For $p>2$ , smooth $J_\nu$ -holomorphic discs with values in $K_0$ and uniformly bounded $W^{1,p}$ norm have derivatives of every order bounded on compact subsets of $D$ , uniformly in $\nu$ (Theorem 2.22 (2a)).
Convergence. For $p>2$ , if such discs converge in $W^{1,p}$ to a smooth map, they converge to it in $C^\infty_{\mathrm{loc}}$ (Theorem 2.22 (2b)).
Weakly holomorphic functions. An $L^1$ function on $D$ with $\partial_su+i\partial_tu=0$ in the sense of distributions agrees almost everywhere with a holomorphic function (Lemma 2.19).
Local solutions with prescribed value. For $2<p<\infty$ and $A\in L^p(D,\operatorname{End}_{\mathbb{R}}(\mathbb{C}^n))$ , the equation $\partial_su+i\partial_tu+Au=0$ has, on every sufficiently small disc, a continuous $W^{1,p}$ solution with any prescribed value at $0$ (Lemma 2.24).
Local holomorphic factorization. A smooth solution of $\partial_sh+\bar J(z)\partial_th+A(z)h=0$ , with $\bar J(z)$ a smooth family of complex structures on $E$ , is locally of the form $h=\Phi f$ , where $\Phi(z):\mathbb{C}^n\to E$ is a continuous family of real-linear bijections with $\Phi(z)\circ i=\bar J(z)\circ\Phi(z)$ and $f$ is holomorphic (Theorem 2.26).
Unique continuation. Two smooth $J$ -holomorphic discs whose derivatives of all orders agree at $0$ coincide near $0$ (Proposition 2.28).

Significance

The results. Regularity and $C^\infty_{\mathrm{loc}}$ compactness are the local half of Gromov compactness: once a moduli space of holomorphic curves has a uniform $C^1$ bound, it is precompact in the smooth topology. Unique continuation is the local input for the structure theory of holomorphic curves, such as the decomposition of a curve into a simple curve and a branched cover.

Formalizing them. The mission introduces almost complex structures, pseudoholomorphic maps, weak derivatives and $W^{1,p}_{\mathrm{loc}}$ solutions of a nonlinear first-order system, in a form that applies to any finite-dimensional target and to structures defined on an open subset. These are foundations for finite-energy holomorphic curves in symplectizations, the next stage of this series. Milestones 4 and 5 are statements about linear first-order elliptic equations in the plane, and milestone 6 is a normal form for real-linear Cauchy–Riemann equations; all three are of independent use in complex analysis.

Difficulty

The equation is nonlinear in $u$ and the structures $J_\nu$ vary with $\nu$ ; the statements about sequences are uniform in $\nu$ , with all constants chosen before the index. The weak formulation involves maps that are not assumed differentiable, and the conclusion of milestone 1 is classical smoothness of the given continuous map, not of a representative. The almost complex structure is only defined on an open subset of the target, so every statement keeps track of where the maps take their values. In milestone 6 the complex structure on the target varies with the point of the domain.

Formalization scope

Namespace JHolomorphic. The definition module JHolomorphic_Setting defines IsAlmostComplexOn, dbarJ, IsJHolomorphicOn, HasWeakPartialsOn, IsWeakJHolomorphicOn and TendstoCInftyLocOn. It imports the DbarRegularity setting for sobolevNorm (the $W^{k,p}(U)$ norm $\sum_{j\le k}\|D^j\varphi\|_{L^p(U)}$ ).
Spaces. $E$ is a real normed space with [FiniteDimensional ℝ E], without an inner product. $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). Almost complex structures have type E → E →L[ℝ] E.
Exponents. $p$ is a real number with $p>2$ , used as ENNReal.ofReal p.
Smoothness. Smoothness is ContDiffOn ℝ ∞ ( $C^\infty$ , not analytic); derivatives of order $m$ are iteratedFDeriv ℝ m.
Generality. Wendl states the nonlinear results for $E=\mathbb{C}^n$ with the normalization $J(0)=i$ , $u(0)=0$ ; the statements here drop the normalization, allow an open domain of definition $O$ for $J$ , and require images in a fixed compact subset of $O$ in the statements about sequences.

Contributions welcome: general lemmas on weak derivatives and on $L^p$ spaces over planar domains.

Selected references

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2 and Lecture 9. https://arxiv.org/abs/1612.01009
D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52 (2012), Chapter 2 and Appendix B.
C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser (2019).

68 thms2 active usersReviewed

Quantum Information·Captain: Goku

Admissibility Conditions for Degenerate Cyclotomic BMW AlgebrasResearch Paper

Motivation

We study admissibility conditions for the parameters of degenerate cyclotomic BMW algebras. We show that the u-admissibility condition of Ariki, Mathas and Rui is equivalent to a simple module theoretic condition.

This mission is the statement-level formalization of Admissibility Conditions for Degenerate Cyclotomic BMW Algebras (arXiv:0905.4253v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The four equivalent admissibility conditions (Theorem 5.2, PDF p. 8). 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.

Selected references

Admissibility Conditions for Degenerate Cyclotomic BMW Algebras, arXiv:0905.4253v2, https://arxiv.org/abs/0905.4253v2

16 thms2 active usersReviewed

Quantum Information·Captain: Goku

Observable actions of algebraic groupsResearch Paper

Motivation

Let G be an affine algebraic group and let X be an affine algebraic variety. An action $G\times X \to X$ is called observable if for any G-invariant, proper, closed subset Y of X there is a nonzero invariant $f\in K[X]^G$ such that f(Y) =0. We characterize this condition geometrically as follows. The action $G\times X \to X$ is observable if and only if (1) there is a nonempty open subset $U\subseteq X$ consisting of closed orbits, and (2) the field $K(X)^G$ of G-invariant rational functions on X is equal to the quotient field of $K[X]^G$ . In case G is reductive, we conclude that there exists a unique, maximal, G-stable, closed subset $X_{\soc}$ of $X$ such that $G\times X_{\soc} \to X_{\soc}$ is observable. Furthermore, the canonical map $X_{\soc}// G \to X//G$ is finite and bijective.

This mission is the statement-level formalization of Observable actions of algebraic groups (arXiv:0902.0137v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Observability, invariant rational functions, and generic closed orbits (Abstract main characterization; Theorem 3.10, PDF p. 1). 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.

Deferred results

12 results of the paper are not stated yet, because the library lacks an interface they need:

§1, unnumbered: left and right translation observability: Closed algebraic subgroup, homogeneous-space geometric quotient, and quasi-affineness (hard)
§1, unnumbered main result: finite purely inseparable socle quotient: Reductive group, computed socle, canonical restriction of invariant algebras, and finite socle quotient morphism (hard)
Proposition 2.7: Characteristic-free algebraic unipotence and universal quantification over affine actions (hard)
Proposition 3.2: A valid reduced/reducible six-way equivalence (source obstruction) (source-ambiguity)
Proposition 3.13: Characteristic-free reductive and unipotent algebraic groups and regular direct product (hard)
Proposition 3.17: Genuine contracted product G*_H X with geometric quotient sheaf and induced G-action (hard)
Theorem 3.18: Full geometric quotient property for the canonical localized affine quotient (hard)
Lemma 4.3: Reductive categorical quotient with canonical map on geometric points (hard)
Lemma 4.5: Reductive categorical quotient and restriction to the nonmaximal locus (hard)
Theorem 4.6: Reduced stable subvariety restriction, reductive categorical quotient, socle and canonical invariant-field map for possibly reducible Z (hard)
Theorem 4.7: Computed socle as a reduced stable subvariety with its induced action, plus reductivity (hard)
Proposition 4.8: Computed socle vanishing ideal and arbitrary-characteristic reductivity (hard)

Selected references

Observable actions of algebraic groups, arXiv:0902.0137v2, https://arxiv.org/abs/0902.0137v2

9 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Implementation of group-covariant POVMs by orthogonal measurementsResearch Paper

Motivation

We consider group-covariant positive operator valued measures (POVMs) on a finite dimensional quantum system. Following Neumark's theorem a POVM can be implemented by an orthogonal measurement on a larger system. Accordingly, our goal is to find an implementation of a given group-covariant POVM by a quantum circuit using its symmetry. Based on representation theory of the symmetry group we develop a general approach for the implementation of group-covariant POVMs which consist of rank-one operators. The construction relies on a method to decompose matrices that intertwine two representations of a finite group. We give several examples for which the resulting quantum circuits are efficient. In particular, we obtain efficient quantum circuits for a class of POVMs generated by Weyl-Heisenberg groups. These circuits allow to implement an approximative simultaneous measurement of the position and crystal momentum of a particle moving on a cyclic chain.

This mission is the statement-level formalization of Implementation of group-covariant POVMs by orthogonal measurements (arXiv:quant-ph/0407054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetry-preserving orthogonal dilation (Paper main result: symmetry-preserving orthogonal dilation, PDF p. 2). 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.

Selected references

Implementation of group-covariant POVMs by orthogonal measurements, arXiv:quant-ph/0407054v1, https://arxiv.org/abs/quant-ph/0407054v1

20 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical SystemsResearch Paper

Motivation

Within the abstract framework of dynamical system theory we describe a general approach to the Transient (or Evans-Searles) and Steady State (or Gallavotti-Cohen) Fluctuation Theorems of non-equilibrium statistical mechanics. Our main objective is to display the minimal, model independent mathematical structure at work behind fluctuation theorems. Besides its conceptual simplicity, another advantage of our approach is its natural extension to quantum statistical mechanics which will be presented in a companion paper. We shall discuss several examples including thermostated systems, open Hamiltonian systems, chaotic homeomorphisms of compact metric spaces and Anosov diffeomorphisms.

This mission is the statement-level formalization of Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical Systems (arXiv:1009.3248v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-time Evans–Searles theorem (Proposition 3.3, PDF p. 10). 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.

Deferred results

79 results of the paper are not stated yet, because the library lacks an interface they need:

Proposition 3.9: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
Proposition 4.2: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
Proposition 4.3: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
Proposition 4.5: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
Proposition 4.6: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
Proposition 5.6: Unpinned/incorrect source hypothesis or conclusion for Proposition 5.6 (source-ambiguity)
Proposition 5.15: Unpinned/incorrect source hypothesis or conclusion for Proposition 5.15 (source-ambiguity)
Proposition 5.16: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
Proposition 5.17: Unpinned/incorrect source hypothesis or conclusion for Proposition 5.17 (source-ambiguity)
Proposition 6.3: Unpinned/incorrect source hypothesis or conclusion for Proposition 6.3 (source-ambiguity)
Proposition 6.4: Unpinned/incorrect source hypothesis or conclusion for Proposition 6.4 (source-ambiguity)
Proposition 6.5: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
Proposition 9.1: Gaussian cylinder probability, trace-class quadratic observable and evolved covariance (hard)
Proposition 9.2: Gaussian cylinder probability, trace-class quadratic observable and evolved covariance (hard)
Proposition 9.3: Unpinned/incorrect source hypothesis or conclusion for Proposition 9.3 (source-ambiguity)
Theorem 9.4: Unpinned/incorrect source hypothesis or conclusion for Theorem 9.4 (source-ambiguity)
Proposition 9.5: Unpinned/incorrect source hypothesis or conclusion for Proposition 9.5 (source-ambiguity)
Corollary 10.4: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Proposition 10.5: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Corollary 10.6: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Proposition 10.7: Unpinned/incorrect source hypothesis or conclusion for Proposition 10.7 (source-ambiguity)
Proposition 10.9: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Proposition 10.11: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Proposition 10.12: Resolution of printed sup versus inf in the concave rate, and the actual source weak-Gibbs/pressure interface (source-ambiguity)
Proposition 10.13: Resolution of printed sup versus inf in the concave rate, and the actual source weak-Gibbs/pressure interface (source-ambiguity)
Proposition 10.14: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Proposition 10.15: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Corollary 10.16: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Proposition 11.2: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
Proposition 11.4: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
Proposition 11.5: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
Theorem 11.6: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
discrete-integrated-entropy: Well-defined separate extended expectations of every transported discrete summand (source-ambiguity)
reference-L2-moment-representation: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
discrete-transfer-representation: Unpinned/incorrect source hypothesis or conclusion for discrete-transfer-representation (source-ambiguity)
differentiable-jacobian-entropy: Euclidean C1 dynamics on a compact invariant set, normalized restricted Lebesgue probability, and its RN/Jacobian and divergence identification (hard)
thermostat-energy-and-entropy: Unpinned/incorrect source hypothesis or conclusion for thermostat-energy-and-entropy (source-ambiguity)
gas-exact-trajectory: Unpinned/incorrect source hypothesis or conclusion for gas-exact-trajectory (source-ambiguity)
gas-finite-pressure: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
canonical-smooth-flux: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
ges-functional-structure: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
finite-response-positivity: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
finite-einstein-relations: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
hamiltonian-flux-and-cocycle: General finite-dimensional coupled Hamiltonian system, normalized Gibbs probability on its convergence domain, and Poisson-bracket reservoir fluxes (hard)
hamiltonian-TRI-criterion: Unpinned/incorrect source hypothesis or conclusion for hamiltonian-TRI-criterion (source-ambiguity)
harmonic-finite-gaussian-formula: Unpinned/incorrect source hypothesis or conclusion for harmonic-finite-gaussian-formula (source-ambiguity)
gas-asymptotic-entropy: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
gas-asymptotic-pressure-and-response: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
finite-harmonic-zero-currents: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
harmonic-thermodynamic-limit: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
harmonic-scattering-pressure: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
harmonic-explicit-pressure-and-current: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
harmonic-explicit-LDP: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
harmonic-analytic-bound-and-FDT: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
harmonic-energy-conservation: Unpinned/incorrect source hypothesis or conclusion for harmonic-energy-conservation (source-ambiguity)
gas-NESS-and-GC-failure: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
harmonic-NESS-and-GGC: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
regular-fluctuation-implications: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
bernoulli-pressure-and-NESS: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
bernoulli-FDT: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
baker-Bernoulli-isomorphism: Unpinned/incorrect source hypothesis or conclusion for baker-Bernoulli-isomorphism (source-ambiguity)
dilation-pressure-and-NESS: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
dilation-linear-response-counterexamples: Unpinned/incorrect source hypothesis or conclusion for dilation-linear-response-counterexamples (source-ambiguity)
gaussian-configuration-and-support: Gaussian cylinder probability, trace-class quadratic observable and evolved covariance (hard)
pressure-time-reversal: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
RN-entropy-homology: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
positive-Markov-fluctuations: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Markov-controlled-FDT: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
Anosov-Jacobian-reversal-homology: Unpinned/incorrect source hypothesis or conclusion for Anosov-Jacobian-reversal-homology (source-ambiguity)
Anosov-finite-time-ES: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
Anosov-unique-NESS-and-LDP: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
Proposition 5.15 part-2: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
Proposition 5.15 parts-3-4: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
Proposition 6.4 part-2: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
NESS-L2-moment-representation: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
regular-pressure-limit-exchange: Unpinned/incorrect source hypothesis or conclusion for regular-pressure-limit-exchange (source-ambiguity)
gaussian-parameter-extension: Unpinned/incorrect source hypothesis or conclusion for gaussian-parameter-extension (source-ambiguity)
Smale-transitivity-specification: Unpinned/incorrect source hypothesis or conclusion for Smale-transitivity-specification (source-ambiguity)
Anosov-flow-extensions: Unpinned/incorrect source hypothesis or conclusion for Anosov-flow-extensions (source-ambiguity)

Selected references

Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical Systems, arXiv:1009.3248v2, https://arxiv.org/abs/1009.3248v2

23 thms2 active usersReviewed

Quantum Information·Captain: Goku

Skew shape representations are irreducibleResearch Paper

Motivation

In this paper all of the classical constructions of A. Young are generalized to affine Hecke algebras of type A. It is proved that the calibrated irreducible representations of the affine Hecke algebra are indexed by placed skew shapes and that these representations can be constructed explicitly with a generalization of Young's seminormal construction of the irreducible representations of the symmetric group. The seminormal construction of an irreducible calibrated module does not produce a basis on which the affine Hecke algebra acts integrally but using it one is able to pick out a different basis, an analogue of Young's natural basis, which does generate an integral lattice in the module. Analogues of the "Garnir relations" play an important role in the proof. The Littlewood-Richardson coefficients arise naturally as the decomposition multiplicities for the restriction of an irreducible representation of the affine Hecke algebra to the Iwahori-Hecke algebra.

This mission is the statement-level formalization of Skew shape representations are irreducible (arXiv:math/0401326v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Local intertwiners on generalized weight spaces (Proposition 3.2, PDF p. 8). 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.

Deferred results

10 results of the paper are not stated yet, because the library lacks an interface they need:

Lemma 2.2: Multiplicative placed-skew geometry and its content-preserving isomorphism quotient (hard)
Intertwiners 3.3 3.5: Rational Bernstein localization, PBW coefficients, and evaluation on generalized weight spaces (hard)
Theorem 4.1 (a)–(c); Introduction main results (1),(4); original title seed: Explicit placed-shape seminormal modules and their isomorphism classes (hard)
Proposition 5.3: The actual column-reading tableau and unnormalized vectors n_L=T_w v_C (hard)
Nonstandard 5.4: An extension of the local tau_w to singular nonstandard fillings (source-ambiguity)
Theorem 5.5: Geometric snakes, actual parabolic shuffles and both Garnir zero relations on the computed natural basis (hard)
Proposition 5.6: Coordinates of the actual natural basis and its evaluated Z[q,q^-1] lattice (hard)
Theorem 6.1: Restriction of the actual q-Hecke module and the actual straight-shape modules in an LR direct sum (hard)
Theorem 6.2: Source-specified compatibility of placed factors under vertical/horizontal gluing (source-ambiguity)
Corollary 6.3: Actual principal-series induction, finite composition-factor classes and normalized connected ribbon modules (hard)

Selected references

Skew shape representations are irreducible, arXiv:math/0401326v2, https://arxiv.org/abs/math/0401326v2

5 thms2 active usersReviewed

Quantum Information·Captain: Goku

Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type RepresentationsResearch Paper

Motivation

A representation of the exceptional Lie algebras is presented. It reflects a simple unifying view and it is realized in terms of Zorn-type matrices. The role of the underlying Jordan pair and Jordan algebra content is crucial in the development of the structure. Each algebra contains three Jordan pairs sharing the same Lie algebra of automorphisms and the same external su(3) symmetry. Applications in physics are outlined.

This mission is the statement-level formalization of Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type Representations (arXiv:1403.5120v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is G2 realized by the closed special Zorn commutator (§4, (4.4)–(4.7): G2 Lie realization, PDF p. 11). 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.

Deferred results

12 results of the paper are not stated yet, because the library lacks an interface they need:

Abstract and §1: unified exceptional Zorn realizations: Joint exceptional/Jordan-pair compatibility; compatible normalized G2 generator and Tits-to-Zorn comparison maps (hard)
§5.1: normalization equivalence with Tits: Two fully specified normalized Tits tensor constructions (hard)
(5.15): F4 branching: The labelled equivariant (3,bar6)+(bar3,6) module interface (hard)
§6 Table 2: root and weight correspondence: A pinned E6 Cartan/root-coordinate dictionary and all nine Table-2 weight vectors (hard)
(6.9): E6 branching: Root-aligned three-factor module restriction with the exact Table-2 dictionary (hard)
(7.2): specified E6 inside E7: The specified quaternion-unit embedding of the E6 coordinate bracket inside E7 (hard)
(7.3)–(7.5): E6 action on the two 27 spaces: The two nilpotent 27 coordinate modules and the four block extraction maps (hard)
(7.6): E7 branching: A standard central sl6 identification and labelled exterior-square/dual module equivalences (hard)
§9: closure of the new operator Zorn bracket: Concrete complex Albert algebra, reduced structure operators, and their intrinsic trace adjoint (hard)
§9: E8 operator-valued realization: The concrete Albert operator Zorn space and its comparison with independent complex E8 (hard)
(9.5): E8 branching: External sl3 plus operator-E6 restriction with the Albert 27 and its true contragredient (hard)
§10: Jacobi for E8 raw operator bracket: The raw nonassociative Albert operator bracket of (9.2)-(9.4) (hard)

Selected references

Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type Representations, arXiv:1403.5120v2, https://arxiv.org/abs/1403.5120v2

10 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

A general proof of Landauer-Büttiker formulaResearch Paper

Motivation

We point out a general argument leading from the formula for currents through an open mesoscopic system given by the theory of non-equilibrium steady states (NESS) to the Landauer-Büttiker formula.

This mission is the statement-level formalization of A general proof of Landauer-Büttiker formula (arXiv:math-ph/0603030v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-channel optical theorem with the Landauer–Büttiker transition normalization (Equations (15)–(17), PDF p. 5). 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.

Deferred results

6 results of the paper are not stated yet, because the library lacks an interface they need:

Equation (19), main result; assumptions pp.2–4 and proof pp.5–6: Precisely specified rigged-Hilbert-space stationary scattering data, admissible resolvent boundary values, and a justified trace-to-transmission integral interface for the actual model. (source-ambiguity)
Remark i, equation (24): The stationary scattering interface of (19), plus an energy-current commutator with its actual operator domain, trace-class extension and energy-weighted integrability. (source-ambiguity)
Remark ii, unequal reservoir spectra: The stationary scattering interface of (19), with measurable channel fibers indexed by the distinct reservoir spectral supports. (source-ambiguity)
Remark iii, equation (25): The stationary scattering interface of (19) for finitely many actual reservoirs, tied to the same incoming occupation and on-shell transition matrix. (source-ambiguity)
Remark iii, charge conservation and normality: An assembled unbounded self-adjoint reservoir/sample model and canonical incoming occupation and finite-rank charge-current trace, together with the same model’s on-shell scattering representation. (hard)
Remark iv, multiple spectral channels: Measurable reservoir channel fields of unrestricted multiplicity, correctly directed transmission blocks and their trace-class products, attached to the actual trace-current model. (source-ambiguity)

Selected references

A general proof of Landauer-Büttiker formula, arXiv:math-ph/0603030v4, https://arxiv.org/abs/math-ph/0603030v4

2 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Cellularity and the Jones basic constructionResearch Paper

Motivation

We establish a framework for cellularity of algebras related to the Jones basic construction. Our framework allows a uniform proof of cellularity of Brauer algebras, ordinary and cyclotomic BMW algebras, walled Brauer algebras, partition algebras, and others. Our cellular bases are labeled by paths on certain branching diagrams rather than by tangles. Moreover, for the class of algebras that we study, we show that the cellular structures are compatible with restriction and induction of modules. Applied to cyclotomic BMW algebras, our method allows a new a shorter proof of the finite spanning result and isomorphism with cyclotomic Kauffman tangle algebras.

This mission is the statement-level formalization of Cellularity and the Jones basic construction (arXiv:0906.1496v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Free modules embed into their fraction-field scalar extension (Lemma 2.20, PDF p. 15). 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.

Deferred results

70 results of the paper are not stated yet, because the library lacks an interface they need:

Lemma 2.1: Tagged involution twist of both bimodules and their balanced tensor; descended C-B actions; canonical twist-reversing tensor map (hard)
Lemma 2.9: Invariant two-sided ideals, split-ideal predicate with actual left ideal, and M tensor_R i(M) with both A actions and swap involution (hard)
Lemma 2.10: Finite proper cell chains with split successive quotient ideals, actual quotient involutions, and relaxed cellular data (hard)
Proposition 2.13: Lambda-cell net on upward-closed label sets, quotient bimodule actions and fixed-label cell data (hard)
Lemma 2.19: Scalar-extended noncommutative algebra/module actions and canonical balanced-tensor base-change map, including optional left and right B^F actions (hard)
Lemma 2.22: Constructed cell modules and coherent towers; all finite induction/restriction cell filtrations; actual generic inclusion multiplicities (hard)
Lemma 2.23: Actual generic multiplicity-free branching paths and reindexed cellular data on the original label posets (hard)
Theorem 3.2: All eight framework axioms on actual towers; constructed coherent cell-data family; reflected label order and branching multiplicities; same-level ideal-action scalar extension (hard)
Lemma 4.1: Iterated noncommutative balanced tensor with canonical fraction-field base change and both optional B^F actions (hard)
Lemma 4.2: Semisimple noncommutative algebra, two-sided ideal as a bimodule, and the induced contraction map on iterated balanced tensors (hard)
Proposition 4.3: Full finite-tower induction setup; actual J(Gamma), Jhat(Gamma), tensor domain with A_(n+1) actions, unscaled Phi and inclusion beta (hard)
Lemma 4.4: Canonical Phi and beta for nested cellular order-ideal spans within the finite-tower induction setup (hard)
Lemma 4.5: Canonical Phi from the actual free tensor domain to Jhat(Gamma), with ambient bimodule actions (hard)
Corollary 4.6: Canonical unscaled map xe_n tensor e_ny to xe_ny between actual A_(n+1) bimodules (hard)
Proposition 4.7: Actual Jhat cell net; ambient cellular ideal; lifted ordinal-sum cellular datum and its tensor cell modules (hard)
Corollary 4.8: Constructed next-level cellular datum and reflected disjoint-union label poset with both order cases (hard)
Corollary 4.9: Same constructed next-level cell modules and basic-construction ideal-action submodule, extended to F only in the lower-label case (hard)
Proposition 4.10: Restriction of every actual newly constructed cell module and genuine finite A_n-submodule filtrations (hard)
Lemma 4.11: Scalar-extended noncommutative semisimple algebra and the canonical map id_P tensor inclusion on balanced tensors (hard)
Lemma 4.12: Given actual finite cell filtration; canonical tensor embeddings, quotient maps, transported labels and next-level module action (hard)
Lemma 4.13: Actual restriction functor and the two balanced tensor modules with A_(n+1)-linear equivalences (hard)
Proposition 4.14: Ideal-tensor module, actual induction module, canonical embedding and quotient, and both Q_(n+1) and A_(n+1) cell filtrations (hard)
Corollary 4.15: Simultaneously constructed cellular data and induction/restriction cell filtrations through level n+1 (hard)
Corollary 4.16: Actual generic simple modules and inclusion matrices through n+1, and reflection preserving edge multiplicities (hard)
Lemma 5.2: Brauer loop-count diagram algebra, inclusions and contraction e_n; actual corner and right-product submodules (hard)
Lemma 5.3: Canonical Brauer strand inclusion, e_n, right-ideal images and multiplication-by-e_n map (hard)
Proposition 5.4: Concrete generic Brauer and symmetric-group towers, involutions and all-eight-axiom framework predicate (hard)
Corollary 5.5: Actual specialized Brauer cellular tower, parity Young labels, up-down paths, and whole compatible datum family (hard)
Proposition 5.6: Temperley-Lieb presented algebra and structure maps over Z[delta]; constant quotient tower; all framework axioms (hard)
Corollary 5.7: Specialized Temperley-Lieb cellular tower with actual at-most-two-row Young labels and standard-tableau bases (hard)
Lemma 5.9: Ordinary BMW presentation with all seven relation groups, canonical strand maps, and corner/right-product submodules (hard)
Lemma 5.10: Ordinary BMW algebra and generator-preserving homomorphism between levels, right-ideal images, and multiplication map (hard)
Proposition 5.11: Generic BMW coefficient quotient ring, ordinary BMW/Hecke towers with matching quadratic convention, all framework axioms (hard)
Corollary 5.12: Full BMW coefficient systems and actual specialized coherent cell data with parity Young labels and up-down bases (hard)
Lemma 5.20: Geometric cyclotomic KT_0 with all local affine-loop/skein relations, canonical empty diagram, and actual W_0 (hard)
Lemma 5.21: Actual admissible cyclotomic BMW/KT algebras and canonical phi and strand homomorphisms (hard)
Lemma 5.23: Full generic admissible coefficient system and presented cyclotomic W_n; actual cardinal module rank and pairing count (hard)
Lemma 5.24: Actual generic cyclotomic W_n and geometric KT_n, canonical phi and finite spanning-set cardinality (hard)
Lemma 5.25: Actual W_0,W_1,W_2,KT_1 and cyclotomic H_1; canonical maps and finite free rank (hard)
Lemma 5.26: Canonical cyclotomic phi maps at all levels through n, geometric KT and BMW strand maps, and corner/right-ideal images (hard)
Theorem 5.27: Concrete generic cyclotomic BMW/Hecke framework pair, geometric KT with canonical phi, inclusions and constructed coherent cell data (hard)
Corollary 5.28: Admissible specialized cyclotomic BMW/KT towers, canonical phi, multipartition cellular modules and up-down bases (hard)
Lemma 5.31: Actual walled Brauer diagram subalgebras, long-range e_(a,b), both strand inclusions and both closure maps (hard)
Lemma 5.32: Walled Brauer two-sided contraction ideal and actual involutive quotient to the product symmetric-group algebra (hard)
Lemma 5.33: Walled Brauer left/right strand inclusions and contraction right-ideal images in two different ambient algebras (hard)
Lemma 5.34: Actual Brauer and walled diagram multiplication and normalized full-closure traces over Q(delta) (hard)
Lemma 5.35: Walled Brauer algebra over Q(delta) and finite product-of-full-matrix-algebras meaning of split semisimplicity (hard)
Proposition 5.36: Alternating walled algebra and quotient towers, generators f_n, and generalized framework with replacement axiom (3 prime) (hard)
Corollary 5.38: Walled cellular data for all pairs, both restriction/induction filtrations, integer size-difference labels and augmented branching paths (hard)
Lemma 5.39: Actual even/odd partition diagram algebras and propagating ideals, quotient involutions and symmetric-group algebras (hard)
Lemma 5.40: Partition diagram products, embeddings, propagating ideal J_k and image of A_(k-1)p_(k-1)A_(k-1) (hard)
Lemma 5.41: Partition generators p_k, canonical level inclusions, and corner/right-product submodules with alternating parity (hard)
Lemma 5.42: Partition tower canonical inclusions and actual map x to x p_(k-1), correcting the printed e notation (hard)
Lemma 5.43: Actual partition diagram algebra and its alternating normalized closure trace over Q(delta) (hard)
Proposition 5.45: Concrete generic partition and repeated symmetric-group quotient towers, p generators, and all framework axioms (hard)
Corollary 5.46: Actual specialized partition cellular tower, corrected half-level Young labels and Lemma 5.44 branching-path bases (hard)
Lemma 5.47: Oriented A-labelled planar algebra, western-depth subalgebra and every label generator a^(k) (hard)
Lemma 5.48: Actual depth-restricted labelled planar algebra, strand inclusions and e generators with corner/right-product submodules (hard)
Lemma 5.49: Contour strand homomorphisms, right-ideal images and actual multiplication-by-e_(n-1) map (hard)
Lemma 5.50: Generic labelled contour algebra and normalized closure trace extended from the specified cellular label algebra (hard)
Lemma 5.51: Actual generic contour algebra and finite-dimensional split matrix-block decomposition predicate (hard)
Proposition 5.52: Concrete contour and tensor-power quotient towers over R_0[delta], with orientation-sensitive embeddings and all framework axioms (hard)
§2.2: cell modules and canonical layer tensor isomorphism: Cell representation constructed from triangular coefficients; column and layer quotient actions; invariant cell ideals; canonical bimodule tensor-layer equivalence (hard)
Remark 2.6: extensions of cellular algebras: Ambient cellular-ideal data, actual quotient involution and basis, ordinal-sum order and every choice of quotient-basis lifts (hard)
Remark 2.11: strict cell chains: Finite proper cell chains with involution-invariant R-module complements at every successive pair (hard)
Remark 2.14: strict cell nets: Fixed-Lambda cell nets, all nested-ideal and principal-layer invariant complements, and strict cellular data (hard)
Remark 2.24: inductively lifted path bases: Actual restriction filtrations and quotient isomorphisms, recursive arbitrary R-linear lifts, and actual branching paths (hard)
Remark 3.3: path-indexed cell bases: Constructed basic-construction cell data on reflected label posets and multiplicity-free generic branching paths (hard)
Remark 5.29: strictly cellular cyclotomic Murphy-type bases: Full generic cyclotomic BMW presentation and coefficient system, strict cellular data and multipartition up-down path bases (hard)
Remark 5.37: quotient walled branching diagram: Product symmetric-group quotient tower, its actual generic simple modules and inclusion multiplicities, and bipartition Young labels (hard)

Selected references

Cellularity and the Jones basic construction, arXiv:0906.1496v2, https://arxiv.org/abs/0906.1496v2

5 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

A Cocycle Model for Topological and Lie Group CohomologyResearch Paper

Motivation

We propose a unified framework in which the different constructions of cohomology groups for topological and Lie groups can all be treated on equal footings. In particular, we show that the cohomology of "locally continuous" cochains (respectively "locally smooth" in the case of Lie groups) fits into this framework, which provides an easily accessible cocycle model for topological and Lie group cohomology. We illustrate the use of this unified framework and the relation between the different models in various applications. This includes the construction of cohomology classes characterizing the string group and a direct connection to Lie algebra cohomology.

This mission is the statement-level formalization of A Cocycle Model for Topological and Lie Group Cohomology (arXiv:1110.3304v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem VI.2: delta-functor comparison principle (Theorem VI.2: delta-functor comparison principle, PDF p. 25). 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.

Deferred results

63 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem IV.5 (Comparison Theorem); introductory theorem p. 2: Segal-Mitchison and global continuous cohomology as concrete delta-functors on locally contractible k-G-modules (hard)
Remark I.2: local coefficient long exact sequences: Unnormalized continuous/smooth local cohomology and lift-defined connecting homomorphisms (hard)
Remark I.3: degrees zero, one, two: Low-degree regular cohomology and the Baer group of locally trivial abelian extensions (hard)
Remark I.4: comparison in low degrees and global coefficient sequence: Actual global-to-local cohomology maps, globally split coefficient sequences and connected-G extension comparison (hard)
Proposition I.5: loop-contractible comparison (cited): Loop-contractible comparison for unnormalized regular cochain complexes (hard)
Lemma I.6: discrete smooth-continuous comparison: Inclusion-induced map on the unnormalized discrete-coefficient local smooth and local continuous cohomologies (hard)
Proposition I.7: finite-dimensional comparison: Regular cohomology inclusion for quasi-complete locally convex discrete-submodule quotients (hard)
Remark I.8: ordinary-product variant: Ordinary-product local/global cohomology and locally split connecting sequences (hard)
Remark II.2: simplicial sheaves form an abelian category with injectives: Category of compatible abelian sheaves on a simplicial space, with componentwise operations (hard)
Lemma II.4: left exact section functor: The actual simplicial section functor ker(D0-D1) (hard)
Proposition II.6: simplicial sheaf spectral sequence: Derived simplicial section cohomology, first-quadrant spectral sequence and convergence filtration (hard)
Corollary II.8: acyclic component calculation: Cosimplicial section Moore complex and its comparison with derived simplicial sections (hard)
Lemma II.11: simplicial coefficient sequences: Continuous and smooth simplicial coefficient functors with natural connecting maps (hard)
Proposition II.12: contractible simplicial coefficients: Contractible-coefficient simplicial-to-global comparison (hard)
Proposition II.15: local sheaves are soft: Local-regularity abelian sheaf, softness and positive-degree sheaf cohomology (hard)
Corollary II.16: local sheaf model: Derived sections of local-regularity simplicial sheaves and local cohomology (hard)
Remark II.17: sheaf-to-local comparison morphisms: Sheaf-inclusion-induced natural morphisms from simplicial to local cohomology (hard)
Remark III.2: construction of semi-simplicial good covers: Coherent semi-simplicial open covers and good refinements (hard)
Proposition III.4: Cech sequences and spectral sequence: Leray comparison for arbitrary sheaves on a fixed good cover (source-ambiguity)
Remark III.5: explicit degree-two comparison: Consistent explicit right-fiber-coordinate Cech comparison (source-ambiguity)
Lemma IV.3: sections of the soft embedding (cited): Thin Segal realization E_G(A), quotient B_G(A), local/global sections (hard)
Proposition IV.4: soft module acyclicity: Globally continuous cohomology of the actual coinduced k-function module (hard)
Remark IV.6: weaker loop-contractible comparison axiom: Loop contraction of actual Segal realization/coinduction and comparison on contractible coefficients (hard)
Corollary IV.7: Natural Segal-Mitchison/simplicial cohomology comparison (hard)
Corollary IV.8: Canonical local/Segal comparison and simplicial-to-local inclusion map (hard)
Corollary IV.9: All three canonical arrows between smooth and continuous simplicial/local cohomology (hard)
Corollary IV.10: Segal cohomology and fixed-good-cover Cech total cohomology (hard)
Remark IV.11: explicit Cech-to-local map: Staircase Cech-to-local comparison as a delta-functor morphism (hard)
Remark IV.12: Flach comparison: Precise Flach external cohomology functor and coefficient category (hard)
Remark IV.12: smooth infinity-groupoid comparison: The cited big smooth topos cohomology and exact Schreiber comparison (hard)
Remark IV.13: Moore and locally continuous measurable comparisons: Polish coefficient category, Borel/local-measurable cochain quotients and delta-functor comparisons (hard)
Remark IV.14: bounded comparison for compact groups: Bounded and unbounded continuous Banach-coefficient cohomology with inclusion-induced map (hard)
Remark IV.16(1): Twisted classifying-space cohomology with pi0 action and Hurewicz comparison (hard)
Remark IV.16(2): Contractible-G global/local/Segal comparison maps (hard)
Remark IV.16(3): Discrete-submodule quotient coefficients, twisted BG cohomology and degree-shift comparison (hard)
Example V.1(1): spherical string four-cocycle: Actual smooth simplex fillings and their homology-valued four-cocycle (hard)
Example V.1(2): integral string cocycle and connecting identity: Cartan-form singular integral, real lift, string cocycle and actual coefficient connecting map (hard)
Example V.1(3) and continuation: external string models: External strict and stacky string models and characteristic classes (hard)
Example V.2: characteristic spherical cocycles: Based simplex-valued filling choices, singular homology cocycle and choice independence (hard)
Example V.2: realization gives a connected cover: Correctly indexed path-loop extension and connected-cover realization (source-ambiguity)
Theorem V.4: crossed-module classification: Topologically split crossed modules, zigzag equivalence and characteristic 3-class (hard)
Remark V.5: metrizable crossed-module realization: The constructed metrizable crossed module and string-generator specialization (hard)
Remark V.6: topology on local cohomology: Shrinking-neighborhood colimit topology on local cochains and quotient cohomology (hard)
Remark V.7: cup products and compatibility: Actual kTop tensor cup product, induced cohomology product and differentiation compatibility (hard)
Equation (13): degree-two topological characteristic sequence: Bundle-characteristic map on actual ordinary-product H^2 and its compatible-extension image (hard)
Proposition V.8: explicit Cech characteristic map: Explicit translated-cover Cech cocycle and induced natural characteristic homomorphism (hard)
Proposition V.9: edge map is the explicit characteristic map: Filtered simplicial spectral-sequence edge and its actual characteristic-map square (hard)
Remark V.10: degree-one edge with trivial action: Degree-one trivial-action edge and characteristic map (hard)
Remark V.11: other edge is inclusion of global cochains: Other filtered edge, E2^(n,0) identification and inclusion-induced global-to-local map (hard)
Corollary V.12: injectivity of the characteristic map: Actual tau_(n+1) on discrete-coefficient local cohomology and full Cech cohomology (hard)
Remark V.13: primitive image: Cech pullbacks along multiplication/projections and the range of actual tau (hard)
Remark V.13: string classes are generators: Integral string classes, characteristic isomorphisms and generator property (hard)
Remark V.14: kernel of differentiation: Differentiation of actual local smooth quotient cohomology (hard)
Remark V.14: discrete-coefficient exact sequence: Continuity of the same coefficient action after discretizing A (source-ambiguity)
Remark V.14: van Est comparison (cited): Actual differentiation map, van Est comparison and split de Rham extension (hard)
Remark V.14: period criterion and explicit integration: Consistent equivariant simplex integral and spherical period map for nontrivial coefficients (source-ambiguity)
Example VI.5: effacement for sheaf cohomology: Positive-degree Cech/sheaf cohomology of actual E_G(A) (hard)
Remark VI.6: counterexample to weaker comparison hypotheses: Concrete geometric counterexamples to weakened effacement hypotheses (hard)
Section VII observation 1: invariants of a coinduced module: Coinduced k-function module and invariants on admissible extensions (hard)
Section VII observation 2: soft resolutions compute SM: Arbitrary soft resolution, constituent local sections and its invariant cohomology complex (hard)
Section VII observation 3: contractible coinduced quotients: Contractible coinduced quotient and its canonical coinduction isomorphism (hard)
Section VII conclusion: SM soft acyclicity: Exact invariant augmented soft resolution and positive-degree Segal cohomology (hard)
Section VII conclusion: SM equals global cohomology on contractible coefficients: Homogeneous coinduced resolution, natural invariant cohomology and global comparison (hard)

Selected references

A Cocycle Model for Topological and Lie Group Cohomology, arXiv:1110.3304v3, https://arxiv.org/abs/1110.3304v3

3 thms2 active usersReviewed

Quantum Information·Captain: Goku

Covariant quantum measurements which maximize the likelihoodResearch Paper

Motivation

We derive the class of covariant measurements which are optimal according to the maximum likelihood criterion. The optimization problem is fully resolved in the case of pure input states, under the physically meaningful hypotheses of unimodularity of the covariance group and measurability of the stability subgroup. The general result is applied to the case of covariant state estimation for finite dimension, and to the Weyl-Heisenberg displacement estimation in infinite dimension. We also consider estimation with multiple copies, and compare collective measurements on identical copies with the scheme of independent measurements on each copy. A "continuous-variables" analogue of the measurement of direction of the angular momentum with two anti-parallel spins by Gisin and Popescu is given.

This mission is the statement-level formalization of Covariant quantum measurements which maximize the likelihood (arXiv:quant-ph/0403083v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §III, Eq.(12): finite-component weak twirling formula (§III, Eq.(12): finite-component weak twirling formula, PDF p. 3). 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.

Deferred results

6 results of the paper are not stated yet, because the library lacks an interface they need:

Abstract / §§IV,VII: unrestricted pure-state canonical maximum-likelihood measurement: Source-selected domain and pointwise density convention for unrestricted generalized pure-state canonical seeds, including infinite attained likelihood (source-ambiguity)
§III, Eqs.(3),(12): unrestricted operator class and infinite sums: Unrestricted operator/form class, well-defined component traces, and convergence topology for the weak Haar twirl and infinite double sum (source-ambiguity)
§V, Eq.(19): asserted independent-average likelihood bound: Outcome coordinate space, real scaling dimension, reference measure, and valid dimension-dependent arithmetic-mean bound (source-ambiguity)
§V.A.2: asserted universal breach for N>2: Correct admissible dimension/copy range for the printed universal strict inequality dim(Sym^N C^d)>Nd (source-ambiguity)
§V.B.3: continuous Wedderburn identity: Domain and diagonal pairing with generalized continuous-spectral projectors, and weak/direct-integral convergence (source-ambiguity)
§V.B.3: canonical optimum for arbitrary two-mode input: Invariant generalized-seed domain and selected pointwise likelihood for arbitrary L2 spectral inputs, including divergent likelihood (source-ambiguity)

Selected references

Covariant quantum measurements which maximize the likelihood, arXiv:quant-ph/0403083v1, https://arxiv.org/abs/quant-ph/0403083v1

29 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite FieldsResearch Paper

Motivation

We present an axiomatic approach to finite- and infinite-dimensional differential calculus over arbitrary infinite fields (and, more generally, suitable rings). The corresponding basic theory of manifolds and Lie groups is developed. Special attention is paid to the case of mappings between topological vector spaces over non-discrete topological fields, in particular ultrametric fields or the fields of real and complex numbers. In the latter case, a theory of differentiable mappings between general, not necessarily locally convex spaces is obtained, which in the locally convex case is equivalent to Keller's C^k_c-theory.

This mission is the statement-level formalization of Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite Fields (arXiv:math/0303300v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularity of a co-restriction to a subspace (Lemma 10.1, PDF p. 48). 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.

Deferred results

65 results of the paper are not stated yet, because the library lacks an interface they need:

Remark 1.2: C0Concept, ConceptLinearMaps (hard)
Remark 1.4: C0Concept, ConceptDense (hard)
Proposition 2.2: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ConceptLinearMaps (hard)
Example 2.3: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Lemma 2.6: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Proposition 3.1 (Chain Rule): C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TangentMapOnDomain, ExtendedTangentMap (hard)
3.2 Linearity: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
3.3 Product rule: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ConceptBilinearMap (hard)
3.4 Polynomial maps: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ModulePolynomialMap (hard)
3.5 Quotient rule: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ConceptInverseAlgebra (hard)
3.6 Rational maps: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ModulePolynomialMap, RationalMap (hard)
3.7 Direct Products: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
3.8 Rule on partial derivatives: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, PartialDifferenceQuotient (hard)
Lemma 3.9: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, PartialDifferenceQuotient (hard)
Remark 4.2: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Example 4.3: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Lemma 4.4: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Proposition 4.5: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Lemma 4.6 (Schwarz): C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, HigherDifferential (hard)
Lemma 4.8: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, HigherDifferential (hard)
Lemma 4.9: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Theorem 5.1: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, TaylorRemainder (hard)
Lemma 5.2: C0Concept, FiniteExpansion (hard)
Proposition 5.3: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, HigherDifferential (hard)
Theorem 5.4: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, TaylorRemainder, HigherDifferential (hard)
Unnumbered second-quotient identity after Theorem 5.4: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, HigherDifferential, TaylorCoefficient (hard)
Lemma 5.5: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Theorem 5.6: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, TaylorRemainder, ModulePolynomialMap (hard)
Lemma 6.1: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, CurveDividedDifference (hard)
Proposition 6.2: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, CurveDividedDifference, HigherDifferential, TaylorCoefficient, TaylorRemainder (hard)
Remark 6.4: C0Concept, ConceptDense (hard)
Lemma 6.6: C0Concept standing environment, plus symmetric raw-quotient splicing identity (hard)
Lemma 6.7: SchikhofCk, CurveDividedDifference (hard)
Lemma 6.8: SchikhofCk, CurveDividedDifference, C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Proposition 6.9: SchikhofCk, CurveDividedDifference, C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
Lemma 7.1: The Section 7 continuous C^0-concept construction over a Hausdorff commutative topological ring: the class of all Hausdorff topological K-modules, product topologies, and C^0(U,F) equal to continuous maps. Package axioms I.1–I.5 and II.1–II.5 and prove III: for every open U ⊆ K and Hausdorff topological K-module F, continuous f,g : U → F agreeing on U ∩ {a : K | IsUnit a} agree everywhere, assuming the units are dense. Include the nondiscrete topological-field specialization; open units and continuous inversion are the source’s standing topological-ring requirements. (hard)
Proposition 7.4: MichalBastianiCk, ExtendedDifferenceQuotient, Differential (hard)
Lemma 7.5: MichalBastianiCk, RepresentedWeakIntegral, FirstVariableDifferential (hard)
Lemma 7.6: MichalBastianiCk, RepresentedWeakIntegral, FirstVariableDifferential (hard)
Proposition 7.7: MichalBastianiCk, LocallyConvexComplexAnalytic, ContinuousDiagonalPolynomial, MackeyComplete, ExtendedDifferenceQuotient, Differential (hard)
Proposition 7.11: PolynormedSpace, StrictDifferentiable, StrictCk, ExtendedDifferenceQuotient, Differential (hard)
Proposition 7.20: UltrametricLocallyConvexSpace, ContinuousDiagonalPolynomial, PolynomialSeminorm, StrictConvergenceIndicatrix, UltrametricAnalytic, ExtendedDifferenceQuotient, Differential (hard)
§7.3 Rational calculus: C0Concept, RationalMap, ZariskiVectorTopology, ConceptCk (hard)
Remark 7.21: AlgebraicKGroup, RationalLieGroup (source-ambiguity)
§7.4 Convenient calculus: C0Concept, CInfinityRefinement, MackeyComplete, ConvenientSmoothMap, ConceptCk (hard)
§8.1 Category and products: ConceptManifold, ManifoldCkMap, ConceptProductManifold, SmoothScalarFunctions (hard)
§8.2 Tangent functor: ConceptManifold, ManifoldCkMap, TangentVector, ConceptTangentBundle, ManifoldTangentMap (hard)
§8.3 Bundle gluing: ConceptManifold, ManifoldCkMap, SmoothBundleCocycle, ConceptFiberBundle, ConceptVectorBundle (hard)
§8.4 Sections and derivations: ConceptVectorBundle, SmoothSection, VectorField, SmoothScalarFunctions, VectorFieldDerivation, ManifoldTangentMap (hard)
Example 8.2: VectorField, SmoothScalarFunctions, VectorFieldDerivation, QuasiBanachLp, ConceptManifold (hard)
Example 8.3: VectorField, VectorFieldDerivation, SmoothScalarFunctions, HigherDifferential, CompactSymmetricBilinearForms, ConceptManifold (hard)
Theorem 8.4: VectorField, VectorFieldBracket, ConceptManifold, ManifoldTangentMap (hard)
Lemma 8.5: VectorField, VectorFieldBracket, RelatedVectorFields, ManifoldTangentMap, ConceptDiffeomorphism (hard)
Unnumbered Lie homomorphism after Lemma 8.5: VectorField, VectorFieldBracket, VectorFieldDerivation, SmoothScalarFunctions (hard)
§9.1 Tangent multiplication: ManifoldWithMultiplication, ConceptTangentBundle, ManifoldTangentMap (hard)
§9.2 Tangent Lie group: ConceptLieGroup, ConceptTangentBundle, ManifoldTangentMap, LieGroupMorphism (hard)
§9.3 Left invariant fields: ConceptLieGroup, LeftInvariantVectorField, VectorFieldBracket, TangentLieAlgebra, ManifoldTangentMap (hard)
Theorem 9.1 (paper seed: Lie functor): ConceptLieGroup, LieGroupMorphism, TangentLieAlgebra, VectorFieldBracket, ManifoldTangentMap (hard)
12.2 Highest raw quotient criterion: RawIteratedDifferenceQuotient, ExtendedDifferenceQuotient, ConceptCk (hard)
Lemma 12.3: RawIteratedDifferenceQuotient, ExtendedDifferenceQuotient, ConceptCk (hard)
§13.1 Continuous inverse algebra examples: ContinuousInverseAlgebra, ConceptLieGroup, ContinuousFunctionAlgebra (hard)
Proposition 13.1: SupportedContinuousMapGroup, UniformMapTopology, ConceptLieGroup, LieStructureOnGroup (hard)
Proposition 13.2: SupportedCrMapGroup, CompactOpenCrTopology, TestFunctionGroup, LocallyConvexDirectLimit, ConceptLieGroup (hard)
§13.3 Diffeomorphism groups: ConceptDiffeomorphism, CompactOpenCrTopology, CompactSupportVectorFields, DiffeomorphismGroupStructure (hard)
§13.4 Direct limit groups: ConceptLieGroup, LieGroupMorphism, ClosedSubmanifold, LocallyConvexDirectLimit, DirectLimitGroup (hard)

Selected references

Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite Fields, arXiv:math/0303300v1, https://arxiv.org/abs/math/0303300v1

18 thms2 active usersReviewed

Quantum Information·Captain: Goku

Tight continuity bounds for the quantum conditional mutual information, for the Holevo quantity and for capacities of quantum channelsResearch Paper

Motivation

We start with Fannes' type and Winter's type tight continuity bounds for the quantum conditional mutual information and their specifications for states of special types. Then we analyse continuity of the Holevo quantity with respect to nonequivalent metrics on the set of discrete ensembles of quantum states. We show that the Holevo quantity is continuous on the set of all ensembles of m states with respect to all the metrics if either m or the dimension of underlying Hilbert space is finite and obtain Fannes' type tight continuity bounds for the Holevo quantity in this case. In general case conditions for local continuity of the Holevo quantity for discrete and continuous ensembles are found. Winter's type tight continuity bound for the Holevo quantity under constraint on the average energy of ensembles is obtained and applied to the system of quantum oscillators. The above results are used to obtain tight and close-to-tight continuity bounds for basic capacities of finite-dimensional channels (refining the Leung-Smith continuity bounds).

This mission is the statement-level formalization of Tight continuity bounds for the quantum conditional mutual information, for the Holevo quantity and for capacities of quantum channels (arXiv:1512.09047v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

28 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2, (35): optimized energy-constrained QCMI continuity; original seed (Proposition 2, (35): optimized energy-constrained QCMI continuity; original seed, PDF p. 14). 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.

Deferred results

11 results of the paper are not stated yet, because the library lacks an interface they need:

Proposition 1, (20)–(21): Jordan-part QCMI comparison: Normalized Jordan parts on arbitrary nuclear coefficient operators, plus their actual finite-dimensional marginal support predicates. (hard)
Corollary 1, (25): finite-minimum-dimension QCMI bound and tightness: Compatibility of the accepted exact isotropicDensity witness with normalized nuclear states and the extended QMI model, including the large-d tightness comparison. (hard)
Corollary 2, (28): qqc continuity and Shannon refinement: Complete countable qqc continuity theorem: computed gamma laws, dimension/Shannon alternatives, finite-difference domains, and both equal-marginal refinements. (hard)
Remark 3: claimed attainment of optimal t: Attained minimum for all admissible entropy majorants (source-ambiguity)
Corollary 3, (44): tight oscillator QCMI bound: Actual oscillator Gibbs purification/mixed-product witness and its energy/information evaluations. (hard)
Proposition 3, (45)–(47): n-copy output QCMI continuity: Local-marginal stabilized channel divergence for arbitrary entangled blocks, plus actual finite and oscillator sharpness witnesses. (hard)
Remark 6, second clause: claimed standard linear programming: Standard linear-program encoding of general noncommuting EHS distance (source-ambiguity)
Proposition 5, (60)–(61): tight global Holevo bounds: All four global Holevo tightness witnesses and normalized gamma-law Shannon refinement in the same ensemble model. (hard)
Proposition 7, (68)–(70): tight energy-bounded discrete Holevo continuity: Actual Gibbs pure-state ensemble sharpness construction (70) and its coefficient-state entropy/energy bridge. (hard)
Proposition 10, (80)–(81): tight Holevo/assisted capacity bounds: CPTP adapters and actual depolarizing channel capacity evaluations in nats, with the unstabilized induced trace norm on all operators. (hard)
Proposition 11, (86)–(87): classical/quantum capacity bounds: Signed extended coherent information, operational/regularized capacity identification and actual erasure/depolarizing sharpness. (hard)

Selected references

Tight continuity bounds for the quantum conditional mutual information, for the Holevo quantity and for capacities of quantum channels, arXiv:1512.09047v7, https://arxiv.org/abs/1512.09047v7

34 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Lie groups over non-discrete topological fieldsResearch Paper

Motivation

We generalize the classical construction principles of infinite-dimensional real (and complex) Lie groups to the case of Lie groups over non-discrete topological fields. In particular, we discuss linear Lie groups, mapping groups, test function groups, diffeomorphism groups, and weak direct products of Lie groups. The specific tools of differential calculus required for the Lie group constructions are developed. Notably, we establish differentiability properties of composition and evaluation, as well as exponential laws for function spaces. We also present techniques to deal with the subtle differentiability and continuity properties of non-linear mappings between spaces of test functions. Most of the results are independent of any specific properties of the topological vector spaces involved; in particular, we can deal with real and complex Lie groups modeled on non-locally convex spaces.

This mission is the statement-level formalization of Lie groups over non-discrete topological fields (arXiv:math/0408008v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The ordinary difference quotient and its continuous extension (Numbered assertion 1.8, PDF p. 14). 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.

Deferred results

111 results of the paper are not stated yet, because the library lacks an interface they need:

Numbered assertion 1.7: Canonical iterated extended-quotient domains and values (hard)
Proposition 1.18: ExtendedDifferenceDomain, BGNLieGroup, BGNManifoldCrMap, BGNManifold (hard)
Proposition 2.2: The actual BGN Lie structure on the open unit submanifold (hard)
Numbered assertion 3.2: Uniform-convergence topology on supported continuous maps and ultrametric local convexity (hard)
Proposition 3.3: SupportedContinuousMaps, ParameterizedPushforward, ExtendedDifferenceDomain (hard)
Corollary 3.4: SupportedContinuousMaps, ParameterizedPushforward, ExtendedDifferenceDomain (hard)
Corollary 3.5: SupportedContinuousMaps, ParameterizedPushforward, ExtendedDifferenceDomain (hard)
Remark 4.2: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.3: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.4: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.5: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.6: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.9: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Remark 4.10: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.11: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.12: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.13: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.14: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 4.15: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Proposition 4.16: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, ParameterizedPushforward (hard)
Proposition 4.19: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, MackeyComplete, MackeyCauchySequence, UltrametricLocalConvexity, IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, SupportedCrMaps (hard)
Proposition 4.20: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, SupportedCrMaps, ParameterizedPushforward (hard)
Corollary 4.21: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, SupportedCrMaps, ParameterizedPushforward (hard)
Lemma 4.22: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
Proposition 4.23: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint, ParameterizedPushforward (hard)
Lemma 4.24: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, SupportedCrMaps (hard)
Paper seed, pinned to Proposition 5.1: supported mapping groups and tangent bracket: SupportedMappingGroup, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BGNLieGroup, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential (hard)
Proposition 5.7: SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Numbered assertion 6.3: BoxDirectSumTopology (hard)
Numbered assertion 6.4: BoxDirectSumTopology, UltrametricLocalConvexity (hard)
Numbered assertion 6.5: BoxDirectSumTopology, OpenDirectSumBox (hard)
Remark 6.6: BoxDirectSumTopology, UltrametricLocalConvexity (hard)
Remark 6.7: BoxDirectSumTopology, UltrametricLocalConvexity (hard)
Lemma 6.8: BoxDirectSumTopology, ReorderedDifferenceQuotient, ExtendedDifferenceQuotient, ExtendedDifferenceDomain (hard)
Proposition 6.9: BoxDirectSumTopology, ReorderedDifferenceQuotient, ExtendedDifferenceQuotient, ExtendedDifferenceDomain, OpenDirectSumBox (hard)
Proposition 6.10: BoxDirectSumTopology, OpenDirectSumBox, ExtendedDifferenceDomain (hard)
Remark 6.11: BoxDirectSumTopology, AffineAtInfinityGroup, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace (hard)
Proposition 7.1: WeakDirectProductLieChart, BGNLieGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology (hard)
Lemma 7.2: WeakDirectProductLieChart, BGNLieGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology (hard)
Lemma 8.3: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, LocalFieldManifoldBall (hard)
Lemma 8.1: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain (hard)
Lemma 8.5: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain (hard)
Lemma 8.7: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ClopenPartitionOfUnity (hard)
Lemma 8.8: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ClopenPartitionOfUnity (hard)
Lemma 8.10: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology (hard)
Proposition 8.13: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, TestFunctionTVSDirectLimitTopology, TestFunctionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
Remark 8.15: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, TestFunctionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
Remark 8.17: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, BGNVectorBundle, BGNTangentBundle, DirectionalDifferential, CompactSupportVectorFields, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection (hard)
Example 8.19: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, PatchedVectorSpace (hard)
Proposition 8.21: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, PatchedMap, PatchedVectorSpace (hard)
Proposition 8.22: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, ParameterizedPushforward, CompactImageConstraint (hard)
Corollary 8.23: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, ParameterizedPushforward (hard)
Proposition 9.1: TestFunctionGroup, BGNLieGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, BoxDirectSumTopology (hard)
Theorem 10.4: LocallyAlmostLocalMap, AlmostLocalMap, TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology (hard)
Proposition 11.1: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
Proposition 11.2: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint, DirectionalDifferential, SupportedCrMaps (hard)
Proposition 11.3: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint, DirectionalDifferential (hard)
Lemma 11.4: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
Lemma 12.1: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Proposition 12.2: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 12.5: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, ConvenientKSmooth, ConvenientOpenTopology (hard)
Proposition 12.6: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, ConvenientKSmooth, ConvenientOpenTopology (hard)
Proposition 13.2: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Lemma 13.7: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace, BoxDirectSumTopology (hard)
Lemma 13.8: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall (hard)
Lemma 13.9: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Lemma 13.10: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, WeakDirectProductLieChart, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology, LocalFieldManifoldBall (hard)
Lemma 13.11: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, WeakDirectProductLieChart, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology, LocalFieldManifoldBall (hard)
Theorem 13.12: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, WeakDirectProductLieChart, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology, LocalFieldManifoldBall, CompactSupportVectorFields, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace (hard)
Remark 13.14: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, CompactSupportDiffeomorphisms, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, FunctionSpaceEvaluationAndComposition, CompactImageConstraint (hard)
Numbered assertion 14.2: CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Numbered assertion 14.3: CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology (hard)
Numbered assertion 14.5: ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace, BoxDirectSumTopology, TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps (hard)
Proposition 14.6: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
Lemma 14.17: CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
Lemma 14.18: CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle (hard)
Proposition 14.19: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
Proposition 14.21: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
Remark 14.22: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
Lemma A.1: IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, CompactOpenCr, CrMappingSpace (hard)
Lemma A.2: IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, CompactOpenCr, CrMappingSpace (hard)
Lemma A.3: IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, CompactOpenCr, CrMappingSpace (hard)
Lemma A.4: Represented weak interval integrals in complete arbitrary locally convex spaces (hard)
Lemma A.5: Weak-integral domain with all partial directional derivative integrals and induced derivative topology (hard)
Lemma C.1: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
Theorem D.1: Mackey completeness and ultrametric local convexity in the source topology (hard)
Lemma E.1: The six concrete Boman target classes including Mackey completeness and ultrametric local convexity (hard)
Theorem E.2: Mackey-complete ultrametric locally convex targets and the universal scalar Boman premise (hard)
Remark F.2: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Lemma F.6: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Remark F.8: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, UltrametricLocalConvexity (hard)
Lemma F.9: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Theorem F.11: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, FibrePreservingBundleMap, ParameterizedPushforward (hard)
Numbered assertion F.12: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, WhitneySumBundle (hard)
Corollary F.13: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Lemma F.15: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SupportedCrSections (hard)
Lemma F.16: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
Lemma F.18: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
Proposition F.19: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, SectionTVSDirectLimitTopology, SectionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
Remark F.20: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, SectionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
Remark F.21: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, PatchedVectorSpace (hard)
Lemma F.22: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
Theorem F.23: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, FibrePreservingBundleMap, ParameterizedPushforward (hard)
Corollary F.24: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, FibrePreservingBundleMap (hard)
Remark F.25: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, FibrePreservingBundleMap (hard)
Numbered assertion F.26: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, WhitneySumBundle (hard)
Corollary F.27: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
Remark F.28: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, BundleOfTopologicalModules, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
Theorem F.30: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, AlmostLocalSectionMap, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
10.3: local maps are almost local (explicit assertion): Germ and patch predicates on the actual box-topologized compact-support mapping spaces (hard)
F.29: local maps are almost local (explicit assertion): Germ and patch predicates on actual compact-support section spaces (hard)

Selected references

Lie groups over non-discrete topological fields, arXiv:math/0408008v1, https://arxiv.org/abs/math/0408008v1

14 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Multipartite Classical and Quantum Secrecy MonotonesResearch Paper

Motivation

In order to study multipartite quantum cryptography, we introduce quantities which vanish on product probability distributions, and which can only decrease if the parties carry out local operations or carry out public classical communication. These ``secrecy monotones'' therefore measure how much secret correlations are shared by the parties. In the bipartite case we show that the mutual information is a secrecy monotone. In the multipartite case we describe two different generalisations of the mutual information, both of which are secrecy monotones. The existence of two distinct secrecy monotones allows us to show that in multipartite quantum cryptography the parties must make irreversible choices about which multipartite correlations they want to obtain. Secrecy monotones can be extended to the quantum domain and are then defined on density matrices. We illustrate this generalisation by considering tri-partite quantum cryptography based on the Greenberger-Horne-Zeilinger (GHZ) state. We show that before carrying out measurements on the state, the parties must make an irreversible decision about what probability distribution they want to obtain.

This mission is the statement-level formalization of Multipartite Classical and Quantum Secrecy Monotones (arXiv:quant-ph/0202103v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The two classical multipartite secrecy monotones (Abstract; §III, (12)–(17),(24),(28),(30),(35), PDF p. 1). 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.

Deferred results

5 results of the paper are not stated yet, because the library lacks an interface they need:

§II.B.1, exact case of (8)–(11): A general exact finite-block LOPC conversion relation retaining arbitrary initial Eve side information, full public-copy transitions, and independent Eve output registers. (hard)
§II.B.1, (8)–(11): An approximation metric, growth-controlled continuity modulus, and operational asymptotic rate for general M. (source-ambiguity)
§III.B: The admissible classical local erasure operations, environment initialization/return constraints, entropy cost, and exact/asymptotic precision convention. (source-ambiguity)
§V.B: The admissible quantum local erasure operations, environment initialization/return constraints, entropy cost, and exact/asymptotic precision convention. (source-ambiguity)
§V.E, after (70): A correct equality characterization or a source-specified nondegenerate measurement class. (source-ambiguity)

Selected references

Multipartite Classical and Quantum Secrecy Monotones, arXiv:quant-ph/0202103v1, https://arxiv.org/abs/quant-ph/0202103v1

33 thms2 active usersReviewed

Quantum Information·Captain: Goku

On Quantum Communication Channels with Constrained InputsResearch Paper

Motivation

The purpose of this work is to extend the result of previous papers quant-ph/9611023, quant-ph/9703013 to quantum channels with additive constraints onto the input signal, by showing that the capacity of such channel is equal to the supremum of the entropy bound with respect to all apriori distributions satisfying the constraint. We also make an extension to channels with continuous alphabet. As an application we prove the formula for the capacity of the quantum Gaussian channel with constrained energy of the signal, establishing the asymptotic equivalence of this channel to the semiclassical photon channel. We also study the lower bounds for the reliability function of the pure-state Gaussian channel.

This mission is the statement-level formalization of On Quantum Communication Channels with Constrained Inputs (arXiv:quant-ph/9705054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2: constrained discrete classical–quantum capacity, (10) (Proposition 2: constrained discrete classical–quantum capacity, (10), PDF p. 3). 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.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

Section IV, sentence after (34): A valid shell-probability asymptotic on the source domain of all admissible priors. (source-ambiguity)
Section IV, (40)-(41) and reliability lower bound: A finite valid optimized reliability lower bound over all pi in P1 and all p>=0 after removal of the shell factor. (source-ambiguity)

Selected references

On Quantum Communication Channels with Constrained Inputs, arXiv:quant-ph/9705054v1, https://arxiv.org/abs/quant-ph/9705054v1

20 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Operator Isomorphisms on Hilbert Space Tensor ProductsResearch Paper

Motivation

This article presents an isomorphism between two operator algebras $L_1$ and $L_2$ where $L_1$ is the set of operators on a space of Hilbert-Schmidt operators and $L_2$ is the set of operators on a tensor product space. We next compare our isomorphism to a well-known result called Choi's isomorphism theorem. The advantage of Choi's isomorphism is that it takes completely positive maps to positive operators. One advantage of our isomorphism is that it applies to infinite dimensional Hilbert spaces, while Choi's isomorphism only holds for finite dimensions. Also, our isomorphism preserves operator products while Choi's does not. We close with a brief discussion on some uses of our isomorphism.

This mission is the statement-level formalization of Operator Isomorphisms on Hilbert Space Tensor Products (arXiv:2010.15901v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1.3: formula for a basis conjugation (Lemma 1.3, PDF p. 3). 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.

Deferred results

19 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 1.7: the operator C*-algebra isomorphisms R and S: The complete realized rectangular HS Hilbert space and the prescribed bounded maps J_A, J_A*, R, S (hard)
Theorem 1.1 (background attributed to [3]): matrix-unit basis and three equivalent conditions: Theorem 1.1 (background attributed to [3]): matrix-unit basis and three equivalent conditions (source-ambiguity)
Theorem 1.2: basis vectorization is unitary, with explicit adjoint: Complete realized HS(H1,H2), its matrix-unit basis, and the bounded series-defined J_A (hard)
Lemma 1.5: rank-one operators and simple tensors, with conjugation: Rank-one elements of realized HS(H1,H2), J_A and its Hilbert adjoint (hard)
Corollary 1.6: change of orthonormal bases: Two independently constructed HS vectorizations for the reference and new bases (hard)
Lemma 1.8: finite-family positivity inequality for R: The prescribed R between endomorphism algebras of the realized HS and completed tensor spaces (hard)
Theorem 1.9: R preserves the HS class and HS inner product: Nested realized HS Hilbert spaces and the restriction of source R (hard)
Lemma 2.1: the one-basis vectorization equals J_A: HS-domain one-basis vectorization T_B and independently defined two-basis J_A (hard)
Lemma 2.3: slice expansion of T_B adjoint: The bounded HS-domain T_B and HS-valued rank-one slice series (hard)
Unnumbered claim: the spectrum characterization of conjugation: Unnumbered claim: the spectrum characterization of conjugation (source-ambiguity)
Unnumbered consequence: positivity and complete positivity of R and S: Prescribed R and S on the full bounded endomorphism algebras of the HS Hilbert space and completed tensor space (hard)
Unnumbered analogue of Theorem 1.9 for S: Nested realized HS Hilbert spaces and source S restricted to the HS class (hard)
Unnumbered comparison: Choi fails product preservation and differs from R: Compatible finite HS Hilbert realization, prescribed R, and unnormalized input-first Choi map (hard)
Discussion: concatenation of the displayed Kraus maps: Bounded HS endomorphisms and actual HS-norm-convergent Kraus sandwich series (hard)
Equations (3.1)–(3.2): R of a represented Kraus map: HS-valued Kraus representation, constructed M_alpha and source R (hard)
Discussion: adapted product vectors and their rank-one projections under S: Adapted complete bases, source J_A*, and S acting on rank-one projections (hard)
Discussion: Schmidt coefficients detect entanglement and give the J_A* image: Finite realized HS Hilbert space and J_A* for the supplied Schmidt bases (hard)
Discussion: the printed general product-operator action under S: Discussion: the printed general product-operator action under S (source-ambiguity)
Discussion: the final printed HS expansion: Discussion: the final printed HS expansion (source-ambiguity)

Selected references

Operator Isomorphisms on Hilbert Space Tensor Products, arXiv:2010.15901v1, https://arxiv.org/abs/2010.15901v1

7 thms2 active usersReviewed

Quantum Information·Captain: Goku

Optimal Cloning of Pure States, Judging Single ClonesResearch Paper

Motivation

We consider quantum devices for turning a finite number N of d-level quantum systems in the same unknown pure state \sigma into M>N systems of the same kind, in an approximation of the M-fold tensor product of the state \sigma. In a previous paper it was shown that this problem has a unique optimal solution, when the quality of the output is judged by arbitrary measurements, involving also the correlations between the clones. We show in this paper, that if the quality judgement is based solely on measurements of single output clones, there is again a unique optimal cloning device, which coincides with the one found previously.

This mission is the statement-level formalization of Optimal Cloning of Pure States, Judging Single Clones (arXiv:quant-ph/9807010v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Sharp single-clone error bound and explicit attainment (Theorem 1, inequality and Eq.(3), PDF p. 3). 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.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 1, unrestricted equality iff: Validity of the printed equality-if-and-only-if characterization over every CP unital cloning map. (source-ambiguity)
Proposition 7: Validity of the printed assertion that the normalized U(d) Haar-average fiber of the canonical cloner is a singleton. (source-ambiguity)

Selected references

Optimal Cloning of Pure States, Judging Single Clones, arXiv:quant-ph/9807010v1, https://arxiv.org/abs/quant-ph/9807010v1

18 thms2 active usersReviewed

Quantum Information·Captain: Goku

Coding Theorems for Quantum ChannelsResearch Paper

Motivation

The more than thirty years old issue of the (classical) information capacity of quantum communication channels was dramatically clarified during the last years, when a number of direct quantum coding theorems was discovered. The present paper gives a self contained treatment of the subject, following as much in parallel as possible with classical information theory and, on the other side, stressing profound differences of the quantum case. An emphasis is made on recent results, such as general quantum coding theorems including cases of infinite (possibly continuous) alphabets and constrained inputs, reliability function for pure state channels and quantum Gaussian channel. Several still unsolved problems are briefly outlined.

This mission is the statement-level formalization of Coding Theorems for Quantum Channels (arXiv:quant-ph/9809023v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: general quantum-channel coding theorem (seed) (Theorem 1: general quantum-channel coding theorem (seed), PDF p. 8). 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.

Deferred results

3 results of the paper are not stated yet, because the library lacks an interface they need:

§IV.3, (80)–(81): claimed general constrained reliability exponents: A corrected admissible-prior class and proved subexponential positive shell probabilities, with finite tilted moments, or a different construction proving the unrestricted exponents in (80)-(81). (source-ambiguity)
§V.2, (100) and piecewise Gaussian reliability comparison: A theorem optimizing both exponent functionals over all admissible priors, or a source-pinned reformulation explicitly limited to the fixed Gaussian prior, with the stationary-s direction corrected. (source-ambiguity)
§V.4, (148)–(150): formal continuum-noise commutator and covariance: A test-function space, a growth condition on N, a specified finite-part kernel and a smeared CCR/quasifree-state construction on which (149)-(150) are well-defined identities. (source-ambiguity)

Selected references

Coding Theorems for Quantum Channels, arXiv:quant-ph/9809023v1, https://arxiv.org/abs/quant-ph/9809023v1

31 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Optimal Teleportation Based on Bell MeasurementResearch Paper

Motivation

We study optimal teleportation based on the Bell measurements. An explicit expression for the quantum channel associated with the optimal teleportation with an arbitrary mixed state resource is presented. The optimal transmission fidelity of the corresponding quantum channel is calculated and shown to be related to the fully entangled fraction of the quantum resource, rather than the singlet fraction as in the standard teleportation protocol.

This mission is the statement-level formalization of Optimal Teleportation Based on Bell Measurement (arXiv:quant-ph/0208015v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal Bell-measurement teleportation channel and attained mean fidelity (Theorem 3, Eqs.(14)-(15): optimal Bell-measurement channel and maximal mean fidelity (abstract seed), PDF p. 6). 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.

Selected references

Optimal Teleportation Based on Bell Measurement, arXiv:quant-ph/0208015v2, https://arxiv.org/abs/quant-ph/0208015v2

5 thms2 active usersReviewed

Quantum Information·Captain: Goku

On the impossibility of distilling Gaussian states with Gaussian operationsResearch Paper

Motivation

We show that no distillation protocol for Gaussian quantum states exists that relies on (i) arbitrary local unitary operations that preserve the Gaussian character of the state and (ii) homodyne detection together with classical communication and postprocessing by means of local Gaussian unitary operations on two symmetric identically prepared copies. This is in contrast to the finite-dimensional case, where entanglement can be distilled in an iterative protocol using two copies at a time. The ramifications for the distribution of Gaussian states over large distances will be outlined. We also comment on the generality of the approach and sketch the most general form of a Gaussian local operation with classical communication in a bipartite setting.

This mission is the statement-level formalization of On the impossibility of distilling Gaussian states with Gaussian operations (arXiv:quant-ph/0204052v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-copy Gaussian no-distillation under the restricted Fig.1 protocol (Theorem (p.2); restricted two-copy Gaussian no-distillation result announced p.1, PDF p. 2). 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.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

Unnumbered closing sketch: general Gaussian LOCC decomposition: An exact operational Gaussian-LOCC class, including adaptive composition, ideal-limit closure and selective failure branches, and an equivalence theorem for the five-step sketch. (source-ambiguity)

Selected references

On the impossibility of distilling Gaussian states with Gaussian operations, arXiv:quant-ph/0204052v4, https://arxiv.org/abs/quant-ph/0204052v4

13 thms2 active usersReviewed

Quantum Information·Captain: Goku

A family of quantum protocolsResearch Paper

Motivation

We introduce two dual, purely quantum protocols: for entanglement distillation assisted by quantum communication (mother'' protocol) and for entanglement assisted quantum communication (father'' protocol). We show how a large class of children'' protocols (including many previously known ones) can be derived from the two by direct application of teleportation or super-dense coding. Furthermore, the parent may be recovered from most of the children protocols by making them coherent''. We also summarize the various resource trade-offs these protocols give rise to.

This mission is the statement-level formalization of A family of quantum protocols (arXiv:quant-ph/0308044v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Mother: qubit-assisted entanglement distillation (Mother resource inequality (♀); seed pinned to the first new parent result, PDF p. 1). 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.

Deferred results

8 results of the paper are not stated yet, because the library lacks an interface they need:

(7): asymptotic coherent-bit equivalence: Sequential resource protocols with resource-generated startup entanglement and vanishing-rate catalytic recycling (hard)
Rule I: coherify input classical communication: Retained-environment measured protocol family and constructive input-message coherification (hard)
Rule O: coherify output classical communication: Retained-environment unitary protocol family and constructive output-message coherification (hard)
Unnumbered proposed relaxation of Rule I uniformity: Quantified real log-probability equiprobability condition and its entanglement yield (source-ambiguity)
Constructive hashing-to-mother Rule I adapter: Actual admissible hashing implementation and resource-counted Rule I witness (hard)
Constructive noisy-super-dense-coding-to-mother Rule O adapter: Specified noisy-super-dense family with full residual decoupling and Rule O transformation (hard)
Constructive entanglement-assisted-classical-to-father Rule O adapter: Specified retained-environment EAC family, corrected vectorization cleanup and catalytic father adapter (hard)
Coherifying the new noisy-teleportation child regenerates mother: The constructed noisy-teleportation child family and its coherent regeneration map (hard)

Selected references

A family of quantum protocols, arXiv:quant-ph/0308044v2, https://arxiv.org/abs/quant-ph/0308044v2

19 thms2 active usersReviewed

Quantum Information·Captain: Goku

A New Approach to the Representation Thoery of the Symmetric Groups. 2Research Paper

Motivation

The new approach to the theory of complex representrations of the finite symmetric groups which based on the notions of Coxeter generators., Gelfand-Zetlin algebras, Hecke algebra, Young-Jucys-Murphi generators and which hardly used inductive structure - is systematically developed. The appearence of Young diagrams, tables is naturally explained - the set of content vectors of all Young tables is the spectra of Gel'fand-Zetlin algebra. The first steps of the theory (the list of the irrediucible representatinos, branching rule, Young orthopgonal form, Murnagan-Nakayama rule etc.)are established.This appraoch canbe used for other classical series, wreath products with symmetric groups. This paper is the revcised version of the paper of the same authors which was published in Selecta MAth. (New Series) V.2(1996).

This mission is the statement-level formalization of A New Approach to the Representation Thoery of the Symmetric Groups. 2 (arXiv:math/0503040v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5.8: Young branching, content spectrum, and equivalence relations (Theorem 5.8, PDF p. 22). 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.

Deferred results

23 results of the paper are not stated yet, because the library lacks an interface they need:

Proposition 1.1: The full general finite-group tower, its canonical class projectors/path lines, and the global diagonal subalgebra across all irreducibles. (hard)
Remark 1.2: Canonical lines and all GZ joint characters for an arbitrary simple-branching finite-group chain. (hard)
Remark 1.3: An arbitrary split finite-dimensional semisimple complex algebra tower with independent GZ and actual branching graph. (hard)
Theorem 2.4: A corrected general real-star-algebra criterion with explicitly stated representation hypotheses and the missing coefficient-invariance premise. (source-ambiguity)
Unnumbered classification of finite-dimensional irreducible H(2)-modules: An independently moderated corrected classification specifying both irreducible 1D/2D modules and, at b=a+/-1, the correctly labelled invariant submodule and quotient. Equal a=b must remain allowed in the generic 2D family. (source-ambiguity)
Remark 5.7: A precise infinite Young-path successor/predecessor map, its domain and exceptional-path convention, and the meaning of finite tableau orbit intervals. (source-ambiguity)
Unnumbered canonical seminormal construction (6.1), (6.2): The row-reading starting vector, character-product projectors, and the vectors constructed by (6.1), with length filtration. (hard)
Proposition 6.1: The constructed seminormal basis indexed by ordinary tableaux in each actual shape-labelled irreducible, together with rational descent. (hard)
Proposition 6.2: A normalized Young basis in an explicitly invariant positive definite Hermitian structure, coherently indexed by tableaux. (hard)
Remark 6.3: The actual shape-labelled row-reading starting tableau/vector and its lexicographic spectral weight. (hard)
Corollary 7.1: Shape-labelled actual restriction multiplicities, finite skew-path counts, and an explicit globally sharp factorial family. (hard)
Unnumbered two-step branching cases: The full two-level interval/multiplicity classification and scalar action on every extended canonical path. (hard)
Unnumbered uniqueness and normalization claims for deletion: A corrected and distinguished group-valued versus linear projection uniqueness statement, with an accurate threshold; the valid constructed-map identities are already stated separately. (source-ambiguity)
Proposition 7.2: A source-authorized correction distinguishing the group-valued preimage of the identity from the inverse image of all scalars under the linear extension; do not replace cycle deletion by coefficient truncation. (source-ambiguity)
Remark 7.4: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Theorem 8.1: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Murnaghan–Nakayama rule (unnumbered): The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Proposition 8.2: An actual ordinary shape-labelled irreducible trace character and the full-hook predicate/height, with the source shape association. (hard)
Proposition 8.3: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Proposition 8.4: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Proposition 8.5: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Unnumbered strengthening after Proposition 8.5: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
Proposition 8.6: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)

Selected references

A New Approach to the Representation Thoery of the Symmetric Groups. 2, arXiv:math/0503040v3, https://arxiv.org/abs/math/0503040v3

28 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

On the Douglas–Rachford Algorithm for Solving Possibly Inconsistent Optimization Problems: The Primal Shadows Converge Weakly, and in Value, to a Solution of the Normal ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.9

Milestones

Significance

Difficulty

Formalization scope

Selected references

Remarks on Cyclotomic and Degenerate Cyclotomic BMW AlgebrasResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Lectures on Symplectic Field Theory VI: Elliptic Regularity and Compactness of Pseudoholomorphic MapsTextbook

Motivation

Setting

Formalization targets

Goal: compactness of pseudoholomorphic discs

Milestones

Significance

Difficulty

Formalization scope

Selected references

Admissibility Conditions for Degenerate Cyclotomic BMW AlgebrasResearch Paper

Motivation

What is formalized

Selected references

Observable actions of algebraic groupsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Implementation of group-covariant POVMs by orthogonal measurementsResearch Paper

Motivation

What is formalized

Selected references

Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical SystemsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Skew shape representations are irreducibleResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type RepresentationsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

A general proof of Landauer-Büttiker formulaResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Cellularity and the Jones basic constructionResearch Paper

Motivation

What is formalized

Deferred results

Selected references

A Cocycle Model for Topological and Lie Group CohomologyResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Covariant quantum measurements which maximize the likelihoodResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite FieldsResearch Paper