8.1. 5. The mismatch payment🔗

Theorem8.1.1

Group: The mismatch payment. (4)

Group member previews

Preview

Theorem 8.1.2

Loading preview

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

uses 1

Used by 2

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 P5.1 (replica symmetry and the relative-entropy profile). Let p=\sum_i \pi_i q_i be any finite latent with positive priors, and construct the replicas by (Q3.2). Put \mu_{ij}=\Pr(L_1=i,L_2=j) and \Omega=\{(i,j):\mu_{ij}>0\}. For (i,j)\in\Omega, put t_{ij}=\Pr(Z=\cdot\mid L_1=i,L_2=j); positive pair mass is where the conditional law is defined, and a pair of zero mass is omitted. Then

\begin{aligned} \mu_{ij}&=\sum_{z:p(z)>0}p(z)r_z(i)r_z(j)=\mu_{ji},\\ t_{ij}(z)&=\frac{p(z)r_z(i)r_z(j)}{\mu_{ij}}=t_{ji}(z),\\ \sum_j\mu_{ij} &=\sum_{z:p(z)>0}p(z)r_z(i)\sum_jr_z(j) =\sum_{z:p(z)>0}p(z)r_z(i)=\pi_i. \end{aligned} \qquad \text{(P5.1)}

Both marginal relative-entropy sums have an endpoint symmetrization:

\begin{aligned} I(L_2;X\mid L_1) &=\sum_{(i,j)\in\Omega}\mu_{ij} D((t_{ij})_X\Vert(q_i)_X)\\ &=\sum_{(i,j)\in\Omega}\mu_{ij} D((t_{ij})_X\Vert(q_j)_X)\\ &=\frac12\sum_{(i,j)\in\Omega}\mu_{ij} \bigl[D((t_{ij})_X\Vert(q_i)_X) +D((t_{ij})_X\Vert(q_j)_X)\bigr],\\ I(L_2;Y\mid L_1) &=\sum_{(i,j)\in\Omega}\mu_{ij} D((t_{ij})_Y\Vert(q_i)_Y)\\ &=\sum_{(i,j)\in\Omega}\mu_{ij} D((t_{ij})_Y\Vert(q_j)_Y)\\ &=\frac12\sum_{(i,j)\in\Omega}\mu_{ij} \bigl[D((t_{ij})_Y\Vert(q_i)_Y) +D((t_{ij})_Y\Vert(q_j)_Y)\bigr]. \end{aligned} \qquad \text{(P5.2)}

Lean code for Theorem8.1.1●6 theorems

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_pairMass_comm {X Y : Type} [Fintype X]
  [Fintype Y] {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p) (i j : L.ι) :
  NaturalLatents.General.pairMass L i j =
    NaturalLatents.General.pairMass L j i

theorem NaturalLatents.General.payment_pairMass_comm
  {X Y : Type} [Fintype X] [Fintype Y]
  {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p)
  (i j : L.ι) :
  NaturalLatents.General.pairMass L i j =
    NaturalLatents.General.pairMass L j i

Posterior overlap is symmetric.

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_pairMass_rows {X Y : Type} [Fintype X]
  [Fintype Y] {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p) (i : L.ι) :
  ∑ j, NaturalLatents.General.pairMass L i j = L.prior i

theorem NaturalLatents.General.payment_pairMass_rows
  {X Y : Type} [Fintype X] [Fintype Y]
  {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p) (i : L.ι) :
  ∑ j,
      NaturalLatents.General.pairMass L i
        j =
    L.prior i

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_pairMass_nonneg {X Y : Type} [Fintype X]
  [Fintype Y] {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) (i j : L.ι) :
  0 ≤ NaturalLatents.General.pairMass L i j

theorem NaturalLatents.General.payment_pairMass_nonneg
  {X Y : Type} [Fintype X] [Fintype Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (L : stoch_to_det.Latent p)
  (i j : L.ι) :
  0 ≤
    NaturalLatents.General.pairMass L i j

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_condMI_KL.{u_1, u_2} {A : Type u_1}
  {C : Type u_2} [Fintype A] [Fintype C] [DecidableEq A] [DecidableEq C]
  (q : A × A × C → ℝ) (a : A → ℝ) (P : A → C → ℝ)
  (hq : stoch_to_det.IsPMF q) (ha : ∀ (i : A), 0 < a i)
  (hP : ∀ (i : A), stoch_to_det.IsPMF (P i))
  (hrow : ∀ (i : A) (c : C), ∑ j, q (i, j, c) = a i * P i c)
  (hm : ∀ (i j : A), 0 < ∑ c, q (i, j, c)) :
  stoch_to_det.condMI (fun u => u.2.1) (fun u => u.2.2) (fun u => u.1)
      q =
    ∑ i,
      ∑ j,
        (∑ c, q (i, j, c)) *
          stoch_to_det.KL (fun c => q (i, j, c) / ∑ c, q (i, j, c))
            (P i)

theorem NaturalLatents.General.payment_condMI_KL.{u_1,
    u_2}
  {A : Type u_1} {C : Type u_2}
  [Fintype A] [Fintype C] [DecidableEq A]
  [DecidableEq C] (q : A × A × C → ℝ)
  (a : A → ℝ) (P : A → C → ℝ)
  (hq : stoch_to_det.IsPMF q)
  (ha : ∀ (i : A), 0 < a i)
  (hP :
    ∀ (i : A), stoch_to_det.IsPMF (P i))
  (hrow :
    ∀ (i : A) (c : C),
      ∑ j, q (i, j, c) = a i * P i c)
  (hm :
    ∀ (i j : A), 0 < ∑ c, q (i, j, c)) :
  stoch_to_det.condMI (fun u => u.2.1)
      (fun u => u.2.2) (fun u => u.1) q =
    ∑ i,
      ∑ j,
        (∑ c, q (i, j, c)) *
          stoch_to_det.KL
            (fun c =>
              q (i, j, c) /
                ∑ c, q (i, j, c))
            (P i)

Conditional MI of a finite replica law is a weighted conditional KL sum (bits).

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_midpoint_profile.{u_1, u_2}
  {A : Type u_1} {C : Type u_2} [Fintype A] [Fintype C] [DecidableEq A]
  [DecidableEq C] (q : A × A × C → ℝ) (a : A → ℝ) (P : A → C → ℝ)
  (hq : stoch_to_det.IsPMF q) (ha : ∀ (i : A), 0 < a i)
  (hP : ∀ (i : A), stoch_to_det.IsPMF (P i))
  (hrow : ∀ (i : A) (c : C), ∑ j, q (i, j, c) = a i * P i c)
  (hm : ∀ (i j : A), 0 < ∑ c, q (i, j, c))
  (hsym : ∀ (i j : A) (c : C), q (i, j, c) = q (j, i, c)) :
  ∑ i,
      ∑ j,
        (∑ c, q (i, j, c)) * -Real.log (stoch_to_det.BC (P i) (P j)) ≤
    NaturalLatents.General.condMINat (fun u => u.2.1) (fun u => u.2.2)
      (fun u => u.1) q

theorem NaturalLatents.General.payment_midpoint_profile.{u_1,
    u_2}
  {A : Type u_1} {C : Type u_2}
  [Fintype A] [Fintype C] [DecidableEq A]
  [DecidableEq C] (q : A × A × C → ℝ)
  (a : A → ℝ) (P : A → C → ℝ)
  (hq : stoch_to_det.IsPMF q)
  (ha : ∀ (i : A), 0 < a i)
  (hP :
    ∀ (i : A), stoch_to_det.IsPMF (P i))
  (hrow :
    ∀ (i : A) (c : C),
      ∑ j, q (i, j, c) = a i * P i c)
  (hm : ∀ (i j : A), 0 < ∑ c, q (i, j, c))
  (hsym :
    ∀ (i j : A) (c : C),
      q (i, j, c) = q (j, i, c)) :
  ∑ i,
      ∑ j,
        (∑ c, q (i, j, c)) *
          -Real.log
              (stoch_to_det.BC (P i)
                (P j)) ≤
    NaturalLatents.General.condMINat
      (fun u => u.2.1) (fun u => u.2.2)
      (fun u => u.1) q

Midpoint KL and replica symmetry pay the entire marginal affinity profile.

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_pairMass_pos {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (D : NaturalLatents.General.CommonSetup p) (i j : D.L.ι) :
  0 < NaturalLatents.General.pairMass D.L i j

theorem NaturalLatents.General.payment_pairMass_pos
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (D :
    NaturalLatents.General.CommonSetup p)
  (i j : D.L.ι) :
  0 <
    NaturalLatents.General.pairMass D.L i
      j

Proof for Theorem 8.1.1

uses 0

Lean proves: symmetry, nonnegativity and row sums \sum_j\mu_{ij}=\pi_i of the pair masses, strict positivity of every pair mass for a CommonSetup (payment_pairMass_pos), the first relative-entropy expression of (P5.2) when every pair mass is positive, and the resulting midpoint-profile inequality under replica symmetry.

Expand the posterior pair masses and conditional relative entropies, then interchange the replica labels and average. See the page section.

Lean: pairMass (NaturalLatents/General/Definitions.lean) is \mu_{ij}=\sum_zp(z)r_z(i)r_z(j), summing over all cells, those with p(z)=0 contributing zero, with payment_pairMass_comm (symmetry), payment_pairMass_rows (row sums \pi_i) and payment_pairMass_nonneg; payment_condMI_KL states the first line of (P5.2), in bits, for any finite law of (L_1,L_2,W) whose rows have the form \pi_iP_i and whose pair masses are all positive, and the symmetrization is a step inside payment_midpoint_profile. Lean names neither t_{ij} nor \Omega: on the setup latent every posterior is positive, so every \mu_{ij} is positive (payment_pairMass_pos) and \Omega contains every pair.

Theorem8.1.2

Group: The mismatch payment. (4)

Group member previews

Preview

Theorem 8.1.1

Loading preview

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

uses 0used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma P5.2 (normalized midpoint; Gibbs' inequality). Let a,b,t be probability vectors on a finite nonempty set, with a_x>0 and b_x>0 wherever t_x>0. Put c=BC(a,b)=\sum_x \sqrt{\smash[b]{a_x b_x}} and v_x=\sqrt{\smash[b]{a_x b_x}}/c. Then c>0, v is a probability vector, and

\begin{aligned} D(t\Vert v) &=\sum_{x:t_x>0}t_x\ln\frac{t_x}{\frac{\sqrt{a_xb_x}}{c}}\\ &=\sum_{x:t_x>0}t_x\ln t_x -\frac12\sum_{x:t_x>0}t_x\ln a_x -\frac12\sum_{x:t_x>0}t_x\ln b_x+\ln c\\ &=\frac{D(t\Vert a)+D(t\Vert b)}2+\ln c. \end{aligned} \qquad \text{(P5.3)}

Consequently

\frac{D(t\Vert a)+D(t\Vert b)}2 =D(t\Vert v)-\ln BC(a,b)\ge-\ln BC(a,b). \qquad \text{(P5.4)}

Lean code for Theorem8.1.2●1 theorem

theoremdefined in NaturalLatents/Upstream/Toolkit.lean

complete

theorem stoch_to_det.bhattacharyya_le.{u_1} {ω : Type u_1} [Fintype ω]
  {P Q : ω → ℝ} (hP : stoch_to_det.IsPMF P) (hQ : stoch_to_det.IsPMF Q)
  {r : ω → ℝ} (hr : stoch_to_det.IsPMF r)
  (hacP : stoch_to_det.AbsCont r P) (hacQ : stoch_to_det.AbsCont r Q) :
  -2 * stoch_to_det.lg (stoch_to_det.BC P Q) ≤
    stoch_to_det.KL r P + stoch_to_det.KL r Q

theorem stoch_to_det.bhattacharyya_le.{u_1}
  {ω : Type u_1} [Fintype ω] {P Q : ω → ℝ}
  (hP : stoch_to_det.IsPMF P)
  (hQ : stoch_to_det.IsPMF Q) {r : ω → ℝ}
  (hr : stoch_to_det.IsPMF r)
  (hacP : stoch_to_det.AbsCont r P)
  (hacQ : stoch_to_det.AbsCont r Q) :
  -2 *
      stoch_to_det.lg
        (stoch_to_det.BC P Q) ≤
    stoch_to_det.KL r P +
      stoch_to_det.KL r Q

Bhattacharyya inequality:
`min_r [D(r‖P) + D(r‖Q)] = −2 lg BC(P,Q)`. Only the lower-bound direction is needed.

Proof for Theorem 8.1.2

uses 0

Lean proves: -2\log_2BC(a,b)\le D_2(t\Vert a)+D_2(t\Vert b) under absolute continuity of t with respect to both a and b, the bit-valued inequality of (P5.4).

Normalize the geometric midpoint, expand its relative entropy, and apply the finite Gibbs inequality. See the page section.

Lean: stoch_to_det.bhattacharyya_le (NaturalLatents/Upstream/Toolkit.lean) states (P5.4) in bits, as -2\log_2BC(a,b)\le D_2(t\Vert a)+D_2(t\Vert b) with D_2 the relative entropy in bits, under absolute continuity of t with respect to a and b; the reference v and the identity (P5.3) appear only inside its proof.

Theorem8.1.3

Group: The mismatch payment. (4)

Group member previews

Preview

Theorem 8.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 6.1.2

Loading preview

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

used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma P5.3 (separation-profile payment). Let X,Y,L be finite random variables with latent decomposition p=\sum_i\pi_iq_i, positive priors and distinct components that are positive contacts of one feasible kernel on a common support. Suppose the affinity bound, (A2.11) on the affinity page, holds for every distinct pair. Let BC_X and BC_Y be the marginal affinities of (A2.1) on the affinity page, and put s_{ij}=s(q_i,q_j) for i\ne j, with s as in (C1.3) on the contact page. The replicas (Q3.2) satisfy

K\ge\sum_{\substack{(i,j)\in\Omega\\i\ne j}} \mu_{ij}\bigl[-\ln BC_X(q_i,q_j)-\ln BC_Y(q_i,q_j)\bigr] \ge\sum_{\substack{(i,j)\in\Omega\\i\ne j}} \mu_{ij}\Psi(s_{ij}). \qquad \text{(P5.5)}

Lean code for Theorem8.1.3●4 theorems

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_profile_payment {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (D : NaturalLatents.General.CommonSetup p)
  (haffinity :
    ∀ (i j : D.L.ι),
      i ≠ j →
        NaturalLatents.General.AffinityBound (D.L.comp i)
          (D.L.comp j)) :
  ∑ i,
      ∑ j with i ≠ j,
        NaturalLatents.General.pairMass D.L i j *
          NaturalLatents.General.separationPrice
            (NaturalLatents.General.separation (D.L.comp i)
              (D.L.comp j)) ≤
    NaturalLatents.General.replicaBudget D.L

theorem NaturalLatents.General.payment_profile_payment
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (D :
    NaturalLatents.General.CommonSetup p)
  (haffinity :
    ∀ (i j : D.L.ι),
      i ≠ j →
        NaturalLatents.General.AffinityBound
          (D.L.comp i) (D.L.comp j)) :
  ∑ i,
      ∑ j with i ≠ j,
        NaturalLatents.General.pairMass
            D.L i j *
          NaturalLatents.General.separationPrice
            (NaturalLatents.General.separation
              (D.L.comp i) (D.L.comp j)) ≤
    NaturalLatents.General.replicaBudget
      D.L

The replica budget pays the off-diagonal separation prices.

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_coordinate_payment.{u_1} {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (D : NaturalLatents.General.CommonSetup p) {C : Type u_1} [Fintype C]
  [DecidableEq C] (f : X × Y → C) :
  ∑ i,
      ∑ j,
        NaturalLatents.General.pairMass D.L i j *
          -Real.log
              (stoch_to_det.BC (stoch_to_det.push f (D.L.comp i))
                (stoch_to_det.push f (D.L.comp j))) ≤
    NaturalLatents.General.condMINat (fun u => u.2.1) (fun u => f u.2.2)
      (fun u => u.1) (NaturalLatents.General.replicaJoint D.L)

theorem NaturalLatents.General.payment_coordinate_payment.{u_1}
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (D :
    NaturalLatents.General.CommonSetup p)
  {C : Type u_1} [Fintype C]
  [DecidableEq C] (f : X × Y → C) :
  ∑ i,
      ∑ j,
        NaturalLatents.General.pairMass
            D.L i j *
          -Real.log
              (stoch_to_det.BC
                (stoch_to_det.push f
                  (D.L.comp i))
                (stoch_to_det.push f
                  (D.L.comp j))) ≤
    NaturalLatents.General.condMINat
      (fun u => u.2.1) (fun u => f u.2.2)
      (fun u => u.1)
      (NaturalLatents.General.replicaJoint
        D.L)

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_midpoint_profile.{u_1, u_2}
  {A : Type u_1} {C : Type u_2} [Fintype A] [Fintype C] [DecidableEq A]
  [DecidableEq C] (q : A × A × C → ℝ) (a : A → ℝ) (P : A → C → ℝ)
  (hq : stoch_to_det.IsPMF q) (ha : ∀ (i : A), 0 < a i)
  (hP : ∀ (i : A), stoch_to_det.IsPMF (P i))
  (hrow : ∀ (i : A) (c : C), ∑ j, q (i, j, c) = a i * P i c)
  (hm : ∀ (i j : A), 0 < ∑ c, q (i, j, c))
  (hsym : ∀ (i j : A) (c : C), q (i, j, c) = q (j, i, c)) :
  ∑ i,
      ∑ j,
        (∑ c, q (i, j, c)) * -Real.log (stoch_to_det.BC (P i) (P j)) ≤
    NaturalLatents.General.condMINat (fun u => u.2.1) (fun u => u.2.2)
      (fun u => u.1) q

theorem NaturalLatents.General.payment_midpoint_profile.{u_1,
    u_2}
  {A : Type u_1} {C : Type u_2}
  [Fintype A] [Fintype C] [DecidableEq A]
  [DecidableEq C] (q : A × A × C → ℝ)
  (a : A → ℝ) (P : A → C → ℝ)
  (hq : stoch_to_det.IsPMF q)
  (ha : ∀ (i : A), 0 < a i)
  (hP :
    ∀ (i : A), stoch_to_det.IsPMF (P i))
  (hrow :
    ∀ (i : A) (c : C),
      ∑ j, q (i, j, c) = a i * P i c)
  (hm : ∀ (i j : A), 0 < ∑ c, q (i, j, c))
  (hsym :
    ∀ (i j : A) (c : C),
      q (i, j, c) = q (j, i, c)) :
  ∑ i,
      ∑ j,
        (∑ c, q (i, j, c)) *
          -Real.log
              (stoch_to_det.BC (P i)
                (P j)) ≤
    NaturalLatents.General.condMINat
      (fun u => u.2.1) (fun u => u.2.2)
      (fun u => u.1) q

Midpoint KL and replica symmetry pay the entire marginal affinity profile.

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_bhattacharyya_self.{u_1} {C : Type u_1}
  [Fintype C] (P : C → ℝ) (hP : stoch_to_det.IsPMF P) :
  stoch_to_det.BC P P = 1

theorem NaturalLatents.General.payment_bhattacharyya_self.{u_1}
  {C : Type u_1} [Fintype C] (P : C → ℝ)
  (hP : stoch_to_det.IsPMF P) :
  stoch_to_det.BC P P = 1

Proof for Theorem 8.1.3

uses 0

Lean proves: \sum_{i\ne j}\mu_{ij}\Psi(s_{ij})\le K for the setup latent under the distinct-pair affinity hypothesis, the coordinate midpoint-profile inequalities, and BC(q_i,q_i)=1.

Delete the nonnegative diagonal relative entropy terms, apply the midpoint inequality, and then use the affinity bound. See the page section.

Lean: payment_profile_payment states the outer inequality of (P5.5), \sum_{i\ne j}\mu_{ij}\Psi(s_{ij})\le K, for the setup latent given AffinityBound for every distinct pair, through payment_coordinate_payment (one coordinate at a time) and payment_midpoint_profile (the sum over all pairs of (P5.4)); the middle expression of (P5.5) appears only inside its proof. Lean keeps the diagonal pairs and applies (P5.4) to them too, where -\ln BC(q_i,q_i)=0 (payment_bhattacharyya_self), instead of deleting the diagonal relative-entropy summands.

Theorem8.1.4

Group: The mismatch payment. (4)

Group member previews

Preview

Theorem 8.1.1

Loading preview

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

uses 1used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma P5.4 (mismatch mass and the exact information sum). For every finite latent p=\sum_i \pi_i q_i with positive priors and replicas (Q3.2), with d as in (D3) and I(q_i) as in (D2),

\begin{aligned} \sum_{i\ne j}\mu_{ij} &=\sum_{z:p(z)>0}p(z)\sum_{i\ne j}r_z(i)r_z(j)\\ &=\sum_{z:p(z)>0}p(z) \left[\left(\sum_i r_z(i)\right)^2-\sum_i r_z(i)^2\right]\\ &=\sum_{z:p(z)>0}p(z)\left[1-\sum_i r_z(i)^2\right] =E_Z\!\left[1-\sum_i r_Z(i)^2\right]=d. \end{aligned} \qquad \text{(P5.6)}

By the definition of conditional mutual information, M=I(X;Y\mid L)=\sum_i\pi_iI(q_i). The symmetric row and column sums from (P5.1) also give

\begin{aligned} \sum_{i\ne j}\mu_{ij}\frac{I(q_i)+I(q_j)}2 &=\frac12\sum_i(\pi_i-\mu_{ii})I(q_i) +\frac12\sum_j(\pi_j-\mu_{jj})I(q_j)\\ &=\sum_i(\pi_i-\mu_{ii})I(q_i)\\ &=M-\sum_i\mu_{ii}I(q_i)\le M. \end{aligned} \qquad \text{(P5.7)}

Lean code for Theorem8.1.4●3 theorems

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_mismatch {X Y : Type} [Fintype X]
  [Fintype Y] {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p) (L : stoch_to_det.Latent p) :
  NaturalLatents.General.mismatch L =
    ∑ i, ∑ j with i ≠ j, NaturalLatents.General.pairMass L i j

theorem NaturalLatents.General.payment_mismatch
  {X Y : Type} [Fintype X] [Fintype Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (L : stoch_to_det.Latent p) :
  NaturalLatents.General.mismatch L =
    ∑ i,
      ∑ j with i ≠ j,
        NaturalLatents.General.pairMass L
          i j

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_mediation_average {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) :
  NaturalLatents.General.mediation L =
    ∑ i, L.prior i * stoch_to_det.Knat (L.comp i)

theorem NaturalLatents.General.payment_mediation_average
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p) :
  NaturalLatents.General.mediation L =
    ∑ i,
      L.prior i *
        stoch_to_det.Knat (L.comp i)

The conditional information budget is the prior average of component information.

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.payment_information_payment {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (L : stoch_to_det.Latent p) :
  ∑ i,
      ∑ j with i ≠ j,
        NaturalLatents.General.pairMass L i j *
          ((stoch_to_det.Knat (L.comp i) +
              stoch_to_det.Knat (L.comp j)) /
            2) ≤
    NaturalLatents.General.mediation L

theorem NaturalLatents.General.payment_information_payment
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (L : stoch_to_det.Latent p) :
  ∑ i,
      ∑ j with i ≠ j,
        NaturalLatents.General.pairMass L
            i j *
          ((stoch_to_det.Knat (L.comp i) +
              stoch_to_det.Knat
                (L.comp j)) /
            2) ≤
    NaturalLatents.General.mediation L

Proof for Theorem 8.1.4

uses 0

Lean proves: d=\sum_i\sum_{j\ne i}\mu_{ij}, M=\sum_i\pi_iI(q_i), and \sum_{i\ne j}\mu_{ij}(I(q_i)+I(q_j))/2\le M.

Expand the finite posterior square sum and use symmetric pair-mass row sums with nonnegative component information. See the page section.

Lean: payment_mismatch states (P5.6) as d=\sum_i\sum_{j\ne i}\mu_{ij}, proved through d=1-\sum_i\mu_{ii} and the total mass \sum_{i,j}\mu_{ij}=1 rather than expanding \left(\sum_ir_z(i)\right)^2 cell by cell; payment_mediation_average states M=\sum_i\pi_iI(q_i); and payment_information_payment states only the inequality of (P5.7), without the identity with M-\sum_i\mu_{ii}I(q_i).

Theorem8.1.5

Group: The mismatch payment. (4)

Group member previews

Preview

Theorem 8.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 7.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 10.1.1

Loading preview

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

✓L∃∀N

Tagspartly kernel-verified

Lemma P5.5 (the mismatch payment for every nonnegative charge coefficient). For every \beta\ge0, \gamma>0, let p=\sum_i \pi_i q_i be a latent of the setup of section 0 of the contact page, with positive priors and distinct components, satisfying M+B=\tau(p). Thus every q_i is positive on S=\mathrm{supp}\,p and is a contact of one common feasible w>0 on S. Assume the affinity bound for its distinct pairs and PC(\beta,\gamma) on the domain of their common feasible kernel: for every two distinct positive contacts P,R of such a kernel,

\frac{I(P)+I(R)}2+\beta\Psi(s(P,R))\ge\gamma. \qquad \text{(P5.8)}

With M, B and d as in (D3), and with the replica budget K\le2M+B,

\gamma d\le(1+2\beta)M+\beta B. \qquad \text{(P5.9)}

Lean code for Theorem8.1.5●1 theorem

theoremdefined in NaturalLatents/General/Payment.lean

complete

theorem NaturalLatents.General.mismatch_payment {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (D : NaturalLatents.General.CommonSetup p) (beta gamma : ℝ)
  (hbeta : 0 ≤ beta) (hgamma : 0 ≤ gamma)
  (haffinity :
    ∀ (i j : D.L.ι),
      i ≠ j →
        NaturalLatents.General.AffinityBound (D.L.comp i) (D.L.comp j))
  (hreplica :
    NaturalLatents.General.replicaBudget D.L ≤
      2 * NaturalLatents.General.mediation D.L +
        NaturalLatents.General.redundancy D.L)
  (hPC :
    NaturalLatents.General.HasPairCharge
      NaturalLatents.General.CommonSupportPair beta gamma) :
  gamma * NaturalLatents.General.mismatch D.L ≤
    (1 + 2 * beta) * NaturalLatents.General.mediation D.L +
      beta * NaturalLatents.General.redundancy D.L

theorem NaturalLatents.General.mismatch_payment
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (D :
    NaturalLatents.General.CommonSetup p)
  (beta gamma : ℝ) (hbeta : 0 ≤ beta)
  (hgamma : 0 ≤ gamma)
  (haffinity :
    ∀ (i j : D.L.ι),
      i ≠ j →
        NaturalLatents.General.AffinityBound
          (D.L.comp i) (D.L.comp j))
  (hreplica :
    NaturalLatents.General.replicaBudget
        D.L ≤
      2 *
          NaturalLatents.General.mediation
            D.L +
        NaturalLatents.General.redundancy
          D.L)
  (hPC :
    NaturalLatents.General.HasPairCharge
      NaturalLatents.General.CommonSupportPair
      beta gamma) :
  gamma *
      NaturalLatents.General.mismatch
        D.L ≤
    (1 + 2 * beta) *
        NaturalLatents.General.mediation
          D.L +
      beta *
        NaturalLatents.General.redundancy
          D.L

The mismatch of a `CommonSetup` is paid by its budgets: `gamma * mismatch L ≤ (1 + 2 * beta) * mediation L + beta * redundancy L`,
given the affinity bound for every pair, the replica budget and `HasPairCharge beta gamma`.

Proof for Theorem 8.1.5

uses 0

Lean proves: the conclusion under PC(\beta,\gamma) for all supports and all common feasible kernels (HasPairCharge CommonSupportPair β γ), the form that pairCharge_C supplies.

Weight each off-diagonal pair charge by its replica mass and close with the profile payment, information payment, and replica budget. See the page section.

Lean: mismatch_payment, for a CommonSetup p and real \beta,\gamma with \beta\ge0 and \gamma\ge0, taking as hypotheses AffinityBound for every distinct pair, the replica budget K\le2M+B, and HasPairCharge CommonSupportPair beta gamma, the pair charge on distinct positive contacts of any common feasible kernel; it requires \gamma\ge0 where the page keeps \gamma>0, and d_* of (P5.D) has no counterpart, the off-diagonal sum entering through payment_mismatch.

The payment at the pair charge PC(23/250, 7/60). The pair charge PC(23/250,7/60) is inequality (P5.8) with \beta=23/250 and \gamma=7/60, on every two distinct positive contacts of a common feasible kernel. Since 1+2\cdot23/250=148/125, Lemma P5.5 at these values gives

\frac7{60}\,d\le\frac{148}{125}\,M+\frac{23}{250}\,B, \qquad\text{equivalently}\qquad d\le\frac{1776}{175}\,M+\frac{138}{175}\,B. \qquad \text{(P5.11)}

The second form divides by \gamma=7/60: (60/7)(148/125)=1776/175 and (60/7)(23/250)=138/175.

Lean: mismatch_payment at (23/250) (7/60) with pairCharge_C (NaturalLatents/General/PairCharge.lean), the pair charge PC(23/250,7/60), inside T_le_of_connected (NaturalLatents/General/Pricing.lean); the divided form of (P5.11) is not stated.