- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
For real \(t\), the exponential generating series of the target-chain coefficients is
The absolute value of time gives the same series for \(t\) and \(-t\).
For a finite family \(\mathcal F\) and weights \(w_X\), define recursively
Repeated supports are permitted in the chain.
For \(a\in \mathbb {Z}^2\) and a nonnegative integer \(R\), let \(D_R(a)=\{ x\in \mathbb {Z}^2:\ell (a,x)\le R\} \) be the finite lattice diamond.
For \(a,b\in \mathbb {Z}^2\), set \(\ell (a,b)=|a_1-b_1|+|a_2-b_2|\). In particular, \(\ell (a,a)=0\).
Fix an integer \(R\ge 0\) and \(J{\gt}0\). For each nonempty \(X\subseteq \Lambda \) with \(\operatorname {diam}_{d_\Lambda }X\le R\), assign one Hermitian operator \(h_X\) supported on \(X\), with \(\| h_X\| \le J\). The assigned operator may be zero, and acts as the identity on the complementary tensor factors. Define
The norm is the Euclidean operator norm. Boundary edges are unordered and counted once; empty and full cuts have empty boundary.
- TNLean.PEPS.AreaLaw.IsAdmissibleSupport
- TNLean.PEPS.AreaLaw.AdmissibleSupport
- TNLean.PEPS.AreaLaw.LocalHamiltonian
- TNLean.PEPS.AreaLaw.LocalHamiltonian.operator
- TNLean.PEPS.AreaLaw.LocalHamiltonian.operator_isHermitian
- TNLean.PEPS.AreaLaw.LocalHamiltonian.zero
- TNLean.PEPS.AreaLaw.localLift
- TNLean.PEPS.AreaLaw.localLift_mem_supportedOperators
- TNLean.PEPS.AreaLaw.localLift_eq_entropyLocalLift
- TNLean.PEPS.AreaLaw.edgeBoundary
- TNLean.PEPS.AreaLaw.edgeBoundary_empty
- TNLean.PEPS.AreaLaw.edgeBoundary_univ
For a target \(y\in V\) and a finite support \(X\), define
Thus the initial support is tested at \(n=0\), and a support may be revisited at subsequent steps.
Suppose \(|V|\ge 2\). Choose a connected spanning subgraph \(T\subseteq G\), a root \(r\in V\), and, at every vertex \(v\), an incident edge \(p(v)\) of \(T\). For \(\psi \colon \Sigma \to \mathbb {C}\), assign bond dimensions \(D_e=N\) when \(e\in T\) and \(D_e=1\) otherwise. Decode each active edge index as a configuration \(\tau _e\in \Sigma \), and define
The one-dimensional indices on \(E\setminus T\) do not enter the components.
- TNLean.PEPS.ExactTreeRepresentation.configurationEquiv
- TNLean.PEPS.ExactTreeRepresentation.bondDim
- TNLean.PEPS.ExactTreeRepresentation.decode
- TNLean.PEPS.ExactTreeRepresentation.encode
- TNLean.PEPS.ExactTreeRepresentation.Ports
- TNLean.PEPS.ExactTreeRepresentation.Ports.ofConnected
- TNLean.PEPS.ExactTreeRepresentation.localLabel
- TNLean.PEPS.ExactTreeRepresentation.IsConsistent
- TNLean.PEPS.ExactTreeRepresentation.tensor
Attach every party to a dyadic block, and so to its anchor. Each link, oriented arbitrarily, is routed from the anchor of its first party horizontally to the column of the anchor of its second party, then vertically to that anchor. The load of a unit edge of the padded square is the number of steps of all these walks that traverse it, counted with repetition. On the padded square of side \(N=8\), with \(L=5\), the square, the rounded marks and the blue dots below are the anchors of scales \(3\), \(2\) and \(1\), the arrow is one routed link from \(P\) to \(Q\), and the shaded square is the genuine \(L\times L\) square, onto which the fold \(f\) of Definition 27.132.4 maps the endpoint \(Q\).
The assertion is the following. For every integer \(q\ge 2\) and all reals \(J,\Delta {\gt}0\) there are reals \(C,C_1,k\) and natural numbers \(B,\Delta _0,c,L_0\) such that for every integer \(L\ge \max \{ 2,L_0\} \) and every \((H,E_0,\Omega )\in \mathcal G_{q,J,\Delta }(L)\) there is an operator party network with the following properties. Every party is attached to a dyadic block inside the padded square, with at most \(B\) parties per block; every party has at most \(\Delta _0\) links; the two anchors of every link differ in each coordinate by at most \(c\) times the side of either endpoint block; every link dimension is at most \(C_1L^k\); and the operator \(\sigma \) of the network, with the physical pair of each party read at the fold of its anchor, satisfies
The constants are chosen before \(L,H,E_0,\Omega \). This is the conclusion of [ 248 , Section 8.1 ] (07-assembly.tex, lines 53–63), with the anchors of lines 102–114 and the network properties of Proposition 7.1 used in the proof of Lemma 8.2 (lines 128–131).
An operator party network is a party network whose physical index at each party is an output-input pair in \(\{ 1,\ldots ,q\} ^2\). When the pair of party \(p\) is read at the site \(\iota (p)\), the operator \(\sigma \) of the network has the entry \(\langle \tau |\sigma |\rho \rangle \) equal to the coefficient of the network at the configuration \(v\mapsto (\tau (v),\rho (v))\). For a product-basis input \(z\), fixing the input of every party \(p\) to \(z(\iota (p))\) gives a party network with physical dimension \(q\), the same links, and the same link dimensions.
The map \(E_K\) on the operators of \((\mathbb {C}^q)^{\otimes I}\) defined above.
Adjacent sites of \(\Lambda \) have ambient displacement one, and at most \(2(d+1)^2\) sites lie at distance exactly \(d\) from any site. Every original support has \(d_\Lambda \)-diameter at most \(R\) and at most \(v_R\) sites, and for every site \(x\),
- TNLean.PEPS.AreaLaw.latticeL1Distance_le_one_of_domainGraph_adj
- TNLean.PEPS.AreaLaw.card_domainGraph_sphere_le
- TNLean.PEPS.AreaLaw.IsAdmissibleSupport.edist_le
- TNLean.PEPS.AreaLaw.IsAdmissibleSupport.card_le
- TNLean.PEPS.AreaLaw.LocalHamiltonian.normBound_nonneg
- TNLean.PEPS.AreaLaw.LocalHamiltonian.sum_norm_term_containing_le
For \(q\geq 1\), the map \(E_K\) takes values in \(\mathcal A_K\), fixes every operator in \(\mathcal A_K\), is unital, completely positive and trace preserving, and is a contraction in operator norm.
Let \(q\ge 1\). There are positive constants \(C,v,c\), depending only on \(q,R,J\), with the following property. For every domain \(\Lambda \), every Hamiltonian \(H\) as above, every original support \(X\) with anchor \(a\in X\), every operator \(A\) supported in \(X\), every site \(y\), every on-site operator \(B_y\) at \(y\), and every real \(t\),
when \(d_\Lambda (a,y){\lt}\infty \), and the commutator is zero when \(d_\Lambda (a,y)=\infty \). Moreover, for every integer \(l\ge 0\),
This is [ 247 , Lemma 4.1 ] . Explicitly, for every \(\mu \ge 0\) and every integer \(n\le d_\Lambda (a,y)\), \(\| [\tau _t(A),B_y]\| \le 2e^{\mu R}\| A\| \| B_y\| \exp (2v_R\mu _RJe^{2\mu R}|t|-\mu n)\).
Under the common-range hypotheses of Theorem 36.1.1, \(d_G(x,y)\le (m+1)R\), and \(x,y\) belong to the same connected component. Consequently no such chain exists when the components differ, when \(d_G(x,y)=\infty \), or when \((m+1)R{\lt}d_G(x,y)\).
Under the hypotheses of Theorem 36.5.4, let \(d_G(a,y)=D\) for a nonnegative integer \(D\), and let \(\mu \ge 0\). Put \(\kappa =vb\). Then
Under the hypotheses of Theorem 36.6.1, the series in (11) converges and satisfies
This bounds the scalar interaction-chain series used in the proof of [ 247 , Lemma 4.1 ] .
Assign a nonnegative integer range \(r(X)\) to each support \(X\subseteq V\). Let \(X_0,\ldots ,X_m\) satisfy \(X_j\cap X_{j+1}\ne \varnothing \), and suppose any two sites of \(X_j\) can be joined by a walk in \(G\) of length at most \(r(X_j)\). If \(x\in X_0\) and \(y\in X_m\), there is a walk from \(x\) to \(y\) of length at most \(\sum _{j=0}^m r(X_j)\). For the common range \(R\), this is \((m+1)R\).
Let \(V\) be a finite graph embedded injectively in \(\mathbb {Z}^2\), with edge displacement at most one. Let \(\mathcal F\) be a finite family of distinct finite supports such that any two sites in a support admit a walk in the full graph of length at most the nonnegative integer \(R\). Put \(v_R=1+2R(R+1)\) and \(\mu _R=2^{v_R-1}\). Each original support has at most \(v_R\) sites, and at most \(\mu _R\) original supports contain any specified site. For \(J\ge 0\) and real weights \(w_X\le J\),
If also \(w_X\ge 0\) for each \(X\in \mathcal F\), then
The continuation bound holds for each original support \(X\) and permits repetitions. Both bounds apply to \(w_X=\lVert h_X\rVert \) for elements \(h_X\) of any seminormed additive group with \(\lVert h_X\rVert \le J\). These are the interaction budgets used in [ 247 , Sections 2 and 4 ] .
- TNLean.PEPS.AreaLaw.card_support_le_diamond
- TNLean.PEPS.AreaLaw.card_supports_containing_le_diamond
- TNLean.PEPS.AreaLaw.sum_supportWeights_containing_le_diamond
- TNLean.PEPS.AreaLaw.sum_supportNorms_containing_le_diamond
- TNLean.PEPS.AreaLaw.interactionChainWeightSum_le_diamond_pow
- TNLean.PEPS.AreaLaw.interactionChainWeightSum_norm_le_diamond_pow
The diamond \(D_R(a)\) has cardinality \(v_R=1+2R(R+1)\). Let \(\iota :V\to \mathbb {Z}^2\) be injective. A finite set \(S\subseteq V\) with \(\ell (\iota (a),\iota (x))\le R\) for each \(x\in S\) has at most \(v_R\) elements. If every graph edge has displacement at most one, the same bound holds when every \(x\in S\) is reached from \(a\) by a graph walk of length at most \(R\), or when \(d_G(a,x)\le R\). This is the local counting bound of [ 247 , Section 2 ] .
Fix integers \(q\geq 1\) and \(R\geq 0\), and a real number \(J\). There are positive constants \(C,v,c\) with the following property. Let \(\Lambda \subseteq \mathbb {Z}^2\) be any finite domain, and let \(H\) be a finite-range Hamiltonian of range \(R\) and term-norm bound \(J\) on \(\Lambda \). For a region \(S\subseteq \Lambda \), write \(N_l(S)=\{ y\in \Lambda :d_\Lambda (y,S)\leq l\} \), with \(N_l(\varnothing )=\varnothing \). If \(A\) is supported on \(S\), then for every integer \(l\geq 0\) and real \(t\),
Empty domains and empty regions are included. This is the operator localization estimate used in [ 248 ] .
For nonnegative weights on a finite family of distinct supports and any finite region \(S\),
If each inner site sum is at most \(b\), the left side of (1) is at most \(|S|b\).
Let \(B\) be a finite neighborhood and let \(\mathcal F\) be a finite family of distinct subsets of \(B\), each containing \(a\). Then \(|\mathcal F|\le 2^{|B\setminus \{ a\} |}\). If \(a\in B\), this equals \(2^{|B|-1}\).
Fix integers \(q\geq 1\) and \(R\geq 0\), and a real number \(J\). There are positive constants \(C,v,c\) with the following property. Let \(\Lambda \subseteq \mathbb {Z}^2\) be a finite domain, let \(H'\) be a Hamiltonian of range \(R\) and term-norm bound \(J\) on \(\Lambda \), and let \(H\) be any Hermitian operator on the same space. Suppose that \(W\) acts on \(Q\subseteq \Lambda \) and that \(D=H'-H\) acts on \(Z\subseteq \Lambda \). For each integer \(l\geq 0\), put \(B=N_l(Q\cup Z)\), where distance is measured in the induced graph. There is a differentiable path \(U\) such that
For every real \(t\), the operator \(U(t)\) is unitary and acts on \(B\). Choose this path before the Gaussian variance and time cutoff. For every \(\eta \geq 0\) and \(T\geq 0\), let \(\gamma _\eta \) be the centered Gaussian measure of variance \(\eta \), and define
Then \(M_{\eta ,T}\) acts on \(B\), its norm is at most \(\| W\| \), and
The integrals retain their original Gaussian mass. Zero variance, empty domains and empty regions are included. This is the supported Gaussian approximation used in [ 248 ] .
If \(w_Y\ge 0\) for each \(Y\in \mathcal F\), then \(0\le T_n^y(X)\le W_n(X)\) for every finite support \(X\) and every \(n\ge 0\).
Under the range hypotheses of Theorem 36.5.3, suppose \(w_Y\ge 0\), \(|Y|\le v\) for each \(Y\in \mathcal F\), and \(\sum _{Y\in \mathcal F:\, x\in Y}w_Y\le b\) for every site \(x\), where \(v\) is a nonnegative integer and \(b\ge 0\). For \(X\in \mathcal F\), \(a\in X\), and \(n\ge 0\),
In the finite lattice setting of Theorem 36.4.3, one may take \(v=v_R\) and \(b=\mu _RJ\).
Suppose every pair of sites in each \(X\in \mathcal F\) admits a walk of length at most the nonnegative integer \(R\). Fix \(X\in \mathcal F\) and an anchor \(a\in X\). For arbitrary real weights, \(T_n^y(X)=0\) whenever there is no walk from \(a\) to \(y\) of length at most \((n+1)R\). In particular, it vanishes if \((n+1)R{\lt}d_G(a,y)\), including \(d_G(a,y)=\infty \).
The function \(\ell \) satisfies the triangle inequality. Let \(\iota :V\to \mathbb {Z}^2\) assign integer coordinates such that each graph edge has displacement at most one. A walk \(p\) from \(a\) to \(b\) then satisfies \(\ell (\iota (a),\iota (b))\le |p|\). If \(d_G(a,b)\le R{\lt}\infty \), the displacement is at most \(R\).
The uniform polynomial approximation assertion
is equivalent to
In both assertions, the constants are chosen before the size, Hamiltonian, energy, and ground vector.
Fix \(\sigma \in \Sigma \). If all factors in \(\prod _{v\in V}A_v((\tau _e)_{e\ni v},\sigma (v))\) are nonzero, then \(\tau _e=\sigma \) for every \(e\in T\). Conversely, this virtual assignment satisfies all equality constraints.
- TNLean.PEPS.ExactTreeRepresentation.decode_encode
- TNLean.PEPS.ExactTreeRepresentation.decode_injective
- TNLean.PEPS.ExactTreeRepresentation.localLabel_encode
- TNLean.PEPS.ExactTreeRepresentation.isConsistent_encode
- TNLean.PEPS.ExactTreeRepresentation.tensor_component_encode
- TNLean.PEPS.ExactTreeRepresentation.isConsistent_of_component_ne_zero
- TNLean.PEPS.ExactTreeRepresentation.localLabel_eq_of_adj
- TNLean.PEPS.ExactTreeRepresentation.localLabel_eq_of_consistent
- TNLean.PEPS.ExactTreeRepresentation.eq_encode_of_consistent
- TNLean.PEPS.ExactTreeRepresentation.tensor_product_eq_zero
A connected graph with one vertex represents every coefficient function by its single physical tensor. Thus every finite connected graph admits the exact representation with positive bonds bounded by \(q^{|V|}\). For an empty vertex set, however, the contraction is the scalar one for every tensor family.
Fix integers \(q\ge 1\) and \(L_0\ge 0\), and real numbers \(C\) and \(c\ge 0\). Set \(C'=\max \{ C,q^{L_0^2}\} \). For every integer \(0{\lt}L\le L_0\) and every unit vector \(\Omega \) on the open \(L\times L\) square, there is a nonzero PEPS \(\Phi \) on that square with \(1\le D_e\le C'L^c\) on every edge and a real phase \(\theta \) such that \(\| \| \Phi \| ^{-1}\Phi -e^{i\theta }\Omega \| \le L^{-1}\). This is the finite-size part of [ 248 , Section 8 ] (07-assembly.tex, lines 203–214).
Fix \(q\ge 1\) and \(L_0\in \mathbb {N}\). For every \(0{\lt}L\le L_0\), every vector on the open \(L\times L\) square grid has an exact PEPS with positive bonds at most \(C_0=q^{L_0^2}\). This bound is independent of the vector and any Hamiltonian. For any \(C\in \mathbb {R}\) and \(r\ge 0\), the enlarged prefactor \(\max \{ C,C_0\} \) gives \(D_e\le \max \{ C,C_0\} L^r\) throughout the same range. If \(\chi {\gt}0\), then \(C_\chi =\max \{ C,C_0^{1/\chi }\} \) gives \(D_e\le (C_\chi L^r)^\chi \) on this range as well.
For \(q,L\ge 1\), every vector \(\psi \) on the open \(L\times L\) square grid has an exact PEPS with \(1\le D_e\le q^{L^2}\). For \(L\ge 2\), the dimensions can be chosen as \(q^{L^2}\) on a spanning tree and one off that tree. If \(\| \psi \| =1\), its contraction \(\Phi \) satisfies \(\Phi =\psi \), \(\| \Phi \| =1\), and \(\| \| \Phi \| ^{-1}\Phi -1\cdot \psi \| =0\).
For every finite connected graph with \(|V|\ge 2\) and every \(\psi \colon \Sigma \to \mathbb {C}\), there are a spanning tree \(T\subseteq G\) and tensors with dimensions \(D_e=N\) on \(T\) and \(D_e=1\) off \(T\) such that
Every bond is positive and at most \(q^{|V|}\). If \(\psi \ne 0\), then \(c_A\ne 0\).
- TNLean.PEPS.ExactTreeRepresentation.stateCoeff_tensor
- TNLean.PEPS.ExactTreeRepresentation.stateCoeff_tensor_eq
- TNLean.PEPS.ExactTreeRepresentation.stateCoeff_tensor_ne_zero
- TNLean.PEPS.ExactTreeRepresentation.bondDim_pos
- TNLean.PEPS.ExactTreeRepresentation.bondDim_le
- TNLean.PEPS.ExactTreeRepresentation.exists_exact_tree_tensor
If the assertion of Definition 36.12.1.2 holds, then the uniform polynomial approximation assertion (27) holds: for every \(q\ge 2\) and \(J,\Delta {\gt}0\) there are \(C',c'{\gt}0\) such that \(\mathcal A_{C',c'}(L,\Omega )\) for every \(L\ge 2\) and every \((H,E_0,\Omega )\in \mathcal G_{q,J,\Delta }(L)\). This is the argument of [ 248 , Section 8 ] (07-assembly.tex, lines 53–214) after the compressed network has been obtained.
In the setting of Theorem 27.132.1.3, suppose that every link dimension is at most \(C_1L^k\) with \(C_1\ge 1\) and \(k\ge 0\), and that \(2\eta \le L^{-1}\). Then the nonzero PEPS has every bond dimension at most
and normalized error at most \(L^{-1}\), up to a phase. This is the final bond bound of [ 248 , Section 8.3 ] (07-assembly.tex, lines 164–170) for the routed column.
Fix integers \(q\ge 1\) and \(L_0\ge 0\), real \(J,\Delta ,C\), and \(c\ge 0\). Suppose \(\mathcal A_{C,c}(L,\Omega )\) holds for every integer \(L\ge \max \{ 2,L_0\} \) and every \((H,E_0,\Omega )\in \mathcal G_{q,J,\Delta }(L)\). There is one \(C'{\gt}0\) with \(C'\ge C\) such that \(\mathcal A_{C',c}(L,\Omega )\) holds for every integer \(L\ge 2\) and every \((H,E_0,\Omega )\in \mathcal G_{q,J,\Delta }(L)\). The exponent \(c\) is unchanged, and \(C'\) is independent of \(L,H,E_0,\Omega \). This is the finite-size argument in [ 248 , Section 8 ] (07-assembly.tex, lines 203–214).
The open \(w\times h\) nearest-neighbor grid is the Cartesian product of the path graphs on \(w\) and \(h\) vertices. It is connected exactly when \(w,h{\gt}0\). If \(L\ge 2\), its \(L\times L\) vertex set has at least two elements.
Fix integers \(q\ge 1\) and \(L_0\ge 0\), and real numbers \(C\) and \(c\ge 0\). There is a constant \(C'{\gt}0\) with \(C'\ge C\) such that, for every integer \(2\le L{\lt}L_0\) and every unit vector \(\Omega \) on the open \(L\times L\) square, there is a nonzero PEPS \(\Phi \) on that square with \(1\le D_e\le C'L^c\) on every edge and a real phase \(\theta \) satisfying \(\| \| \Phi \| ^{-1}\Phi -e^{i\theta }\Omega \| \le L^{-1}\). The constant is chosen before \(L\) and \(\Omega \), as required for the finite-size argument in [ 248 , Section 8 ] (07-assembly.tex, lines 203–214).
Let \(\mathcal A\) be a complete real normed star algebra satisfying the \(C^*\) identity, and let \(K^*=-K\). For \(A,B\in \mathcal A\) and real \(t\),
In the setting of Theorem 33.9.10, with \(q\geq 1\), assume that at most \(K_g(d+1)^k\) sites lie at distance exactly \(d\) from any site. Let \(N_l(a)=\{ x:d_G(a,x)\leq l\} \). Then
with \(v=2v_Rb_0e^{2R}\) and \(C=2e^RK_g\, 2^kk!\, e^{1/2}/(1-e^{-1/2})\).
In this setting let \(A\in \mathcal A_{X_i}\), let \(y\) be a site, and let \(B\in \mathcal A_{\{ y\} }\). For every \(\mu \geq 0\), every integer \(0\leq n\leq d_G(a_i,y)\) and every real \(t\),
Consequently there are positive constants \(C,v,c\), depending only on \(R,v_R,b_0\), such that \(\| [\tau _t(A),B]\| \leq C\| A\| \| B\| e^{v|t|-cd_G(a_i,y)}\) whenever \(d_G(a_i,y){\lt}\infty \), and \([\tau _t(A),B]=0\) otherwise. The constants do not depend on the number of sites, on \(q\), or on the graph.
Let \(I\) be a finite set of sites, let \(q\geq 1\), and let \(K\subseteq I\). Let \(H'\) and \(H\) be Hermitian operators on \((\mathbb {C}^q)^{\otimes I}\), and put \(G_K(t)=E_K(e^{itH'}(H'-H)e^{-itH'})\). There is a unique differentiable path \(U\) satisfying
For every real \(t\), the operator \(U(t)\) is unitary and acts on \(K\). Moreover, for any real \(t,\varepsilon \), if
for all \(s\) between \(0\) and \(t\), then
Empty site sets and empty regions are included. This is the supported relative evolution used in [ 248 ] .