lemmaroutineinferred_dep

Point profiles approximate wedge differences

Lemma·ext:profiles·§7.2 Point profiles and a common height band

Statement (paper)

For an ordinary wedge (p,q,r)(p,q,r), there are nonnegative random variables E1,E2E_1,E_2, with EE1+EE2=o(S)\E E_1+\E E_2=o(S), such that ∥(npq−nrq)−(ap−ar)∥1≤E1,∥npq−nrq∥1≥Hp∗+Hr∗−E2.\begin{aligned} \norm{(n_{pq}-n_{rq})-(a_p-a_r)}_1&\le E_1, \\ \norm{n_{pq}-n_{rq}}_1&\ge H_p^*+H_r^*-E_2. \end{aligned} Here npq(v)=−log⁡∣zp−zq∣vn_{pq}(v)=-\log\abs{z_p-z_q}_v.

In plain English

For an ordinary wedge (p,q,r)(p,q,r), the profile difference npq−nrqn_{pq}-n_{rq} (with npq(v)=−log⁡∣zp−zq∣vn_{pq}(v)=-\log|z_p-z_q|_v) is within ℓ1\ell^1 distance E1E_1 of ap−ara_p-a_r, and its ℓ1\ell^1 norm is at least Hp∗+Hr∗−E2H_p^*+H_r^*-E_2, where E1,E2≥0E_1,E_2\ge 0 are random variables with EE1+EE2=o(S)\E E_1+\E E_2=o(S).

Why it's here

This lemma links the actual local profile differences at a wedge to the point data ap−ara_p-a_r and to the rare-exception heights Hp∗,Hr∗H_p^*,H_r^*, with total error o(S)o(S) on average. It builds on the rare-exception moment and joint-exception bounds of Lemma 5.2 and on the negligible common variation of Proposition 6.3. Later steps, such as the common height band and the organized pair graph, can then use the point profiles in place of the wedge differences.
Classified routine:
Follows by bookkeeping from the rare-exception moment and joint bounds (Lemma 5.2) and the negligible common variation (Proposition 6.3): it decomposes the wedge profile difference into point data plus error terms whose expectations are o(S).

Uses

lemRare exceptions: comparison, first moments, joint boundspropCommon variation is negligible

Used by

lemCommon height band of accurate wedgespropOrganized pair graph with height-controlled ratios

Sources

PaperOpen
Section
§7.2 Point profiles and a common height band
Page
—
Label
ext:profiles
Line
sections/06-extraction.tex:199
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: 06-extraction.tex:231: "the first term averages to C_Q=o(S)", which is of Proposition com:variation.