LaguerreMoments

Abstract

LaguerreMoments 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 (deltaSq).

$$\forall (M:\mathbb{N}),\forall (x:FinM\to \mathbb{R}),deltaSqMx=(\prod i,\prod j,ifi<jthen(xi-xj{)}^{2}else1)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.deltaSq (✓ std3).

Source. Repository-derived.

Commentary.

The squared Vandermonde product.

Definition 1.2 (deltaPoly).

$$\forall (M:\mathbb{N}),deltaPolyM=(\prod i,\prod j,ifi<jthen(\mathrm{MvPolynomial}.Xi-\mathrm{MvPolynomial}.Xj{)}^{2}else1)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.deltaPoly (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Definition 1.3 (expJet).

$$\forall (K:\mathbb{R}\to \mathbb{R}),\forall (r:\mathbb{N}),expJetKr=(iteratedDerivr(funt\mapsto \mathrm{Real}.\exp (Kt))0)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.expJet (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Definition 1.4 (correctionJet).

$$\forall (K:\mathbb{R}\to \mathbb{R}),\forall (B:\mathbb{R}\to \mathbb{R}),\forall (r:\mathbb{N}),correctionJetKBr=(iteratedDerivr(funt\mapsto \mathrm{Real}.\exp (Kt)\cdot Bt)0)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.correctionJet (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Theorem 1.5 (exp_deriv_near).

$$\forall (K:\mathbb{R}\to \mathbb{R}),(AnalyticAt\mathbb{R}K0)\to deriv(funt\mapsto \mathrm{Real}.\exp (Kt)){=}^f[nhds0](funt\mapsto derivKt\cdot \mathrm{Real}.\exp (Kt))$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Definition 1.6 (laguerreWeight).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),\forall (x:FinM\to \mathbb{R}),laguerreWeightMax=(if\forall i,0\le xithen\mathrm{Real}.\exp (-a\cdot \sum i,xi)\cdot deltaSqMxelse0)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeight (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Theorem 1.7 (deltaPoly_eval).

$$\forall (M:\mathbb{N}),\forall (x:FinM\to \mathbb{R}),\mathrm{MvPolynomial}.\mathrm{eval}x(deltaPolyM)=deltaSqMx$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.8 (deltaSq_nonneg).

$$\forall (M:\mathbb{N}),\forall (x:FinM\to \mathbb{R}),0\le deltaSqMx$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.9 (exp_jet_recurrence).

$$\forall (K:\mathbb{R}\to \mathbb{R}),\forall (n:\mathbb{N}),(AnalyticAt\mathbb{R}K0)\to (K0=0)\to iteratedDeriv(n+1)K0=expJetK(n+1)-\sum i\in rangen,(n.\mathrm{choose}i:\mathbb{R})\cdot iteratedDeriv(i+1)K0\cdot expJetK(n-i)$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.10 (gammaCGF_analytic).

$$\forall (d:\mathbb{R}),AnalyticAt\mathbb{R}(gammaCGFd)0$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.11 (correctionCGF_analytic).

$$\forall (d:\mathbb{R}),AnalyticAt\mathbb{R}(correctionCGFd)0$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.12 (FirstOrder.congr_eventually).

$$\forall (f:\mathbb{R}\to \mathbb{R}),\forall (g:\mathbb{R}\to \mathbb{R}),\forall (a:\mathbb{R}),\forall (b:\mathbb{R}),(FirstOrderfab)\to (f{=}^f[atTop]g)\to FirstOrdergab$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Definition 1.13 (partition).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),partitionMa=(\int x,laguerreWeightMax)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.partition (✓ std3).

Source. Repository-derived.

Commentary.

The integral of the Laguerre weight on the nonnegative orthant.

Theorem 1.14 (laguerreWeight_integrable).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),(0<a)\to Integrable(laguerreWeightMa)$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.15 (laguerreWeight_nonneg).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),\forall (x:FinM\to \mathbb{R}),0\le laguerreWeightMax$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.16 (laguerrePolynomial_integrable).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),\forall (P:MvPolynomial(FinM)\mathbb{R}),(0<a)\to Integrable(funx\mapsto laguerreWeightMax\cdot evalxP)$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.17 (singleWPoly_eval).

$$\forall (M:\mathbb{N}),\forall (x:FinM\to \mathbb{R}),evalx(\mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}(funi:FinM\mapsto ((Xi{)}^2:MvPolynomial(FinM)\mathbb{R})))=(\mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}(funi\mapsto (xi{)}^2))$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.18 (correction_jet_recurrence).

$$\forall (K:\mathbb{R}\to \mathbb{R}),\forall (B:\mathbb{R}\to \mathbb{R}),\forall (n:\mathbb{N}),(AnalyticAt\mathbb{R}K0)\to (AnalyticAt\mathbb{R}B0)\to (K0=0)\to (B0=0)\to iteratedDeriv(n+1)B0=correctionJetKB(n+1)-\sum i\in rangen,(n.\mathrm{choose}i:\mathbb{R})\cdot (iteratedDeriv(i+1)K0\cdot correctionJetKB(n-i)+iteratedDeriv(i+1)B0\cdot expJetK(n-i))$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.19 (partition_pos).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),(0<a)\to 0<partitionMa$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Definition 1.20 (laguerreMoment).

$$\forall (M:\mathbb{N}),\forall (r:\mathbb{N}),\forall (a:\mathbb{R}),laguerreMomentMra=((\int x,(\sum i:FinM,(xi{)}^r)\cdot laguerreWeightMax)/partitionMa)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreMoment (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Definition 1.21 (laguerreWeightedMeasure).

$$\forall (M:\mathbb{N}),\forall (Q:MvPolynomial(FinM)\mathbb{R}),laguerreWeightedMeasureMQ=((\mathrm{ENNReal}.\mathrm{ofReal}(partitionMM){)}^{-1}\cdot \mathrm{volume}.\mathrm{withDensity}(funx\mapsto \mathrm{ENNReal}.\mathrm{ofReal}(laguerreWeightMMx\cdot evalxQ)))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeightedMeasure (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Theorem 1.22 (singleWPoly_nonneg).

$$\forall (M:\mathbb{N}),\forall (x:FinM\to \mathbb{R}),0\le evalx(\mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}(funi:FinM\mapsto ((Xi{)}^2:MvPolynomial(FinM)\mathbb{R})))$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Definition 1.23 (laguerreH).

$$\forall (M:\mathbb{N}),laguerreHM=(mgf((funx:FinM\to \mathbb{R}\mapsto \mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}x))(laguerreWeightedMeasureM1))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreH (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Definition 1.24 (laguerreHw).

$$\forall (M:\mathbb{N}),laguerreHwM=(mgf((funx:FinM\to \mathbb{R}\mapsto \mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}x))(laguerreWeightedMeasureM(\mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}(funi:FinM\mapsto ((Xi{)}^2:MvPolynomial(FinM)\mathbb{R})))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreHw (✓ std3).

Source. Repository-derived.

Commentary.

The displayed definition is used in the moment and density expansions.

Theorem 1.25 (cumulant_expansion_of_moments).

$$\forall (m:\mathbb{N}\to \mathbb{R}\to \mathbb{R}),\forall (k:\mathbb{N}\to \mathbb{R}\to \mathbb{R}),\forall (a:\mathbb{N}\to \mathbb{R}),\forall (b:\mathbb{N}\to \mathbb{R}),\forall (c:\mathbb{N}\to \mathbb{R}),\forall (d:\mathbb{N}\to \mathbb{R}),(\forall r,FirstOrder(mr)(ar)(br))\to (\forall \gamma :\mathbb{R},0<\gamma \to \forall n:\mathbb{N},k(n+1)\gamma =m(n+1)\gamma -\sum i\in rangen,(n.\mathrm{choose}i:\mathbb{R})\cdot k(i+1)\gamma \cdot m(n-i)\gamma )\to (\forall n:\mathbb{N},c(n+1)=a(n+1)-\sum i\in rangen,(n.\mathrm{choose}i:\mathbb{R})\cdot c(i+1)\cdot a(n-i))\to (\forall n:\mathbb{N},d(n+1)=b(n+1)-\sum i\in rangen,(n.\mathrm{choose}i:\mathbb{R})\cdot (c(i+1)\cdot b(n-i)+d(i+1)\cdot a(n-i)))\to \forall r:\mathbb{N},1\le r\to FirstOrder(kr)(cr)(dr)$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.26 (laguerreWeighted_mgf_derivative).

$$\forall (M:\mathbb{N}),\forall (Q:MvPolynomial(FinM)\mathbb{R}),\forall (r:\mathbb{N}),(1\le M)\to (\forall x,0\le evalxQ)\to iteratedDerivr(mgf((funx:FinM\to \mathbb{R}\mapsto \mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}x))(laguerreWeightedMeasureMQ))0=(\int x,laguerreWeightMMx\cdot evalxQ\cdot (\mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}x{)}^r)/partitionMM$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.27 (laguerre_p1).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),(0<a)\to laguerreMomentM1a=(M:\mathbb{R}{)}^2/a$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.28 (laguerreH_near).

$$\forall (M:\mathbb{N}),(1\le M)\to laguerreHM{=}^f[nhds0](funt\mapsto \mathrm{Real}.\exp (gammaCGF((M:\mathbb{R}{)}^2)t))$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.29 (laguerreH_iterated).

$$\forall (M:\mathbb{N}),\forall (r:\mathbb{N}),(1\le M)\to (\int x,laguerreWeightMMx\cdot (\mathrm{Finset}.\mathrm{expect}\mathrm{Finset}.\mathrm{univ}x{)}^r)/partitionMM=expJet(gammaCGF((M:\mathbb{R}{)}^2))r$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.30 (laguerreHw_near).

$$\forall (M:\mathbb{N}),(1\le M)\to laguerreHwM{=}^f[nhds0](funt\mapsto 2\cdot \mathrm{Real}.\exp (gammaCGF((M:\mathbb{R}{)}^2)t)\cdot (inverseSlope((M:\mathbb{R}{)}^2)t{)}^2)$$

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

Source. Repository-derived.

Commentary.

The displayed identity or estimate is used in the moment and density expansions.

Theorem 1.31 (derivation_product_eigen).

$$\forall (M:(\mathbb{N})),((\forall (\sigma :(Type\ast )),((([DecidableEq\sigma ])\to ((\forall (D:(Derivation\mathbb{R}(MvPolynomial(FinM)\mathbb{R})(MvPolynomial(FinM)\mathbb{R}))),((\forall (s:(Finset\sigma )),((\forall (f:((\sigma )\to (MvPolynomial(FinM)\mathbb{R}))),((\forall (g:((\sigma )\to (MvPolynomial(FinM)\mathbb{R}))),((((\forall i\in s,(D(fi)=gi\cdot fi)))\to ((D(\prod i\in s,fi)=(\sum i\in s,gi)\cdot \prod i\in s,fi))))))))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.32 (orthant_measure).

$$\forall (M:(\mathbb{N})),(((volume:(Measure((FinM)\to (\mathbb{R})))).restrict((\mathrm{Set}.\mathrm{Ici}(0:((FinM)\to (\mathbb{R})))))=orthantMeasureM))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.33 (polynomial_exp_integrable_single).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (P:(MvPolynomial(FinM)\mathbb{R})),((Integrable(funx\mapsto (\mathrm{Real}.\exp (-a\cdot \sum i,xi)\cdot \mathrm{MvPolynomial}.\mathrm{eval}xP))(orthantMeasureM)))))))))$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.34 (polyIntegral).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((\forall (P:(MvPolynomial(FinM)\mathbb{R})),((polyIntegralaP=(\int x,\mathrm{Real}.\exp (-a\cdot \sum i,xi)\cdot \mathrm{MvPolynomial}.\mathrm{eval}xPdorthantMeasureM)))))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.polyIntegral (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.35 (polyIntegral_add).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (P:(MvPolynomial(FinM)\mathbb{R})),((\forall (Q:(MvPolynomial(FinM)\mathbb{R})),((polyIntegrala(P+Q)=polyIntegralaP+polyIntegralaQ))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.36 (polyIntegral_sum).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (\sigma :(Type\ast )),((\forall (s:(Finset\sigma )),((\forall (P:((\sigma )\to (MvPolynomial(FinM)\mathbb{R}))),((polyIntegrala(\sum i\in s,Pi)=\sum i\in s,polyIntegrala(Pi)))))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.37 (polyIntegral_X_sq).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (i:(FinM)),((\forall (P:(MvPolynomial(FinM)\mathbb{R})),((a\cdot polyIntegrala(((Xi){)}^2\cdot P)=2\cdot polyIntegrala(Xi\cdot P)+polyIntegrala(((Xi){)}^2\cdot \mathrm{MvPolynomial}.\mathrm{pderiv}iP)))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.38 (laguerre_p2).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((laguerreMomentM2a=2\cdot ((M:(\mathbb{R})){)}^3/(a{)}^2))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerre_p2 (✓ 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/StrongAbsorption/LaguerreMoments.congr_eventually
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.correctionCGF_analytic
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.correctionJet
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.correction_jet_recurrence
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.cumulant_expansion_of_moments
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.deltaPoly
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.deltaPoly_eval
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.deltaSq
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.deltaSq_nonneg
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.derivation_product_eigen
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.expJet
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.exp_deriv_near
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.exp_jet_recurrence
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.gammaCGF_analytic
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreH
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreH_iterated
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreH_near
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreHw
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreHw_near
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreMoment
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerrePolynomial_integrable
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeight
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeight_integrable
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeight_nonneg
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeightedMeasure
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerreWeighted_mgf_derivative
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerre_p1
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.laguerre_p2
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.orthant_measure
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.partition
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.partition_pos
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.polyIntegral
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.polyIntegral_X_sq
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.polyIntegral_add
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.polyIntegral_sum
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.polynomial_exp_integrable_single
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.singleWPoly_eval
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments.singleWPoly_nonneg
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/Foundations