Linear Margin and Typical Distance Density

Abstract

Diagonal listings satisfy the corrected linear-margin bound and concentrate at the typical distance density.

Theorem 1.1 (Linear margins concentrate at the nonzero-choice density).

$$\begin{array}{c}\forall Y:\mathrm{Type},f:Y\to Y,alpha\in \mathbb{R},\\ (\mathrm{Fintype}\left(Y\right)\wedge 2\le \mathrm{card}\left(Y\right)\wedge 0<alpha\wedge alpha<\frac{\mathrm{card}\left(Y\right)-1}{\mathrm{card}\left(Y\right)})\Rightarrow \\ (\forall A:\mathrm{Type},(\mathrm{Fintype}\left(A\right)\wedge 2\le \mathrm{card}\left(A\right)\wedge \frac{alpha\cdot \mathrm{card}\left(A\right)}{\mathrm{card}\left(A\right)-1}<\frac{\mathrm{card}\left(Y\right)-1}{\mathrm{card}\left(Y\right)})\Rightarrow \mathrm{marginFailureProbability}\left(f,alpha\right)\le \mathrm{linearMarginBound}\left(\mathrm{card}\left(Y\right),alpha,\mathrm{card}\left(A\right)\right))\wedge \\ (\underset{A\to \infty }{\lim }\mathrm{linearMarginBound}\left(\mathrm{card}\left(Y\right),alpha,A\right)=0)\wedge \\ (\underset{A\to \infty }{\lim }\mathrm{marginFailureProbability}\left(f,alpha\right)=0)\wedge \\ (\forall beta\in \mathbb{R},(\frac{\mathrm{card}\left(Y\right)-1}{\mathrm{card}\left(Y\right)}<beta\wedge beta<1)\Rightarrow \underset{A\to \infty }{\lim }\mathrm{typicalDensityFailureProbability}\left(f,alpha,beta\right)=0).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Probability/LinearMarginConcentration.linear_margin_concentration (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite value type Y of cardinality at least two, a self-map f, and a lower density alpha strictly between zero and (card(Y)-1)/card(Y), the first conjunct gives the corrected finite KL-Chernoff bound for every finite address type satisfying the displayed threshold restriction.

The second conjunct states that the corrected bound tends to zero. The third states that the actual probability of any row missing the linear margin also tends to zero, which is the asymptotically almost-sure linear escape clause. The fourth quantifies over every upper density between the typical density and one and states two-sided concentration of the minimum-distance density.

The proof directly combines the four frozen diagonal-margin theorems. It introduces no replacement probability, distance, divergence, or carrier. The displayed probability names abbreviate the finite uniform cardinality ratios written explicitly in the Lean statement.

References

• Truth anchor: D5/S0/Diagonal/Probability/LinearMarginConcentration.linear_margin_concentration
• Dependency: D5/S0/Diagonal/TypicalDensity