6.1. 2. The affinity bound🔗

Units and conventions are those of section 0 of the contact page: logarithms are natural. Fix finite nonempty alphabets X,Y, a nonempty common support S\subseteq X\times Y with all rows and columns used, a feasible kernel w>0 on S as in (C1.1), and two positive contacts P,R of w as in (C1.2). The fields of (C1.3) are the cube-root marginal ratios f=(R_X/P_X)^{1/3} and g=(R_Y/P_Y)^{1/3}, their shifts U=f-1 and V=g-1, the mean losses A_0=1-E_Pf and B_0=1-E_Pg, the separation s=A_0+B_0, and the quartic moment J=E_P[U^2V^2]; all expectations are under P. For contacts as in section 1 define

\begin{aligned} BC_X(P,R)&=\sum_x\sqrt{P_X(x)R_X(x)},& BC_Y(P,R)&=\sum_y\sqrt{P_Y(y)R_Y(y)},\\ b(t)&=1-\frac{9t}{16}+\frac{3t^2}{64},& \Psi(t)&=-2\ln b(t). \end{aligned} \qquad \text{(A2.1)}

The formula for \Psi(t) is used only where b(t)>0. This section uses the identities and the quartic estimate of section 1 (Lemmas C1.1, C1.2 and C1.5 of the contact page); it establishes no further contact or Hessian argument. The letters P,R, f,g,U,V,A_0,B_0,s,J are those of the contact page; h_X,h_Y below are Hellinger distances, not the seed entropy h, and y=\sqrt f is a local variable.

Lean: affinityPoly (b), separationPrice (\Psi) and AffinityBound (NaturalLatents/General/Definitions.lean), all NaturalLatents.General.*; BC_X and BC_Y are stoch_to_det.BC (NaturalLatents/Upstream/Toolkit.lean) applied to the X and Y marginals. separationPrice is defined for every real t through Lean's totalized logarithm, and agrees with (A2.1) where b(t)>0.

Theorem6.1.1

group

Statement uses 4

Statement dependency previews

Preview

Theorem 2.2.1

Loading preview

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

used by 1✓L∃∀N

Tagskernel-verified

Lemma A2.1 (each marginal affinity is at most the quadratic b at s). 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 distinct positive contacts P,R, assume the conclusions (C1.4), (C1.9), 0<s<2, and (C1.23) of section 1. Then the affinities defined in (A2.1) satisfy

0<BC_X(P,R)\leq b(s),\qquad 0<BC_Y(P,R)\leq b(s). \qquad \text{(A2.2)}

Lean code for Theorem6.1.1●5 theorems

theoremdefined in NaturalLatents/General/Affinity.lean

complete

theorem NaturalLatents.General.affinity_bhattacharyyaX_le {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)
  (hmoments : NaturalLatents.General.ContactMoments S P R) :
  stoch_to_det.BC (stoch_to_det.mX P) (stoch_to_det.mX R) ≤
    NaturalLatents.General.affinityPoly
      (NaturalLatents.General.separation P R)

theorem NaturalLatents.General.affinity_bhattacharyyaX_le
  {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)
  (hmoments :
    NaturalLatents.General.ContactMoments
      S P R) :
  stoch_to_det.BC (stoch_to_det.mX P)
      (stoch_to_det.mX R) ≤
    NaturalLatents.General.affinityPoly
      (NaturalLatents.General.separation P
        R)

theoremdefined in NaturalLatents/General/Affinity.lean

complete

theorem NaturalLatents.General.affinity_bhattacharyyaY_le {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)
  (hmoments : NaturalLatents.General.ContactMoments S P R) :
  stoch_to_det.BC (stoch_to_det.mY P) (stoch_to_det.mY R) ≤
    NaturalLatents.General.affinityPoly
      (NaturalLatents.General.separation P R)

theorem NaturalLatents.General.affinity_bhattacharyyaY_le
  {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)
  (hmoments :
    NaturalLatents.General.ContactMoments
      S P R) :
  stoch_to_det.BC (stoch_to_det.mY P)
      (stoch_to_det.mY R) ≤
    NaturalLatents.General.affinityPoly
      (NaturalLatents.General.separation P
        R)

theoremdefined in NaturalLatents/General/Affinity.lean

complete

theorem NaturalLatents.General.affinity_affinities_pos {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) :
  0 < stoch_to_det.BC (stoch_to_det.mX P) (stoch_to_det.mX R) ∧
    0 < stoch_to_det.BC (stoch_to_det.mY P) (stoch_to_det.mY R)

theorem NaturalLatents.General.affinity_affinities_pos
  {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) :
  0 <
      stoch_to_det.BC (stoch_to_det.mX P)
        (stoch_to_det.mX R) ∧
    0 <
      stoch_to_det.BC (stoch_to_det.mY P)
        (stoch_to_det.mY R)

theoremdefined in NaturalLatents/General/Affinity.lean

complete

theorem NaturalLatents.General.affinity_conditional_square {ι : Type}
  [Fintype ι] (q G : ι → ℝ) (a : ℝ) (hq : ∀ (i : ι), 0 ≤ q i)
  (ha : 0 < a) (hsecond : ∑ i, q i * G i ^ 2 = (∑ i, q i) * a) :
  (∑ i, q i) * (√a - 1) ^ 2 ≤ ∑ i, q i * (G i - 1) ^ 2

theorem NaturalLatents.General.affinity_conditional_square
  {ι : Type} [Fintype ι] (q G : ι → ℝ)
  (a : ℝ) (hq : ∀ (i : ι), 0 ≤ q i)
  (ha : 0 < a)
  (hsecond :
    ∑ i, q i * G i ^ 2 = (∑ i, q i) * a) :
  (∑ i, q i) * (√a - 1) ^ 2 ≤
    ∑ i, q i * (G i - 1) ^ 2

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

Proof for Theorem 6.1.1

uses 0

The listed moment hypotheses supply every field of ContactMoments except hessian; NaturalLatents.General.contact_hessian (C1.4) supplies that field from the assumed feasible kernel and contact.

Factor the pointwise Hellinger deficit, use conditional Cauchy-Schwarz and the quartic bound, and expand the marginal Hellinger sums. See the page section.

Lean: NaturalLatents.General.affinity_bhattacharyyaX_le and NaturalLatents.General.affinity_bhattacharyyaY_le (the upper bounds) and NaturalLatents.General.affinity_affinities_pos (positivity), in NaturalLatents/General/Affinity.lean. They take CommonSupportPair S w P R and, for the upper bounds, ContactMoments S P R, the conclusions of section 1 as stated in Lean. In place of a named Cauchy-Schwarz theorem, affinity_conditional_square (same file) derives the conditional comparison of (A2.6) and (A2.9) by expanding a nonnegative weighted square.

Theorem6.1.2

group

Statement uses 2

Statement dependency previews

Preview

Theorem 2.2.2

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 8.1.3

Loading preview

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

✓L∃∀N

Tagspartly kernel-verified

Lemma A2.2 (the natural-log affinity payment and the equal-pair endpoint). 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 distinct positive contacts P,R, assume the conclusions of section 1 and of Lemma A2.1. Then \Psi(s) is well defined and nonnegative, and

-\ln BC_X(P,R)-\ln BC_Y(P,R)\geq\Psi(s). \qquad \text{(A2.11)}

Distinct pairs and equal pairs are treated separately. For every equal pair P=R on the same contact domain, (C1.3) gives s=0, so marginal normalization gives BC_X=BC_Y=b(0)=1 and \Psi(0)=0, with equality in (A2.11).

Lean code for Theorem6.1.2●2 theorems

theoremdefined in NaturalLatents/General/Affinity.lean

complete

theorem NaturalLatents.General.affinity_bound {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)
  (hmoments : NaturalLatents.General.ContactMoments S P R) :
  NaturalLatents.General.AffinityBound P R

theorem NaturalLatents.General.affinity_bound
  {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)
  (hmoments :
    NaturalLatents.General.ContactMoments
      S P R) :
  NaturalLatents.General.AffinityBound P R

The separation price is paid by the marginal Bhattacharyya affinities of two contacts.

theoremdefined in NaturalLatents/General/Definitions.lean

complete

theorem NaturalLatents.General.affinityPoly_pos (t : ℝ) (ht : t ≤ 2) :
  0 < NaturalLatents.General.affinityPoly t

theorem NaturalLatents.General.affinityPoly_pos
  (t : ℝ) (ht : t ≤ 2) :
  0 <
    NaturalLatents.General.affinityPoly t

Proof for Theorem 6.1.2

uses 0

Lean proves: the affinity-payment inequality (A2.11) for distinct positive contacts with ContactMoments, and b(t)>0 for t\le2.

Bound the quadratic on the scalar interval and apply monotonicity of the natural logarithm, treating equal contacts separately. See the page section.

Lean: NaturalLatents.General.affinity_bound (NaturalLatents/General/Affinity.lean) proves AffinityBound P R, which is (A2.11), for every CommonSupportPair S w P R given ContactMoments S P R. It obtains b(s)>0 from NaturalLatents.General.affinityPoly_pos (NaturalLatents/General/Definitions.lean, positivity of b(t) for t\le2), and does not state the range 1/16\le b\le1, the nonnegativity of \Psi(s), or the case of equal contacts.