BeamSplitter

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 (exponentialCoeff).

$$\forall alpha:\mathbb{C},(\forall n:\mathbb{N},(\mathrm{exponentialCoeff}\left(alpha,n\right)=\frac{(alpha{)}^n}{\mathrm{ComplexofReal}\left(\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{factorial}\left(n\right)\right)\right)\right)}))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.exponentialCoeff (✓ 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.2 (exponentialVector).

$$\forall alpha:\mathbb{C},(\mathrm{exponentialVector}\left(alpha\right)=\mathrm{lpmk}\left((n:\mathbb{N})\mapsto (\mathrm{exponentialCoeff}\left(alpha,n\right))\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.exponentialVector (✓ 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.

lp.mk forms the square-summable vector with the displayed coefficient function; its membership proof uses the complete exponential series. Proof fields are omitted in constructors.

Definition 1.3 (weylVector).

$$\forall alpha:\mathbb{C},(\forall beta:\mathbb{C},(\mathrm{weylVector}\left(alpha,beta\right)=\mathrm{smul}\left(\mathrm{Complexexp}\left(-(\mathrm{ComplexofReal}\left(\frac{(\Vert alpha\Vert {)}^2}{2}\right))-(\mathrm{conj}\left(alpha\right))\cdot (beta)\right),\mathrm{exponentialVector}\left(alpha+beta\right)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.weylVector (✓ 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 Weyl action on unnormalized exponential vectors includes its scalar phase and normalization factor.

Definition 1.4 (displacement).

$$\forall alpha:\mathbb{C},(\mathrm{displacement}\left(alpha\right)=\mathrm{extendOfIsometry}\left(\mathrm{LinearEquivrefl}\left(\mathbb{C},\mathrm{Finsupp}\left(\mathbb{C},\mathbb{C}\right)\right),\mathrm{linearCombination}\left(\mathbb{C},exponentialVector\right),\mathrm{linearCombination}\left(\mathbb{C},(beta:\mathbb{C})\mapsto (\mathrm{weylVector}\left(alpha,beta\right))\right)\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.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.

extendOfIsometry is Mathlib LinearEquiv.extendOfIsometry: the identity on finitely supported complex coefficient functions extends along the two displayed linearCombination maps. Density and equality of norms are proved in Lean; proof arguments are omitted. This specifies the global displacement on the Hilbert completion.

Definition 1.5 (coherentCoeff).

$$\forall alpha:\mathbb{C},(\forall n:\mathbb{N},(\mathrm{coherentCoeff}\left(alpha,n\right)=\frac{(\mathrm{ComplexofReal}\left(\mathrm{Realexp}\left(-(\frac{(\Vert alpha\Vert {)}^2}{2})\right)\right))\cdot ((alpha{)}^n)}{\mathrm{ComplexofReal}\left(\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{factorial}\left(n\right)\right)\right)\right)}))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.coherentCoeff (✓ 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.6 (coherent).

$$\forall alpha:\mathbb{C},(\mathrm{coherent}\left(alpha\right)=\mathrm{lpmk}\left((n:\mathbb{N})\mapsto (\mathrm{coherentCoeff}\left(alpha,n\right))\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.coherent (✓ 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.

Every complex alpha gives the normalized coherent vector exp(-|alpha|^2/2) alpha^n/sqrt(n!). The infinite series proves square summability and norm one. The displayed flattened identifiers Realexp and Complexexp denote Mathlib Real.exp and Complex.exp; ComplexofReal denotes Complex.ofReal, Functionconst denotes Function.const, and lpmk denotes lp.mk. Namespace components are retained while punctuation is omitted.

Definition 1.7 (tensor).

$$\forall v:\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),(\forall w:\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),(\mathrm{tensor}\left(v,w\right)=\mathrm{lpmk}\left((n:\mathbb{N})\mapsto (\mathrm{smul}\left(w\left(n\right),v\right))\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.tensor (✓ 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 second-mode coordinate n is w(n) times the first-mode vector v. The norm and inner product are the Hilbert tensor-product ones.

Definition 1.8 (exponentialPair).

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

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.exponentialPair (✓ 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.9 (rotate).

$$\forall t:\mathbb{R},(\forall r:\mathbb{R},(\forall z:\mathrm{Prod}\left(\mathbb{C},\mathbb{C}\right),(\mathrm{rotate}\left(t,r,z\right)=\mathrm{pair}\left((\mathrm{ComplexofReal}\left(t\right))\cdot (\mathrm{fst}\left(z\right))-(\mathrm{ComplexofReal}\left(r\right))\cdot (\mathrm{snd}\left(z\right)),(\mathrm{ComplexofReal}\left(r\right))\cdot (\mathrm{fst}\left(z\right))+(\mathrm{ComplexofReal}\left(t\right))\cdot (\mathrm{snd}\left(z\right))\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.rotate (✓ 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.

This real orthogonal rotation fixes the beam-splitter sign convention: creation operators give (t x+r y)^m(-r x+t y)^n.

Definition 1.10 (beamUnitary).

$$\forall t:\mathbb{R},(\forall r:\mathbb{R},(\forall h:(t{)}^2+(r{)}^2=1,(\mathrm{beamUnitary}\left(t,r,h\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{exponentialPair}\left(\mathrm{rotate}\left(t,r,z\right)\right))\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.beamUnitary (✓ 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 global unitary is the dense isometric extension of the rotation on exponential vectors. extendOfIsometry has the same convention as in displacement; its density and norm-equality proof arguments are omitted.

Definition 1.11 (beamSplitter).

$$\forall eta:\mathbb{R},(\forall hEta:eta\in \mathrm{SetIcc}\left(0,1\right),(\mathrm{beamSplitter}\left(eta,hEta\right)=\mathrm{beamUnitary}\left(\mathrm{sqrt}\left(eta\right),\mathrm{sqrt}\left(1-eta\right)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.beamSplitter (✓ 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.

Transmissivity lies in [0,1]. The coefficients are t=sqrt(eta), r=sqrt(1-eta); the unnamed proof argument of beamUnitary, derived from hEta, is omitted under the existing proof-argument convention.

Definition 1.12 (fockPair).

$$\forall m:\mathbb{N},(\forall n:\mathbb{N},(\mathrm{fockPair}\left(m,n\right)=\mathrm{tensor}\left(\mathrm{lpsingle}\left(2,m,\mathrm{ComplexofReal}\left(1\right)\right),\mathrm{lpsingle}\left(2,n,\mathrm{ComplexofReal}\left(1\right)\right)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.fockPair (✓ 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.13 (fockExpansion).

$$\forall t:\mathbb{R},(\forall r:\mathbb{R},(\forall m:\mathbb{N},(\forall n:\mathbb{N},(\mathrm{fockExpansion}\left(t,r,m,n\right)=\sum _{i:\mathrm{Fin}\left(m+1\right)}(\sum _{j:\mathrm{Fin}\left(n+1\right)}(\mathrm{smul}\left(\mathrm{ComplexofReal}\left(\frac{(((((((\mathrm{toReal}\left(\mathrm{choose}\left(m,\mathrm{val}\left(i\right)\right)\right))\cdot (\mathrm{toReal}\left(\mathrm{choose}\left(n,\mathrm{val}\left(j\right)\right)\right)))\cdot ((t{)}^{\mathrm{val}\left(i\right)}))\cdot ((r{)}^{\mathrm{NatSub}\left(m,\mathrm{val}\left(i\right)\right)}))\cdot ((-(r){)}^{\mathrm{val}\left(j\right)}))\cdot ((t{)}^{\mathrm{NatSub}\left(n,\mathrm{val}\left(j\right)\right)}))\cdot (\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{factorial}\left(\mathrm{val}\left(i\right)+\mathrm{val}\left(j\right)\right)\right)\right)))\cdot (\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{factorial}\left(\mathrm{NatSub}\left(m,\mathrm{val}\left(i\right)\right)+\mathrm{NatSub}\left(n,\mathrm{val}\left(j\right)\right)\right)\right)\right))}{(\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{factorial}\left(m\right)\right)\right))\cdot (\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{factorial}\left(n\right)\right)\right))}\right),\mathrm{fockPair}\left(\mathrm{val}\left(i\right)+\mathrm{val}\left(j\right),\mathrm{NatSub}\left(m,\mathrm{val}\left(i\right)\right)+\mathrm{NatSub}\left(n,\mathrm{val}\left(j\right)\right)\right)\right)))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.fockExpansion (✓ 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 two finite sums are the binomial expansion with factorial normalization. val is the natural value of a Fin index; NatSub is truncated natural subtraction. Every term has total occupation m+n.

Theorem 1.14 (beamUnitary_fock).

$$\forall t:\mathbb{R},(\forall r:\mathbb{R},(\forall h:(t{)}^2+(r{)}^2=1,(\forall m:\mathbb{N},(\forall n:\mathbb{N},(\mathrm{beamUnitary}\left(t,r,h,\mathrm{fockPair}\left(m,n\right)\right)=\mathrm{fockExpansion}\left(t,r,m,n\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.beamUnitary_fock (✓ 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 global unitary has this Fock action for every pair of natural occupations. Comparing against the total exponential family identifies the finite binomial expansion.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.beamSplitter
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.beamUnitary
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.beamUnitary_fock
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.coherent
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.coherentCoeff
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.displacement
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.exponentialCoeff
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.exponentialPair
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.exponentialVector
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.fockExpansion
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.fockPair
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.rotate
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.tensor
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter.weylVector