StrongAbsorptionCumulants

Abstract

StrongAbsorptionCumulants for the strong-absorption cumulant expansion.

Natural-number subtraction is truncated. Unmarked integrals use volume; real-number powers and division use the real field.

Definition 1.1 (claim).

$$claim=(\forall M:\mathbb{N},1\le M\to \forall n:\mathbb{N},2\le n\to \exists C{\gamma }_0:\mathbb{R},0<{\gamma }_0\wedge \forall \gamma :\mathbb{R},{\gamma }_0\le \gamma \to |(-1:\mathbb{R}{)}^n\cdot kappaMn\gamma -((n-1).factorial/((M:\mathbb{R}{)}^{2\cdot n-2}\cdot {\gamma }^{2\cdot n})-(2\cdot n-1)\cdot n\cdot (n-1).factorial/((M:\mathbb{R}{)}^{2\cdot n-2}\cdot {\gamma }^{2\cdot n+1}))|\le C/{\gamma }^{2\cdot n+2})$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorptionCumulants.claim (✓ std3).

Citation. M. Novaes (2023). Time delay statistics for chaotic cavities with absorption. DOI: 10.1007/s10955-023-03183-7. URL: https://arxiv.org/abs/2305.18235v1.

Commentary.

Novaes, Section 5, p. 7: “we conjecture that, for n > 1,” followed by Eq. (58). Natural n ≥ 2 expresses n > 1. The two coefficients and the absolute remainder bound refer to every M ≥ 1. The constants may depend on M and n.

Theorem 1.2 (result).

$$\forall M:\mathbb{N},1\le M\to \forall n:\mathbb{N},2\le n\to \exists C{\gamma }_0:\mathbb{R},0<{\gamma }_0\wedge \forall \gamma :\mathbb{R},{\gamma }_0\le \gamma \to |(-1:\mathbb{R}{)}^n\cdot kappaMn\gamma -((n-1).factorial/((M:\mathbb{R}{)}^{2\cdot n-2}\cdot {\gamma }^{2\cdot n})-(2\cdot n-1)\cdot n\cdot (n-1).factorial/((M:\mathbb{R}{)}^{2\cdot n-2}\cdot {\gamma }^{2\cdot n+1}))|\le C/{\gamma }^{2\cdot n+2}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorptionCumulants.result (✓ std3). ∎

Resolves. Problems/novaes-2023-strong-absorption-cumulants (proved) by D5/S3/Quantum/Transport/StrongAbsorptionCumulants.result.

Source. Repository-derived.

Acknowledgement. M. Novaes (2023). Time delay statistics for chaotic cavities with absorption. DOI: 10.1007/s10955-023-03183-7. URL: https://arxiv.org/abs/2305.18235v1.

Commentary.

For every positive channel number and every cumulant order at least two, the normalized law has the two strong-absorption coefficients of Novaes, Eq. (58).

Definition 1.3 (baseExpectation).

$$\forall (M:(\mathbb{N})),((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((baseExpectationMP=((\int p,baseWeightM(M:(\mathbb{R}))p\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P)/((partitionM(M:(\mathbb{R}))){)}^2)))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorptionCumulants.baseExpectation (✓ std3).

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

Definition 1.4 (singleWMoment).

$$\forall (M:(\mathbb{N})),((\forall (r:(\mathbb{N})),((singleWMomentMr=((\int x,laguerreWeightM(M:(\mathbb{R}))x\cdot (\mathrm{Finset}.\mathrm{univ}.\mathrm{expect}(funi\mapsto ((xi{)}^2)))\cdot ((\mathrm{Finset}.\mathrm{univ}.\mathrm{expect}x){)}^r)/partitionM(M:(\mathbb{R})))))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorptionCumulants.singleWMoment (✓ std3).

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

Theorem 1.5 (baseExpectation_add).

$$\forall (M:(\mathbb{N})),((((1\le M))\to ((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((\forall (Q:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((baseExpectationM(P+Q)=baseExpectationMP+baseExpectationMQ))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorptionCumulants.baseExpectation_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

Theorem 1.6 (law_polynomial_integrable).

$$\forall (M:(\mathbb{N})),((((1\le M))\to ((\forall (\gamma :(\mathbb{R})),((((0<\gamma ))\to ((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((Integrable(funp\mapsto (eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P))(lawM\gamma )))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorptionCumulants.law_polynomial_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

Theorem 1.7 (rescaled_pow_integrable).

$$\forall (M:(\mathbb{N})),((((1\le M))\to ((\forall (\gamma :(\mathbb{R})),((((0<\gamma ))\to ((\forall (r:(\mathbb{N})),((Integrable(funp\mapsto ((rescaledObservableM\gamma p{)}^r))(lawM\gamma )))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorptionCumulants.rescaled_pow_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

Theorem 1.8 (singleWMoment_derivative).

$$\forall (M:(\mathbb{N})),((((1\le M))\to ((\forall (r:(\mathbb{N})),((singleWMomentMr=iteratedDerivr(laguerreHwM)0))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorptionCumulants.singleWMoment_derivative (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

Theorem 1.9 (rescaledMomentExpansion).

$$\forall M:(\mathbb{N}),((1\le M)\to (\forall r:(\mathbb{N}),(FirstOrder((fun\gamma \mapsto (\mathrm{ProbabilityTheory}.\mathrm{moment}(rescaledObservableM\gamma )r(lawM\gamma ))))(expJet(gammaCGF(((M:(\mathbb{R})){)}^2))r)(correctionJet(gammaCGF(((M:(\mathbb{R})){)}^2))(correctionCGF(((M:(\mathbb{R})){)}^2))r))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorptionCumulants.rescaledMomentExpansion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed formula relates the polynomial integrals and the normalized finite-channel measure.

References

• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.baseExpectation
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.baseExpectation_add
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.claim
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.law_polynomial_integrable
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.rescaledMomentExpansion
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.rescaled_pow_integrable
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.result
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.singleWMoment
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorptionCumulants.singleWMoment_derivative
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/Density
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/Foundations
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments