Density

Abstract

Density 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 (crossProduct).

$$\forall (M:\mathbb{N}),\forall (\epsilon :\mathbb{R}),\forall (x:FinM\to \mathbb{R}),\forall (y:FinM\to \mathbb{R}),crossProductM\epsilon xy=(\prod i,\prod j,(1+\epsilon \cdot (xi-yj)))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.crossProduct (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.2 (tailSet).

$$\forall (M:\mathbb{N}),\forall (\gamma :\mathbb{R}),tailSetM\gamma =(\{p|\exists j,\gamma <p.2j\})$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.tailSet (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.3 (linearDensityPoly).

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

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.linearDensityPoly (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (measurableSet_tailSet).

$$\forall (M:\mathbb{N}),\forall (\gamma :\mathbb{R}),MeasurableSet(tailSetM\gamma )$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.5 (linearDensityPoly_eval).

$$\forall (M:\mathbb{N}),\forall (p:(FinM\to \mathbb{R})\times (FinM\to \mathbb{R})),eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(linearDensityPolyM)=(M:\mathbb{R})\cdot ((\sum i,p.1i)-(\sum j,p.2j))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.6 (FirstOrder.affine).

$$\forall (a:\mathbb{R}),\forall (b:\mathbb{R}),FirstOrder(fun\gamma \mapsto a+b\cdot {\gamma }^{-1})ab$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.7 (baseWeight).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),\forall (p:(FinM\to \mathbb{R})\times (FinM\to \mathbb{R})),baseWeightMap=(laguerreWeightMap.1\cdot laguerreWeightMap.2)$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.baseWeight (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.8 (baseWeight_mass).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),(\int p,baseWeightMap)=(partitionMa{)}^2$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.9 (linearDensityIntegral_zero).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),(\int p,baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(linearDensityPolyM))=0$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.10 (basePolynomial_integrable).

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

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

Source. Repository-derived.

Commentary.

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

Theorem 1.11 (weight_scaled_cutoff).

$$\forall (M:\mathbb{N}),\forall (\gamma :\mathbb{R}),\forall (p:(FinM\to \mathbb{R})\times (FinM\to \mathbb{R})),(0<\gamma )\to weightM\gamma p={\gamma }^{M^2}\cdot (tailSetM\gamma {)}^c.indicator(funp\mapsto baseWeightMMp\cdot crossProductM{\gamma }^{-1}p.1p.2)p$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.12 (crossIntegrand_integrable).

$$\forall (M:\mathbb{N}),\forall (a:\mathbb{R}),\forall (\epsilon :\mathbb{R}),\forall (P:MvPolynomial(Sum(FinM)(FinM))\mathbb{R}),(0<a)\to Integrable(funp\mapsto baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P\cdot crossProductM\epsilon p.1p.2)$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.13 (law_polynomial_firstOrder).

$$\forall (M:\mathbb{N}),\forall (P:MvPolynomial(Sum(FinM)(FinM))\mathbb{R}),(1\le M)\to FirstOrder(fun\gamma \mapsto \int p,eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)PdlawM\gamma )((\int p,baseWeightMMp\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P)/(partitionMM{)}^2)((\int p,baseWeightMMp\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(P\cdot linearDensityPolyM))/(partitionMM{)}^2)$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.14 (crossProduct_firstOrder).

$$\forall (M:(\mathbb{N})),((\forall (x:((FinM)\to (\mathbb{R}))),((\forall (y:((FinM)\to (\mathbb{R}))),(((\sum p:FinM\times FinM,(xp.1-yp.2))=(M:(\mathbb{R}))\cdot ((\sum i,xi)-(\sum j,yj))))))))$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.15 (jointSum).

$$\forall (M:(\mathbb{N})),((\forall (p:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))),((jointSumMp=((\sum i,p.1i)+(\sum j,p.2j))))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.jointSum (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.16 (crossProduct_abs_bound).

$$\forall (M:(\mathbb{N})),((\forall (\epsilon :(\mathbb{R})),((((0\le \epsilon ))\to ((((\epsilon \le 1))\to ((\forall (x:((FinM)\to (\mathbb{R}))),((\forall (y:((FinM)\to (\mathbb{R}))),((((\forall i,(0\le xi)))\to ((((\forall j,(0\le yj)))\to ((|crossProductM\epsilon xy|\le ((1+(\sum i,xi)+(\sum j,yj)){)}^{(M{)}^2}))))))))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.17 (budgetPoly).

$$\forall (M:(\mathbb{N})),((budgetPolyM=(((1+(\mathrm{MvPolynomial}.\mathrm{psum}(Sum(FinM)(FinM))\mathbb{R}1)){)}^{(M{)}^2})))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.budgetPoly (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.18 (budgetPoly_eval).

$$\forall (M:(\mathbb{N})),((\forall (p:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))),((eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(budgetPolyM)=((1+jointSumMp){)}^{(M{)}^2}))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.19 (baseWeight_nonneg).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((\forall (p:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))),((0\le baseWeightMap))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.20 (budgetPoly_nonneg).

$$\forall (M:(\mathbb{N})),((\forall (p:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))),((((p\in (\mathrm{Set}.\mathrm{Ici}(0:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))))))\to ((0\le eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(budgetPolyM)))))))$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.21 (crossIntegral).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((\forall (\epsilon :(\mathbb{R})),((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((crossIntegralMa\epsilon P=(\int p,baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P\cdot crossProductM\epsilon p.1p.2)))))))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.crossIntegral (✓ std3).

Source. Repository-derived.

Commentary.

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

Definition 1.22 (cutoffIntegral).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((\forall (\gamma :(\mathbb{R})),((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((cutoffIntegralMa\gamma P=(\int p,((tailSetM\gamma ){)}^c.indicator(funp\mapsto (baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P\cdot crossProductM(\gamma {)}^{-1}p.1p.2))p)))))))))$$

Formalization. D5/S3/Quantum/Transport/StrongAbsorption/Density.cutoffIntegral (✓ std3).

Source. Repository-derived.

Commentary.

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

Theorem 1.23 (baseWeight_eq_zero_off_orthant).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((\forall (p:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))),((((p\neg \in (\mathrm{Set}.\mathrm{Ici}(0:(((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))))))\to ((baseWeightMap=0))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.24 (tail_family_exponential_bound).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (\gamma :(\mathbb{R})),((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((\forall (f:((((FinM)\to (\mathbb{R}))\times ((FinM)\to (\mathbb{R})))\to (\mathbb{R}))),((((\forall p,(|fp|\le baseWeightMap\cdot |eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P|)))\to ((|\int pintailSetM\gamma ,fp|\le \mathrm{Real}.\exp (-(a\cdot \gamma )/2)\cdot \int p,baseWeightM(a/2)p\cdot |eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P|))))))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.25 (law_polynomial_ratio).

$$\forall (M:(\mathbb{N})),((((1\le M))\to ((\forall (\gamma :(\mathbb{R})),((((0<\gamma ))\to ((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),(((\int p,eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)PdlawM\gamma )=cutoffIntegralM(M:(\mathbb{R}))\gamma P/cutoffIntegralM(M:(\mathbb{R}))\gamma 1))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.26 (cutoffIntegral_eq_sub).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (\gamma :(\mathbb{R})),((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((cutoffIntegralMa\gamma P=crossIntegralMa(\gamma {)}^{-1}P-\int pintailSetM\gamma ,baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P\cdot crossProductM(\gamma {)}^{-1}p.1p.2))))))))))$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.27 (cutoffIntegral_firstOrder).

$$\forall (M:(\mathbb{N})),((\forall (a:(\mathbb{R})),((((0<a))\to ((\forall (P:(MvPolynomial(Sum(FinM)(FinM))\mathbb{R})),((FirstOrder(fun\gamma \mapsto (cutoffIntegralMa\gamma P))(\int p,baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)P)(\int p,baseWeightMap\cdot eval(\mathrm{Sum}.\mathrm{elim}p.1p.2)(P\cdot linearDensityPolyM))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Transport/StrongAbsorption/Density.cutoffIntegral_firstOrder (✓ 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/Density.affine
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.basePolynomial_integrable
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.baseWeight
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.baseWeight_eq_zero_off_orthant
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.baseWeight_mass
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.baseWeight_nonneg
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.budgetPoly
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.budgetPoly_eval
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.budgetPoly_nonneg
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.crossIntegral
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.crossIntegrand_integrable
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.crossProduct
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.crossProduct_abs_bound
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.crossProduct_firstOrder
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.cutoffIntegral
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.cutoffIntegral_eq_sub
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.cutoffIntegral_firstOrder
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.jointSum
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.law_polynomial_firstOrder
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.law_polynomial_ratio
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.linearDensityIntegral_zero
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.linearDensityPoly
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.linearDensityPoly_eval
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.measurableSet_tailSet
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.tailSet
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.tail_family_exponential_bound
• Truth anchor: D5/S3/Quantum/Transport/StrongAbsorption/Density.weight_scaled_cutoff
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/Foundations
• Dependency: D5/S3/Quantum/Transport/StrongAbsorption/LaguerreMoments