10.1. 5. The pricing🔗

Pricing. At the parameters of Lemma M5.4, given the setup, the ledger, the race and its cap, and the mismatch

payment with PC(23/250,7/60), the inequality T(p)\le(13999/2000)\,\tau(p) holds for every law

p whose support is connected.

The components named in the statement are proved on other pages; this page supplies no new proof of the pair charge, the ledger, the race, the cap or the setup. The calibrated family, h, d and j(a) are those of section 1 of the race page, equation (R1), and of (D3); d\ge0, and the conditional entropies in h are evaluated at each fixed seed and then averaged, so no unconditional label entropy is used. Combining a ledger with a race in this way is the method of pull request #6 by Jeremy Gillen to DLorell/stochtodet: powered-reference race coding with a coordinate ledger (see the upstream page).

Theorem10.1.1

group

Statement uses 5

Statement dependency previews

Preview

Theorem 1.1.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1XL∃∀N

Tagspaper proof

Lemma M5.1 (generic assembly). For every finite nonempty X,Y, every law p whose support is connected, and every real a,u,\beta,\gamma with a>1, u\ge0, \beta\ge0, \gamma>0, suppose the setup (Lemma S1.4 of the setup page) supplies an attained latent with M+B=\tau(p), positive priors, posterior rows positive on the support, and distinct components that are positive contacts of one feasible kernel on the support; the race uses the positive posterior rows, and the payment uses the priors and the contacts. Suppose the ledger (Lemma L4.1 of the ledger page), the race (Lemma R11 of the race page) and the mismatch payment (Lemma P5.5 of the payment page) supply a calibrated family satisfying

T(p)\le M-\frac B2+\frac{3h}{2},\qquad h\le aB+2j(a)d,\qquad \gamma d\le(1+2\beta)M+\beta B,\qquad M\ge0,\quad B\ge0,\quad d\ge0. \qquad \text{(M5.C)}

Assume a cap gives u>j(a), and that the pair charge used by the payment is PC(\beta,\gamma). Then

T(p)\le C\,\tau(p),\qquad C=\max\left\{1+\frac{3u(1+2\beta)}{\gamma}, \frac{3a-1}{2}+\frac{3u\beta}{\gamma}\right\}. \qquad \text{(M5.D)}

Proof for Theorem 10.1.1

uses 0

Substitute the race and cap into the ledger, multiply the mismatch payment by the nonnegative price factor, and dominate both budgets by the maximum coefficient. See the page section.

Lean: no generic theorem; the calculation (M5.E) is carried out inside NaturalLatents.General.T_le_of_connected at its fixed parameters, by linarith from T_le_ledger, the race bound of exists_race, the cap, mismatch_payment and the sign facts. The affinity hypothesis of mismatch_payment is discharged by affinity_bound applied to contact_moments for each pair of distinct components of the setup latent, and its replica hypothesis by replica_budget.

Remark M5.2 (the cap evaluation at a = 211/45). The cap premise is, for every a>1, j(a)<F(a), with all three terms of the cap F of Lemma K13 on the cap page shown:

\begin{aligned} F(a)&=\frac{533}{648a}+\frac{241}{600a^2} +\frac{6503}{24000a^2(a-1)},\\ F(211/45)&=\frac{2665}{15192}+\frac{6507}{356168} +\frac{1580229}{472991104} =\frac{838748045}{4256919936},\\ \frac{3941}{20000}-F(211/45)&=\frac{48767743}{2660574960000}>0 . \end{aligned} \qquad \text{(M5.F)}

Thus j(211/45)<3941/20000. This is point arithmetic for the universal cap, not a new cap proof; the termwise substitution is displayed in section 5 of the cap page.

Lean: racePrice_lt_capC3b at 211/45 followed by norm_num [gammaPriceCap] inside T_le_of_connected, the step hj.

Theorem10.1.2

group

Statement uses 9

Statement dependency previews

Preview

Theorem 1.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma M5.4 (the specialization). For every finite law with connected support, satisfying the setup, ledger, race, payment and cap inputs, the pair charge PC(23/250,7/60) gives

\begin{aligned} a&=\frac{211}{45}>1,\quad u=\frac{3941}{20000}>0,\quad \beta=\frac{23}{250}\ge0,\quad\gamma=\frac7{60}>0,\quad \frac{3u}{\gamma}=\frac{5067}{1000},\\ C_M&=1+\frac{5067}{1000}\cdot\frac{148}{125} =\frac{218729}{31250},\qquad C_B=\frac{98}{15}+\frac{5067}{1000}\cdot\frac{23}{250} =\frac{5249623}{750000},\\ C_B-C_M&=\frac{127}{750000}>0,\qquad \frac{13999}{2000}-C_B=\frac1{375000}>0,\qquad 7-\frac{13999}{2000}=\frac1{2000}>0,\\ T(p)&\le\frac{13999}{2000}\,\tau(p). \end{aligned} \qquad \text{(M5.H)}

Lean code for Theorem10.1.2●1 theorem

theoremdefined in NaturalLatents/General/Pricing.lean

complete

theorem NaturalLatents.General.T_le_of_connected {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (hconn : stoch_to_det.IsConnected (stoch_to_det.support p)) :
  NaturalLatents.General.TNat p ≤
    13999 / 2000 * NaturalLatents.General.tauNat p

theorem NaturalLatents.General.T_le_of_connected
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (hconn :
    stoch_to_det.IsConnected
      (stoch_to_det.support p)) :
  NaturalLatents.General.TNat p ≤
    13999 / 2000 *
      NaturalLatents.General.tauNat p

`TNat p ≤ (13999/2000) * tauNat p`, in nats, for a law with connected support.

Proof for Theorem 10.1.2

uses 0

Lean proves: T(p)\le(13999/2000)\tau(p) in nats for every finite probability law with connected support.

Evaluate the cap at the selected exponent and compute both pricing coefficients exactly, then use their positive margins below the stated constant. See the page section.

Lean: NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean) is Lemma M5.4, in nats and for a law with connected support only; it states TNat p ≤ (13999/2000 : ℝ) * tauNat p. Its proof consists of:

exists_race at 211/45, and hj : gammaPrice (211/45) < 3941/20000 from racePrice_lt_capC3b and norm_num [gammaPriceCap];
the race bound hh with 211/45 and 3941/20000;
mismatch_payment at (23/250) (7/60) with pairCharge_C;
hM : 0 ≤ mediation D.L and hB : 0 ≤ redundancy D.L, from stoch_to_det.condMI_nonneg through nats_nonneg_iff, both passed to the final linarith, since 13999/2000 exceeds both C_M and C_B (the proof of Lemma M5.4).

The constant NaturalLatents.c := 13999 / 2000 and NaturalLatents.T_le_mul_tau are in NaturalLatents/Main.lean, and Verify.lean pins T_le_mul_tau with an example at 13999 / 2000.

The extension to every finite law is not in Pricing.lean: NaturalLatents.T_le_c_mul_tau (NaturalLatents/Main.lean) converts the bound of T_le_of_connected to bits by bits_of_nats (NaturalLatents/General/Nats.lean) and applies extension_of_connected, stated in bits, with c_nonneg.