PhyslibAlpha.ProbabilisticTheory.LocalNet.Region

Regions of a physical system

Regions ordered by inclusion, with separation and enlargement added only when needed.

i. Overview

An extended system, such as a crystal, a spin chain or a field in space-time, is studied through the regions in which it is probed. Regions are ordered by inclusion: `X ≤ Y` means that `X` lies inside `Y`. Nothing else is required at first: no coordinates, no distance, no notion of site. Further structure is added separately, only where a theory needs it:

| Capability | Physical meaning | Lean notion | |---|---|---| | empty region | no physical support | `OrderBot R` | | union | measuring in two regions at once | `SemilatticeSup R` | | directedness | any two regions fit inside a common one | `IsDirected R (· ≤ ·)` | | separation | disjoint sites, or spacelike separation | `HasSeparation R` | | enlargement | how far a disturbance can spread | `HasEnlargement R` |

Directedness is what allows one to speak of the whole infinite system, and is not imposed on every region structure. The enlargement `enlarge r X` of a region is the set of points within distance `r` of it: a disturbance travelling at speed at most `v` for a time `t` stays inside `enlarge (v * t) X`.

ii. Key results

- `HasSeparation` : two regions are separated, symmetrically, and so are their subregions. - `HasEnlargement` : the neighborhood of a region of a given radius, obeying the triangle inequality.

iii. Table of contents

A. Separation
B. Enlargement

iv. References

* R. Haag, Local Quantum Physics, 2nd ed., Chapter III. * E. Lieb & D. Robinson, The finite group velocity of quantum spin systems.

A. Separation

B. Enlargement

4 declarations

theorem

Symmetry of the separation relation

#sep_comm

In a physical system with a notion of separation, for any two regions $X$ and $Y$ , $X$ is separated from $Y$ if and only if $Y$ is separated from $X$ .

theorem

Left Monotonicity of the Separation Relation

#mono_left

Suppose $R$ is a collection of regions in a physical system equipped with an inclusion relation $\le$ and a separation relation $\text{Sep}$ . For any regions $X, X', Y \in R$ , if $X$ and $Y$ are separated ( $\text{Sep}(X, Y)$ ) and $X'$ is a subregion of $X$ ( $X' \le X$ ), then $X'$ and $Y$ are also separated ( $\text{Sep}(X', Y)$ ).

theorem

$\text{Sep } X\ Y \text{ and } Y' \leq Y \implies \text{Sep } X\ Y'$

#mono_right

Let $X, Y,$ and $Y'$ be regions in a physical system. If $X$ and $Y$ are separated, denoted as $\text{Sep } X\ Y$ , and $Y'$ is a subregion of $Y$ (meaning $Y' \leq Y$ ), then $X$ and $Y'$ are also separated.

theorem

$X \le \text{enlarge}(r, X)$

#le_enlarge

For any region $X$ and any non-negative real number $r \in \mathbb{R}_{\ge 0}$ , the region $X$ is contained within its enlargement by radius $r$ , denoted as $X \le \text{enlarge}(r, X)$ . In this context, $\le$ represents the partial order of inclusion between regions.

PhyslibAlpha.ProbabilisticTheory.LocalNet.Region

Regions of a physical system

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Separation

B. Enlargement

Symmetry of the separation relation

Left Monotonicity of the Separation Relation

Sep X Y and Y′≤Y ⟹ Sep X Y′\text{Sep } X\ Y \text{ and } Y' \leq Y \implies \text{Sep } X\ Y'Sep X Y and Y′≤Y⟹Sep X Y′

X≤enlarge(r,X)X \le \text{enlarge}(r, X)X≤enlarge(r,X)

$\text{Sep } X\ Y \text{ and } Y' \leq Y \implies \text{Sep } X\ Y'$

$X \le \text{enlarge}(r, X)$