2.2. 1. Contact moments and the feasible Hessian🔗

Fix finite nonempty alphabets X,Y, a nonempty support S\subseteq X\times Y, and a kernel w:S\to(0,\infty), extended by zero outside S. Remove unused rows and columns, so every symbol of X and Y occurs in S. Feasibility means that, for every pair of probability vectors u on X and v on Y,

\sum_{(x,y)\in S}w(x,y)u_x^{2/3}v_y^{2/3}\leq1. \qquad \text{(C1.1)}

A positive contact is a probability law P positive at every cell of S, zero outside S, and satisfying

P(x,y)=w(x,y)P_X(x)^{2/3}P_Y(y)^{2/3} \quad((x,y)\in S). \qquad \text{(C1.2)}

Thus all used marginal probabilities are positive. Neither full rectangular support nor connectedness is assumed. For two such contacts P,R, define

\begin{aligned} f(x)&=\left(\frac{R_X(x)}{P_X(x)}\right)^{1/3}, &g(y)&=\left(\frac{R_Y(y)}{P_Y(y)}\right)^{1/3},\\ U&=f-1,&V&=g-1,\\ A_0&=1-E_Pf,&B_0&=1-E_Pg,\\ s&=A_0+B_0=2-E_Pf-E_Pg, &J&=E_P[U^2V^2]. \end{aligned} \qquad \text{(C1.3)}

All expectations in this section are under P, including expectations of a field depending on only one coordinate. Some letters in this section are local: f,g are the fields (C1.3), not maps or codes; u,v in (C1.1) are probability vectors, not the price bound u of the cap page; the fields A,B and the normalizers a,b of Lemma C1.3 are not the budget B, the race exponent a or the quadratic b of (A2.1); and L(t), R(t) in the proof of Lemma C1.4 are not a latent or a contact.

Lean: a pair of distinct positive contacts of one feasible kernel is CommonSupportPair S w P R. Feasibility (C1.1) is stoch_to_det.Feasible and the contact equation (C1.2), with P a probability law zero outside S, is stoch_to_det.IsContact (NaturalLatents/Upstream/Duality.lean), both used directly, and positivity on S is PositiveOn (NaturalLatents/General/Definitions.lean). Feasible also records w>0 on S. Lean does not remove unused rows and columns: Feasible quantifies over probability vectors on the full alphabets, and the conditional statements are restricted to the used symbols xSupport S and ySupport S. Lean leaves w outside S unrestricted, because those values never enter the conditions. On unused marginal symbols, its totalized division gives f=g=0 and hence U=V=-1; these symbols contribute zero to every expectation, and conditional identities are asserted only on used symbols. The fields (C1.3) are rootRatioX, rootRatioY, defectX, defectY, separation and quarticMoment, with E_P written expect P, all in NaturalLatents/General/Definitions.lean, and U,V are the upstream secants stoch_to_det.contactSecantX and stoch_to_det.contactSecantY (NaturalLatents/Upstream/Floor.lean), with rootRatioX defined as contactSecantX + 1.

Theorem2.2.1

Group: Contact moments and the feasible Hessian. (4)

Group member previews

Preview

Theorem 2.2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 6

Reverse dependency previews

Preview

Theorem 2.2.2

Loading preview

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

✓L∃∀N

Tagspartly kernel-verified

Lemma C1.1 (contact ratios and conditional moments). For every finite nonempty X,Y, every nonempty S\subseteq X\times Y with all rows and columns used, every feasible kernel w>0 on S, and every pair of positive contacts P,R of w, the fields in (C1.3) satisfy, at every cell of S and every used conditioning symbol respectively,

\frac RP=f^2g^2,\qquad E_P[g^2\mid X]=f,\qquad E_P[f^2\mid Y]=g,\qquad E_Pf^3=E_Pg^3=1,\qquad E_Pf^2=E_Pg,\quad E_Pg^2=E_Pf. \qquad \text{(C1.4)}

Lean code for Theorem2.2.1●7 theorems

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_ratio_mul {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R)
  (z : X × Y) :
  R z =
    P z * NaturalLatents.General.rootRatioX P R z.1 ^ 2 *
      NaturalLatents.General.rootRatioY P R z.2 ^ 2

theorem NaturalLatents.General.contact_ratio_mul
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R)
  (z : X × Y) :
  R z =
    P z *
        NaturalLatents.General.rootRatioX
            P R z.1 ^
          2 *
      NaturalLatents.General.rootRatioY P
          R z.2 ^
        2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_cond_rootRatioY_square {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) {x : X}
  (hx : x ∈ NaturalLatents.General.xSupport S) :
  (∑ y, P (x, y) * NaturalLatents.General.rootRatioY P R y ^ 2) /
      stoch_to_det.mX P x =
    NaturalLatents.General.rootRatioX P R x

theorem NaturalLatents.General.contact_cond_rootRatioY_square
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R)
  {x : X}
  (hx :
    x ∈
      NaturalLatents.General.xSupport S) :
  (∑ y,
        P (x, y) *
          NaturalLatents.General.rootRatioY
              P R y ^
            2) /
      stoch_to_det.mX P x =
    NaturalLatents.General.rootRatioX P R
      x

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_cond_rootRatioX_square {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) {y : Y}
  (hy : y ∈ NaturalLatents.General.ySupport S) :
  (∑ x, P (x, y) * NaturalLatents.General.rootRatioX P R x ^ 2) /
      stoch_to_det.mY P y =
    NaturalLatents.General.rootRatioY P R y

theorem NaturalLatents.General.contact_cond_rootRatioX_square
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R)
  {y : Y}
  (hy :
    y ∈
      NaturalLatents.General.ySupport S) :
  (∑ x,
        P (x, y) *
          NaturalLatents.General.rootRatioX
              P R x ^
            2) /
      stoch_to_det.mY P y =
    NaturalLatents.General.rootRatioY P R
      y

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_rootRatioX_cube {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  (NaturalLatents.General.expect P fun z =>
      NaturalLatents.General.rootRatioX P R z.1 ^ 3) =
    1

theorem NaturalLatents.General.contact_rootRatioX_cube
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  (NaturalLatents.General.expect P
      fun z =>
      NaturalLatents.General.rootRatioX P
          R z.1 ^
        3) =
    1

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_rootRatioY_cube {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  (NaturalLatents.General.expect P fun z =>
      NaturalLatents.General.rootRatioY P R z.2 ^ 3) =
    1

theorem NaturalLatents.General.contact_rootRatioY_cube
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  (NaturalLatents.General.expect P
      fun z =>
      NaturalLatents.General.rootRatioY P
          R z.2 ^
        3) =
    1

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_rootRatioX_square {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  (NaturalLatents.General.expect P fun z =>
      NaturalLatents.General.rootRatioX P R z.1 ^ 2) =
    NaturalLatents.General.expect P fun z =>
      NaturalLatents.General.rootRatioY P R z.2

theorem NaturalLatents.General.contact_rootRatioX_square
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  (NaturalLatents.General.expect P
      fun z =>
      NaturalLatents.General.rootRatioX P
          R z.1 ^
        2) =
    NaturalLatents.General.expect P
      fun z =>
      NaturalLatents.General.rootRatioY P
        R z.2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_rootRatioY_square {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  (NaturalLatents.General.expect P fun z =>
      NaturalLatents.General.rootRatioY P R z.2 ^ 2) =
    NaturalLatents.General.expect P fun z =>
      NaturalLatents.General.rootRatioX P R z.1

theorem NaturalLatents.General.contact_rootRatioY_square
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  (NaturalLatents.General.expect P
      fun z =>
      NaturalLatents.General.rootRatioY P
          R z.2 ^
        2) =
    NaturalLatents.General.expect P
      fun z =>
      NaturalLatents.General.rootRatioX P
        R z.1

Proof for Theorem 2.2.1

uses 0

Lean proves: R=Pf^2g^2, the two conditional identities, the two cube moments and the two second-moment identities of (C1.4) for distinct positive contacts (CommonSupportPair).

Divide the contact equations and sum along rows and columns, using normalization and the conditional expectation tower rule. See the page section.

Lean: contact_ratio_mul (the ratio identity, stated as R=Pf^2g^2 at every cell), contact_cond_rootRatioY_square, contact_cond_rootRatioX_square, contact_rootRatioX_cube, contact_rootRatioY_cube, contact_rootRatioX_square and contact_rootRatioY_square, all NaturalLatents.General.* in NaturalLatents/General/Contact.lean. Their hypothesis is CommonSupportPair S w P R, which includes feasibility and P\ne R. The proof above uses neither feasibility nor distinctness; the stated lemma retains feasibility to match the common contact domain.

Theorem2.2.2

Group: Contact moments and the feasible Hessian. (4)

Group member previews

Preview

Theorem 2.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 5

Reverse dependency previews

Preview

Theorem 2.2.5

Loading preview

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

✓L∃∀N

Tagspartly kernel-verified

Lemma C1.2 (separation and the quartic moment list). For every finite nonempty X,Y, every nonempty common support S with all rows and columns used, every feasible w>0 on S, and every pair of positive contacts P,R, the quantities in (C1.3) satisfy

A_0,B_0\geq0,\qquad E_PU^2=2A_0-B_0,\qquad E_PV^2=2B_0-A_0,\qquad J=4E_P[UV]-s,\qquad s(P,R)=s(R,P). \qquad \text{(C1.9)}

If P\ne R, then 0<s<2. If P=R, then f=g=1 and s=J=0.

Lean code for Theorem2.2.2●5 theorems

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_energy_identities {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hP : stoch_to_det.IsContact S w P)
  (hR : stoch_to_det.IsContact S w R) (hPs : stoch_to_det.support P = S)
  (hRs : stoch_to_det.support R = S) :
  (NaturalLatents.General.expect P fun z =>
        stoch_to_det.contactSecantX P R z.1 ^ 2) =
      2 * NaturalLatents.General.defectX P R -
        NaturalLatents.General.defectY P R ∧
    (NaturalLatents.General.expect P fun z =>
          stoch_to_det.contactSecantY P R z.2 ^ 2) =
        2 * NaturalLatents.General.defectY P R -
          NaturalLatents.General.defectX P R ∧
      NaturalLatents.General.separation P R =
        (NaturalLatents.General.expect P fun z =>
            stoch_to_det.contactSecantX P R z.1 ^ 2) +
          NaturalLatents.General.expect P fun z =>
            stoch_to_det.contactSecantY P R z.2 ^ 2

theorem NaturalLatents.General.contact_energy_identities
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hP : stoch_to_det.IsContact S w P)
  (hR : stoch_to_det.IsContact S w R)
  (hPs : stoch_to_det.support P = S)
  (hRs : stoch_to_det.support R = S) :
  (NaturalLatents.General.expect P
        fun z =>
        stoch_to_det.contactSecantX P R
            z.1 ^
          2) =
      2 *
          NaturalLatents.General.defectX P
            R -
        NaturalLatents.General.defectY P
          R ∧
    (NaturalLatents.General.expect P
          fun z =>
          stoch_to_det.contactSecantY P R
              z.2 ^
            2) =
        2 *
            NaturalLatents.General.defectY
              P R -
          NaturalLatents.General.defectX P
            R ∧
      NaturalLatents.General.separation P
          R =
        (NaturalLatents.General.expect P
            fun z =>
            stoch_to_det.contactSecantX P
                R z.1 ^
              2) +
          NaturalLatents.General.expect P
            fun z =>
            stoch_to_det.contactSecantY P
                R z.2 ^
              2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_quartic_identity {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {P R : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P)
  (hR : stoch_to_det.IsPMF R)
  (hratio :
    ∀ (z : X × Y),
      R z =
        P z * NaturalLatents.General.rootRatioX P R z.1 ^ 2 *
          NaturalLatents.General.rootRatioY P R z.2 ^ 2)
  (hcond_g2 :
    ∀ (x : X),
      ∑ y, P (x, y) * NaturalLatents.General.rootRatioY P R y ^ 2 =
        stoch_to_det.mX P x * NaturalLatents.General.rootRatioX P R x)
  (hcond_f2 :
    ∀ (y : Y),
      ∑ x, P (x, y) * NaturalLatents.General.rootRatioX P R x ^ 2 =
        stoch_to_det.mY P y * NaturalLatents.General.rootRatioY P R y)
  (hf2 :
    (NaturalLatents.General.expect P fun z =>
        NaturalLatents.General.rootRatioX P R z.1 ^ 2) =
      NaturalLatents.General.expect P fun z =>
        NaturalLatents.General.rootRatioY P R z.2)
  (hg2 :
    (NaturalLatents.General.expect P fun z =>
        NaturalLatents.General.rootRatioY P R z.2 ^ 2) =
      NaturalLatents.General.expect P fun z =>
        NaturalLatents.General.rootRatioX P R z.1) :
  NaturalLatents.General.quarticMoment P R =
    (4 *
        NaturalLatents.General.expect P fun z =>
          stoch_to_det.contactSecantX P R z.1 *
            stoch_to_det.contactSecantY P R z.2) -
      NaturalLatents.General.separation P R

theorem NaturalLatents.General.contact_quartic_identity
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {P R : NaturalLatents.General.Law X Y}
  (hP : stoch_to_det.IsPMF P)
  (hR : stoch_to_det.IsPMF R)
  (hratio :
    ∀ (z : X × Y),
      R z =
        P z *
            NaturalLatents.General.rootRatioX
                P R z.1 ^
              2 *
          NaturalLatents.General.rootRatioY
              P R z.2 ^
            2)
  (hcond_g2 :
    ∀ (x : X),
      ∑ y,
          P (x, y) *
            NaturalLatents.General.rootRatioY
                P R y ^
              2 =
        stoch_to_det.mX P x *
          NaturalLatents.General.rootRatioX
            P R x)
  (hcond_f2 :
    ∀ (y : Y),
      ∑ x,
          P (x, y) *
            NaturalLatents.General.rootRatioX
                P R x ^
              2 =
        stoch_to_det.mY P y *
          NaturalLatents.General.rootRatioY
            P R y)
  (hf2 :
    (NaturalLatents.General.expect P
        fun z =>
        NaturalLatents.General.rootRatioX
            P R z.1 ^
          2) =
      NaturalLatents.General.expect P
        fun z =>
        NaturalLatents.General.rootRatioY
          P R z.2)
  (hg2 :
    (NaturalLatents.General.expect P
        fun z =>
        NaturalLatents.General.rootRatioY
            P R z.2 ^
          2) =
      NaturalLatents.General.expect P
        fun z =>
        NaturalLatents.General.rootRatioX
          P R z.1) :
  NaturalLatents.General.quarticMoment P
      R =
    (4 *
        NaturalLatents.General.expect P
          fun z =>
          stoch_to_det.contactSecantX P R
              z.1 *
            stoch_to_det.contactSecantY P
              R z.2) -
      NaturalLatents.General.separation P
        R

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_separation {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R)
  (hratio :
    ∀ (z : X × Y),
      R z =
        P z * NaturalLatents.General.rootRatioX P R z.1 ^ 2 *
          NaturalLatents.General.rootRatioY P R z.2 ^ 2)
  (he :
    NaturalLatents.General.separation P R =
      (NaturalLatents.General.expect P fun z =>
          stoch_to_det.contactSecantX P R z.1 ^ 2) +
        NaturalLatents.General.expect P fun z =>
          stoch_to_det.contactSecantY P R z.2 ^ 2) :
  0 < NaturalLatents.General.separation P R

theorem NaturalLatents.General.contact_separation
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R)
  (hratio :
    ∀ (z : X × Y),
      R z =
        P z *
            NaturalLatents.General.rootRatioX
                P R z.1 ^
              2 *
          NaturalLatents.General.rootRatioY
              P R z.2 ^
            2)
  (he :
    NaturalLatents.General.separation P
        R =
      (NaturalLatents.General.expect P
          fun z =>
          stoch_to_det.contactSecantX P R
              z.1 ^
            2) +
        NaturalLatents.General.expect P
          fun z =>
          stoch_to_det.contactSecantY P R
              z.2 ^
            2) :
  0 <
    NaturalLatents.General.separation P R

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_upper_separation {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {P R : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P)
  (hf : ∀ (x : X), 0 ≤ NaturalLatents.General.rootRatioX P R x)
  (hg : ∀ (y : Y), 0 ≤ NaturalLatents.General.rootRatioY P R y)
  (hfp :
    ∀ (z : X × Y),
      0 < P z → 0 < NaturalLatents.General.rootRatioX P R z.1)
  (hgp :
    ∀ (z : X × Y),
      0 < P z → 0 < NaturalLatents.General.rootRatioY P R z.2) :
  NaturalLatents.General.separation P R < 2

theorem NaturalLatents.General.contact_upper_separation
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {P R : NaturalLatents.General.Law X Y}
  (hP : stoch_to_det.IsPMF P)
  (hf :
    ∀ (x : X),
      0 ≤
        NaturalLatents.General.rootRatioX
          P R x)
  (hg :
    ∀ (y : Y),
      0 ≤
        NaturalLatents.General.rootRatioY
          P R y)
  (hfp :
    ∀ (z : X × Y),
      0 < P z →
        0 <
          NaturalLatents.General.rootRatioX
            P R z.1)
  (hgp :
    ∀ (z : X × Y),
      0 < P z →
        0 <
          NaturalLatents.General.rootRatioY
            P R z.2) :
  NaturalLatents.General.separation P R <
    2

theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.lean

complete

theorem NaturalLatents.General.pairCharge_separation_reverse {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  NaturalLatents.General.separation R P =
    NaturalLatents.General.separation P R

theorem NaturalLatents.General.pairCharge_separation_reverse
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  NaturalLatents.General.separation R P =
    NaturalLatents.General.separation P R

Proof for Theorem 2.2.2

uses 0

Lean proves: the energy and quartic identities of (C1.9), s<2, and, for distinct positive contacts, s>0 and s(P,R)=s(R,P).

Apply strict Jensen for separation, expand the quadratic and quartic moments, and change measure for reversal symmetry. See the page section.

Lean: contact_energy_identities (the two identities for E_PU^2 and E_PV^2, and their sum s), contact_quartic_identity, contact_separation (0<s) and contact_upper_separation (s<2) in NaturalLatents/General/Contact.lean, and pairCharge_separation_reverse (the symmetry) in NaturalLatents/General/PairCharge/MomentBounds.lean, all NaturalLatents.General.*.

These assume distinctness: the positive-separation lemma contact_separation, the symmetry pairCharge_separation_reverse and contact_moments. contact_separation derives 0<s from s=E_PU^2+E_PV^2 rather than from strict Jensen.

These do not assume distinctness: the energy and quartic identities and the upper bound s<2. contact_energy_identities assumes two contacts whose support is exactly S; contact_quartic_identity takes probability laws P,R together with the ratio identity and the conditional and second-moment identities of Lemma C1.1 as inputs; and contact_upper_separation takes a probability law P and nonnegativity of f,g with positivity wherever P is positive. Neither the energy nor the quartic lemma assumes feasibility. The equal-pair conclusions are not collected into a separate Lean statement, and A_0,B_0\ge0 is not stated separately, though it follows from the two energy identities.

Theorem2.2.3

Group: Contact moments and the feasible Hessian. (4)

Group member previews

Preview

Theorem 2.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma C1.3 (feasibility for nonnegative marginal fields). For every finite nonempty X,Y, every nonempty S\subseteq X\times Y with all rows and columns used, every feasible w>0 on S, every positive contact P of w, and every pair of fields A:X\to[0,\infty), B:Y\to[0,\infty),

E_P[A(X)^2B(Y)^2]\leq(E_PA^3)^{2/3}(E_PB^3)^{2/3}. \qquad \text{(C1.15)}

Lean code for Theorem2.2.3●2 theorems

theoremdefined in NaturalLatents/Upstream/Duality.lean

complete

theorem stoch_to_det.contact_hypercontractive.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {S : Finset (α × β)} {w : α × β → ℝ} (hw : stoch_to_det.Feasible S w)
  {q : α × β → ℝ} (hq : stoch_to_det.IsContact S w q) {f : α → ℝ}
  {g : β → ℝ} (hf : ∀ (x : α), 0 ≤ f x) (hg : ∀ (y : β), 0 ≤ g y) :
  ∑ z ∈ S, q z * f z.1 * g z.2 ≤
    (∑ x, stoch_to_det.mX q x * f x ^ (3 / 2)) ^ (2 / 3) *
      (∑ y, stoch_to_det.mY q y * g y ^ (3 / 2)) ^ (2 / 3)

theorem stoch_to_det.contact_hypercontractive.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {S : Finset (α × β)}
  {w : α × β → ℝ}
  (hw : stoch_to_det.Feasible S w)
  {q : α × β → ℝ}
  (hq : stoch_to_det.IsContact S w q)
  {f : α → ℝ} {g : β → ℝ}
  (hf : ∀ (x : α), 0 ≤ f x)
  (hg : ∀ (y : β), 0 ≤ g y) :
  ∑ z ∈ S, q z * f z.1 * g z.2 ≤
    (∑ x,
          stoch_to_det.mX q x *
            f x ^ (3 / 2)) ^
        (2 / 3) *
      (∑ y,
          stoch_to_det.mY q y *
            g y ^ (3 / 2)) ^
        (2 / 3)

Hypercontractivity of contacts:
`E_q[f(X) g(Y)] ≤ ‖f‖_{L^{3/2}(q_X)} ‖g‖_{L^{3/2}(q_Y)}` for `f, g ≥ 0`.

This inequality is proved by applying
`Feasible` to the tilted marginals.

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_hessian_cube_test {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P : NaturalLatents.General.Law X Y}
  (hw : stoch_to_det.Feasible S w) (hP : stoch_to_det.IsContact S w P)
  (F : X → ℝ) (G : Y → ℝ) (t : ℝ) (hF : ∀ (x : X), 0 ≤ 1 + t * F x)
  (hG : ∀ (y : Y), 0 ≤ 1 + t * G y) :
  (NaturalLatents.General.expect P fun z =>
        (1 + t * F z.1) ^ 2 * (1 + t * G z.2) ^ 2) ^
      3 ≤
    (NaturalLatents.General.expect P fun z => (1 + t * F z.1) ^ 3) ^ 2 *
      (NaturalLatents.General.expect P fun z => (1 + t * G z.2) ^ 3) ^ 2

theorem NaturalLatents.General.contact_hessian_cube_test
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P : NaturalLatents.General.Law X Y}
  (hw : stoch_to_det.Feasible S w)
  (hP : stoch_to_det.IsContact S w P)
  (F : X → ℝ) (G : Y → ℝ) (t : ℝ)
  (hF : ∀ (x : X), 0 ≤ 1 + t * F x)
  (hG : ∀ (y : Y), 0 ≤ 1 + t * G y) :
  (NaturalLatents.General.expect P
        fun z =>
        (1 + t * F z.1) ^ 2 *
          (1 + t * G z.2) ^ 2) ^
      3 ≤
    (NaturalLatents.General.expect P
          fun z => (1 + t * F z.1) ^ 3) ^
        2 *
      (NaturalLatents.General.expect P
          fun z => (1 + t * G z.2) ^ 3) ^
        2

Proof for Theorem 2.2.3

uses 0

Lean proves: E_P[FG]\le(E_PF^{3/2})^{2/3}(E_PG^{3/2})^{2/3} for nonnegative marginal fields F,G (contact_hypercontractive), whose F=A^2,G=B^2 specialization gives (C1.15).

Handle a zero normalizer separately, then insert the normalized cubed marginal fields into feasibility. See the page section.

Lean: (C1.15) is not stated separately; it is the case of stoch_to_det.contact_hypercontractive (NaturalLatents/Upstream/Duality.lean) with the fields A^2 and B^2, which assumes a feasible kernel and a contact, without positivity on S. contact_hessian_cube_test (NaturalLatents/General/Contact.lean) applies it to the fields (1+tF)^2 and (1+tG)^2 in the proof of Lemma C1.4.

Theorem2.2.4

Group: Contact moments and the feasible Hessian. (4)

Group member previews

Preview

Theorem 2.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 2.2.5

Loading preview

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

✓L∃∀N

Tagskernel-verified

Lemma C1.4 (the feasible Hessian test). For every finite nonempty X,Y, every nonempty support S with all rows and columns used, every feasible w>0 on S, every positive contact P of w, and every real marginal fields F:X\to\mathbb R, G:Y\to\mathbb R satisfying E_PF=E_PG=0,

4E_P[FG]\leq E_PF^2+E_PG^2. \qquad \text{(C1.18)}

Lean code for Theorem2.2.4●3 theorems

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_hessian {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P : NaturalLatents.General.Law X Y}
  (hw : stoch_to_det.Feasible S w) (hP : stoch_to_det.IsContact S w P)
  (F : X → ℝ) (G : Y → ℝ)
  (hF : (NaturalLatents.General.expect P fun z => F z.1) = 0)
  (hG : (NaturalLatents.General.expect P fun z => G z.2) = 0) :
  (4 * NaturalLatents.General.expect P fun z => F z.1 * G z.2) ≤
    (NaturalLatents.General.expect P fun z => F z.1 ^ 2) +
      NaturalLatents.General.expect P fun z => G z.2 ^ 2

theorem NaturalLatents.General.contact_hessian
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P : NaturalLatents.General.Law X Y}
  (hw : stoch_to_det.Feasible S w)
  (hP : stoch_to_det.IsContact S w P)
  (F : X → ℝ) (G : Y → ℝ)
  (hF :
    (NaturalLatents.General.expect P
        fun z => F z.1) =
      0)
  (hG :
    (NaturalLatents.General.expect P
        fun z => G z.2) =
      0) :
  (4 *
      NaturalLatents.General.expect P
        fun z => F z.1 * G z.2) ≤
    (NaturalLatents.General.expect P
        fun z => F z.1 ^ 2) +
      NaturalLatents.General.expect P
        fun z => G z.2 ^ 2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_hessian_cube_test {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P : NaturalLatents.General.Law X Y}
  (hw : stoch_to_det.Feasible S w) (hP : stoch_to_det.IsContact S w P)
  (F : X → ℝ) (G : Y → ℝ) (t : ℝ) (hF : ∀ (x : X), 0 ≤ 1 + t * F x)
  (hG : ∀ (y : Y), 0 ≤ 1 + t * G y) :
  (NaturalLatents.General.expect P fun z =>
        (1 + t * F z.1) ^ 2 * (1 + t * G z.2) ^ 2) ^
      3 ≤
    (NaturalLatents.General.expect P fun z => (1 + t * F z.1) ^ 3) ^ 2 *
      (NaturalLatents.General.expect P fun z => (1 + t * G z.2) ^ 3) ^ 2

theorem NaturalLatents.General.contact_hessian_cube_test
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P : NaturalLatents.General.Law X Y}
  (hw : stoch_to_det.Feasible S w)
  (hP : stoch_to_det.IsContact S w P)
  (F : X → ℝ) (G : Y → ℝ) (t : ℝ)
  (hF : ∀ (x : X), 0 ≤ 1 + t * F x)
  (hG : ∀ (y : Y), 0 ≤ 1 + t * G y) :
  (NaturalLatents.General.expect P
        fun z =>
        (1 + t * F z.1) ^ 2 *
          (1 + t * G z.2) ^ 2) ^
      3 ≤
    (NaturalLatents.General.expect P
          fun z => (1 + t * F z.1) ^ 3) ^
        2 *
      (NaturalLatents.General.expect P
          fun z => (1 + t * G z.2) ^ 3) ^
        2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_hessian_coefficient {a b l : ℝ → ℝ}
  (ha : ContinuousAt a 0) (hb : ContinuousAt b 0)
  (hl : ContinuousAt l 0)
  (h :
    ∀ᶠ (t : ℝ) in nhds 0,
      (1 + t ^ 2 * l t) ^ 3 ≤
        (1 + t ^ 2 * a t) ^ 2 * (1 + t ^ 2 * b t) ^ 2) :
  3 * l 0 ≤ 2 * (a 0 + b 0)

theorem NaturalLatents.General.contact_hessian_coefficient
  {a b l : ℝ → ℝ} (ha : ContinuousAt a 0)
  (hb : ContinuousAt b 0)
  (hl : ContinuousAt l 0)
  (h :
    ∀ᶠ (t : ℝ) in nhds 0,
      (1 + t ^ 2 * l t) ^ 3 ≤
        (1 + t ^ 2 * a t) ^ 2 *
          (1 + t ^ 2 * b t) ^ 2) :
  3 * l 0 ≤ 2 * (a 0 + b 0)

Proof for Theorem 2.2.4

uses 0

Apply the feasibility inequality to small positive perturbations and extract the quadratic coefficient by a finite real limit. See the page section.

Lean: NaturalLatents.General.contact_hessian (NaturalLatents/General/Contact.lean). It assumes a feasible kernel and a contact, without positivity on S. Its proof uses contact_hessian_cube_test, the cube of (C1.15) for the fields 1+tF and 1+tG, and extracts the coefficient of t^2 by a one-sided limit (contact_hessian_coefficient) instead of Taylor's formula for z^{2/3}.

Theorem2.2.5

Group: Contact moments and the feasible Hessian. (4)

Group member previews

Preview

Theorem 2.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Theorem 2.2.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 6.1.1

Loading preview

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

✓L∃∀N

Tagspartly kernel-verified

Lemma C1.5 (the contact quartic bound). For every finite nonempty X,Y, every nonempty common support S with all rows and columns used, every feasible w>0 on S, and every pair of positive contacts P,R, the quantities defined in (C1.3) satisfy

J\leq6A_0B_0-s^2\leq\frac{s^2}{2}. \qquad \text{(C1.23)}

Lean code for Theorem2.2.5●3 theorems

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_quarticMoment_bound {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {P R : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P)
  (hU2 :
    (NaturalLatents.General.expect P fun z =>
        stoch_to_det.contactSecantX P R z.1 ^ 2) =
      2 * NaturalLatents.General.defectX P R -
        NaturalLatents.General.defectY P R)
  (hV2 :
    (NaturalLatents.General.expect P fun z =>
        stoch_to_det.contactSecantY P R z.2 ^ 2) =
      2 * NaturalLatents.General.defectY P R -
        NaturalLatents.General.defectX P R)
  (hquartic :
    NaturalLatents.General.quarticMoment P R =
      (4 *
          NaturalLatents.General.expect P fun z =>
            stoch_to_det.contactSecantX P R z.1 *
              stoch_to_det.contactSecantY P R z.2) -
        NaturalLatents.General.separation P R)
  (hhessian :
    ∀ (F : X → ℝ) (G : Y → ℝ),
      (NaturalLatents.General.expect P fun z => F z.1) = 0 →
        (NaturalLatents.General.expect P fun z => G z.2) = 0 →
          (4 * NaturalLatents.General.expect P fun z => F z.1 * G z.2) ≤
            (NaturalLatents.General.expect P fun z => F z.1 ^ 2) +
              NaturalLatents.General.expect P fun z => G z.2 ^ 2) :
  NaturalLatents.General.quarticMoment P R ≤
    6 * NaturalLatents.General.defectX P R *
        NaturalLatents.General.defectY P R -
      NaturalLatents.General.separation P R ^ 2

theorem NaturalLatents.General.contact_quarticMoment_bound
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {P R : NaturalLatents.General.Law X Y}
  (hP : stoch_to_det.IsPMF P)
  (hU2 :
    (NaturalLatents.General.expect P
        fun z =>
        stoch_to_det.contactSecantX P R
            z.1 ^
          2) =
      2 *
          NaturalLatents.General.defectX P
            R -
        NaturalLatents.General.defectY P
          R)
  (hV2 :
    (NaturalLatents.General.expect P
        fun z =>
        stoch_to_det.contactSecantY P R
            z.2 ^
          2) =
      2 *
          NaturalLatents.General.defectY P
            R -
        NaturalLatents.General.defectX P
          R)
  (hquartic :
    NaturalLatents.General.quarticMoment P
        R =
      (4 *
          NaturalLatents.General.expect P
            fun z =>
            stoch_to_det.contactSecantX P
                R z.1 *
              stoch_to_det.contactSecantY
                P R z.2) -
        NaturalLatents.General.separation
          P R)
  (hhessian :
    ∀ (F : X → ℝ) (G : Y → ℝ),
      (NaturalLatents.General.expect P
            fun z => F z.1) =
          0 →
        (NaturalLatents.General.expect P
              fun z => G z.2) =
            0 →
          (4 *
              NaturalLatents.General.expect
                P fun z =>
                F z.1 * G z.2) ≤
            (NaturalLatents.General.expect
                P fun z => F z.1 ^ 2) +
              NaturalLatents.General.expect
                P fun z => G z.2 ^ 2) :
  NaturalLatents.General.quarticMoment P
      R ≤
    6 *
          NaturalLatents.General.defectX P
            R *
        NaturalLatents.General.defectY P
          R -
      NaturalLatents.General.separation P
          R ^
        2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_scalar_bound {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  (P R : NaturalLatents.General.Law X Y) :
  6 * NaturalLatents.General.defectX P R *
        NaturalLatents.General.defectY P R -
      NaturalLatents.General.separation P R ^ 2 ≤
    NaturalLatents.General.separation P R ^ 2 / 2

theorem NaturalLatents.General.contact_scalar_bound
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  (P R : NaturalLatents.General.Law X Y) :
  6 * NaturalLatents.General.defectX P R *
        NaturalLatents.General.defectY P
          R -
      NaturalLatents.General.separation P
          R ^
        2 ≤
    NaturalLatents.General.separation P
          R ^
        2 /
      2

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_moments {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  NaturalLatents.General.ContactMoments S P R

theorem NaturalLatents.General.contact_moments
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  NaturalLatents.General.ContactMoments S
    P R

Two distinct positive contacts `P`, `R` of a common feasible kernel satisfy the moment relations of
`ContactMoments`, in particular `quarticMoment P R ≤ separation P R ^ 2 / 2`.

Proof for Theorem 2.2.5

uses 0

Lean proves: J\le6A_0B_0-s^2\le s^2/2 for distinct P\ne R; the equal-pair case (J=s=0) is immediate and is not stated in Lean.

Center the shifted ratio fields, apply the Hessian test, and use square nonnegativity. See the page section.

Lean: contact_quarticMoment_bound (the first inequality) and contact_scalar_bound (the second), both NaturalLatents.General.* in NaturalLatents/General/Contact.lean. contact_quarticMoment_bound assumes only that P is a probability law, together with the energy and quartic identities of Lemma C1.2 and the Hessian test as hypotheses; R is an arbitrary real array and no contact hypothesis appears. contact_scalar_bound holds for arbitrary real arrays P,R, since it uses only s=A_0+B_0. The contact-moment lemma is NaturalLatents.General.contact_moments (NaturalLatents/General/Contact.lean): for every CommonSupportPair S w P R it proves the structure ContactMoments S P R (NaturalLatents/General/Definitions.lean), whose fields are the conditional identities, E_Pf^3=E_Pg^3=1, the second-moment identities, 0<s<2, the two energy identities, the quartic identity, the Hessian test and both inequalities of (C1.23). It does not include the ratio identity, A_0,B_0\ge0 or the symmetry of s.