lemmaroutineinferred_dep

Wedge law has tiny atoms and small information

Lemma·inc:entropy·§2.5 The information carried by a wedge

Statement (paper)

For the wedge law , let dmin⁡,Q=min⁡q∈Qd(q)d_{\min,Q}=\min_{q\in Q}d(q). If p≠rp\ne r, then P(p,r)≤2∣E∣dmin⁡,Q=t−2−3a+o(a). \Prob(p,r)\le\frac{2}{|E|d_{\min,Q}} =t^{-2-3a+o(a)}. The diagonal probability is P(p=r)=∣Q∣∣E∣=t−a+o(a)=o(1). \Prob(p=r)=\frac{|Q|}{|E|}=t^{-a+o(a)}=o(1). The mutual information of the point endpoints satisfies D:=DKL⁡(L(p,r) ∥ μ⊗μ)=o(log⁡t). D:=\KL\bigl(\mathcal L(p,r)\,\Vert\,\mu\otimes\mu\bigr) =o(\log t).

In plain English

For the wedge law on pairs of point endpoints (p,r)(p,r), every off-diagonal atom has probability at most 2/(∣E∣dmin⁡,Q)=t−2−3a+o(a)2/(|E|d_{\min,Q})=t^{-2-3a+o(a)}. The diagonal mass P(p=r)=∣Q∣/∣E∣=t−a+o(a)\Prob(p=r)=|Q|/|E|=t^{-a+o(a)} is o(1)o(1), and the mutual information D=DKL⁡(L(p,r)∥μ⊗μ)D=\KL(\mathcal L(p,r)\Vert\mu\otimes\mu) is o(log⁡t)o(\log t).

Why it's here

This turns the degree and size bounds of the incidence piece into quantitative control of the wedge law: atoms are very small and collisions are rare. The key point is that the point endpoints are nearly independent, with information cost o(log⁡t)o(\log t), which is what the later entropy and history arguments need, including the exclusion of bounded SS.
Classified routine:
These bounds follow from the degree and size estimates of the incidence piece by direct counting, with the atom bound coming from dividing by the minimum degree. The KL bound is a standard entropy calculation from the atom sizes and the size of the support.

Uses

propIncidence piece with degree and expansion control

Used by

propTotal variation S cannot stay boundedclaimQuantized acceptance tests with a history predictor

Sources

PaperOpen
Section
§2.5 The information carried by a wedge
Page
—
Label
inc:entropy
Line
sections/01-incidence.tex:493
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: 01-incidence.tex:518 proves the atom estimate "by --", which are the conclusions of Proposition inc:piece.