DisplacementCovariance

Abstract

The full bosonic attenuator and the coherent-state output-entropy question.

The one-mode space is lp(Function.const(Nat,Complex),2) and the two-mode space is lp(Function.const(Nat,lp(Function.const(Nat,Complex),2)),2). The occupation vector at n is lp.single 2 n (Complex.ofReal 1). All state and environment supports are unrestricted. conjStarAlgEquiv is Mathlib LinearIsometryEquiv.conjStarAlgEquiv, mapping T to U composed with T and U inverse. Function names are the displayed Lean definitions or the explicitly stated Mathlib operations. Application parentheses retain grouping; NatSub is truncated natural subtraction, val is the natural value of a finite index, toReal is the natural-to-real cast and Complex.ofReal is the real-to-complex cast. Fields carrying proofs are omitted from constructor formulas; when a named proof parameter occurs in a function signature it appears as an argument of that function.

Definition 1.1 (mixture).

$$\forall iota:\mathrm{Type}\left(\right),(\forall v:iota\to \mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),(\mathrm{mixture}\left(iota,v\right)=\sum _{i:iota}^{\prime }(\mathrm{rankOne}\left(\mathbb{C},v\left(i\right),v\left(i\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.mixture (✓ std3).

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

The operator is the unconditional sum of rank-one projectors. In every state construction below, summability follows from summability of squared vector norms.

Definition 1.2 (purePartialTrace).

$$\forall v:\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),2\right),(\mathrm{purePartialTrace}\left(v\right)=\mathrm{mixture}\left(\mathbb{N},(n:\mathbb{N})\mapsto (v\left(n\right))\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.purePartialTrace (✓ std3).

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

For a two-mode pure vector the partial trace over the second mode is the sum of the projectors of all first-mode slices. Matrix elements are checked against the contraction by arbitrary first-mode test vectors.

Definition 1.3 (pairWeyl).

$$\forall a:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),(\forall z:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),(\mathrm{pairWeyl}\left(a,z\right)=\mathrm{tensor}\left(\mathrm{weylVector}\left(\mathrm{fst}\left(a\right),\mathrm{fst}\left(z\right)\right),\mathrm{weylVector}\left(\mathrm{snd}\left(a\right),\mathrm{snd}\left(z\right)\right)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.pairWeyl (✓ std3).

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

The displayed equation specifies the defining expression.

Definition 1.4 (pairDisplacement).

$$\forall a:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),(\mathrm{pairDisplacement}\left(a\right)=\mathrm{extendOfIsometry}\left(\mathrm{LinearEquivrefl}\left(\mathbb{C},\mathrm{Finsupp}\left(\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),\mathbb{C}\right)\right),\mathrm{linearCombination}\left(\mathbb{C},exponentialPair\right),\mathrm{linearCombination}\left(\mathbb{C},(z:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right))\mapsto (\mathrm{pairWeyl}\left(a,z\right))\right)\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.pairDisplacement (✓ std3).

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

The product displacement is the dense isometric extension of the two-mode Weyl family, using the same extendOfIsometry convention.

Theorem 1.5 (partialTrace_pairDisplacement).

$$\forall a:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),(\forall w:\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),2\right),(\mathrm{purePartialTrace}\left(\mathrm{pairDisplacement}\left(a,w\right)\right)=\mathrm{conjStarAlgEquiv}\left(\mathrm{displacement}\left(\mathrm{fst}\left(a\right)\right),\mathrm{purePartialTrace}\left(w\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.partialTrace_pairDisplacement (✓ std3). ∎

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

A displacement of the discarded mode cancels from every reduced matrix element, while the retained displacement conjugates the reduced operator.

Theorem 1.6 (beam_displacement).

$$\forall t:\mathbb{R},(\forall r:\mathbb{R},(\forall h:(t{)}^2+(r{)}^2=1,(\forall a:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),(\forall w:\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),2\right),(\mathrm{beamUnitary}\left(t,r,h,\mathrm{pairDisplacement}\left(a,w\right)\right)=\mathrm{pairDisplacement}\left(\mathrm{rotate}\left(t,r,a\right),\mathrm{beamUnitary}\left(t,r,h,w\right)\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.beam_displacement (✓ std3). ∎

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

The displacement commutation identity holds on the entire two-mode Hilbert completion, by continuity from the total exponential family.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.beam_displacement
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.mixture
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.pairDisplacement
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.pairWeyl
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.partialTrace_pairDisplacement
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance.purePartialTrace
• Dependency: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter