SecondOrderDensity

Abstract

SecondOrderDensity for strong-absorption moments.

Real arithmetic is used in all coefficients. Integrals without an explicit measure use volume. M is the channel count; n is the moment order.

Definition 1.1 (quadraticDensityPoly).

$$\forall (M:(\mathbb{N})),((quadraticDensityPolyM=(C(1/2:(\mathbb{R}))\cdot (((linearDensityPolyM){)}^2-C(M:(\mathbb{R}))\cdot ((\sum i:FinM,((X(\mathrm{Sum}.\mathrm{inl}i)){)}^2)+(\sum j:FinM,((X(\mathrm{Sum}.\mathrm{inr}j)){)}^2))+C2\cdot (\sum i:FinM,X(\mathrm{Sum}.\mathrm{inl}i))\cdot (\sum j:FinM,X(\mathrm{Sum}.\mathrm{inr}j))))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/SecondOrderDensity.quadraticDensityPoly (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity is used to evaluate the strong-absorption coefficients.

Theorem 1.2 (law_polynomial_secondOrder).

$$\forall (M:(\mathbb{N})),((((1\le M))\to (((((\int p,baseWeightM(M:(\mathbb{R}))p\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(quadraticDensityPolyM))=0))\to ((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),(((fun\gamma \mapsto ((\int p,eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)PdlawM\gamma )-(\int p,baseWeightM(M:(\mathbb{R}))p\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P)/((partitionM(M:(\mathbb{R}))){)}^2-(\gamma {)}^{-1}\cdot ((\int p,baseWeightM(M:(\mathbb{R}))p\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(P\cdot linearDensityPolyM))/((partitionM(M:(\mathbb{R}))){)}^2)-((\gamma {)}^{-1}{)}^2\cdot ((\int p,baseWeightM(M:(\mathbb{R}))p\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(P\cdot quadraticDensityPolyM))/((partitionM(M:(\mathbb{R}))){)}^2))){=}^O[atTop](fun\gamma :(\mathbb{R})\mapsto (((\gamma {)}^{-1}{)}^3))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorption/SecondOrderDensity.law_polynomial_secondOrder (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used to evaluate the strong-absorption coefficients.

References

• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/SecondOrderDensity.law_polynomial_secondOrder
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/SecondOrderDensity.quadraticDensityPoly
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/Density
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/Foundations
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments