Natural latents: a bound below seven

7.1. 3. The replica budget🔗

Units and conventions are those of section 0 of the contact page: information is in nats, conditional sums range over positive-probability conditioning events, and nonnegativity of conditional mutual information is Gibbs' inequality. The budgets M, B of (Q3.1) are those of (D3); the remainders C and N of (Q3.3) are local to this page, and C is not the constant of the theorem.

Theorem7.1.1

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 8.1.1

Loading preview

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

✓L∃∀N

Tagspartly kernel-verified

Lemma Q3.1 (exact replica budget; the mutual-information chain rule). Let X,Y,L be random variables on finite nonempty alphabets, let Z=(X,Y), write p(z)=\Pr(Z=z) for its law, and put

M=I(X;Y\mid L),\qquad B=I(L;X\mid Y)+I(L;Y\mid X). \qquad \text{(Q3.1)}

For every z of positive probability let r_z(i)=\Pr(L=i\mid Z=z). At a zero-probability cell choose any probability vector r_z; its choice affects no weighted sum. Define L_1,L_2 by

\Pr(Z=z,L_1=i,L_2=j)=p(z)r_z(i)r_z(j). \qquad \text{(Q3.2)}

The two labels are conditionally independent given Z, and each (Z,L_k) has the law of (Z,L). Define

\begin{aligned} K&=I(L_2;X\mid L_1)+I(L_2;Y\mid L_1),\\ C&=I(L_1;L_2\mid X)+I(L_1;L_2\mid Y),\\ N&=I(X;Y\mid L_1,L_2). \end{aligned} \qquad \text{(Q3.3)}

Then K=2M+B-C-2N, and hence K\le2M+B.

Lean code for Theorem7.1.1●5 theorems

theoremdefined in NaturalLatents/General/Replica.lean

complete

theorem NaturalLatents.General.replica_budget {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) :
  NaturalLatents.General.replicaBudget L ≤
    2 * NaturalLatents.General.mediation L +
      NaturalLatents.General.redundancy L

theorem NaturalLatents.General.replica_budget
  {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) :
  NaturalLatents.General.replicaBudget L ≤
    2 *
        NaturalLatents.General.mediation
          L +
      NaturalLatents.General.redundancy L

The replica budget of a latent is at most `2 * mediation L + redundancy L`, in nats.

theoremdefined in NaturalLatents/General/Replica.lean

complete

theorem NaturalLatents.General.replica_total_chain_bound.{u_1, u_2, u_3, u_4,
    u_5}
  {Ω : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4}
  {D : Type u_5} [Fintype Ω] [Fintype A] [Fintype B] [Fintype C]
  [Fintype D] [DecidableEq A] [DecidableEq B] [DecidableEq C]
  [DecidableEq D] {q : Ω → ℝ} (hq : stoch_to_det.IsPMF q) (a : Ω → A)
  (b : Ω → B) (x : Ω → C) (y : Ω → D) :
  stoch_to_det.condMI b x a q + stoch_to_det.condMI b y a q ≤
    2 * stoch_to_det.condMI x y a q +
        (stoch_to_det.condMI b x y q + stoch_to_det.condMI b y x q) +
      2 * stoch_to_det.condMI a b (fun w => (x w, y w)) q

theorem NaturalLatents.General.replica_total_chain_bound.{u_1,
    u_2, u_3, u_4, u_5}
  {Ω : Type u_1} {A : Type u_2}
  {B : Type u_3} {C : Type u_4}
  {D : Type u_5} [Fintype Ω] [Fintype A]
  [Fintype B] [Fintype C] [Fintype D]
  [DecidableEq A] [DecidableEq B]
  [DecidableEq C] [DecidableEq D]
  {q : Ω → ℝ} (hq : stoch_to_det.IsPMF q)
  (a : Ω → A) (b : Ω → B) (x : Ω → C)
  (y : Ω → D) :
  stoch_to_det.condMI b x a q +
      stoch_to_det.condMI b y a q ≤
    2 * stoch_to_det.condMI x y a q +
        (stoch_to_det.condMI b x y q +
          stoch_to_det.condMI b y x q) +
      2 *
        stoch_to_det.condMI a b
          (fun w => (x w, y w)) q

The total two-coordinate budget, before applying the replica Markov law.

theoremdefined in NaturalLatents/General/Replica.lean

complete

theorem NaturalLatents.General.replica_replica_markov {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) :
  stoch_to_det.condMI (fun u => u.1) (fun u => u.2.1) (fun u => u.2.2)
      (NaturalLatents.General.replicaJoint L) =
    0

theorem NaturalLatents.General.replica_replica_markov
  {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) :
  stoch_to_det.condMI (fun u => u.1)
      (fun u => u.2.1) (fun u => u.2.2)
      (NaturalLatents.General.replicaJoint
        L) =
    0

theoremdefined in NaturalLatents/General/Replica.lean

complete

theorem NaturalLatents.General.replica_push_first {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) :
  stoch_to_det.push (fun u => (u.1, u.2.2))
      (NaturalLatents.General.replicaJoint L) =
    L.joint

theorem NaturalLatents.General.replica_push_first
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p) :
  stoch_to_det.push
      (fun u => (u.1, u.2.2))
      (NaturalLatents.General.replicaJoint
        L) =
    L.joint

theoremdefined in NaturalLatents/General/Replica.lean

complete

theorem NaturalLatents.General.replica_push_second {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y} (L : stoch_to_det.Latent p) :
  stoch_to_det.push Prod.snd (NaturalLatents.General.replicaJoint L) =
    L.joint

theorem NaturalLatents.General.replica_push_second
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {p : NaturalLatents.General.Law X Y}
  (L : stoch_to_det.Latent p) :
  stoch_to_det.push Prod.snd
      (NaturalLatents.General.replicaJoint
        L) =
    L.joint

Proof for Theorem 7.1.1

uses 0

Lean proves: K\le2M+B, I(L_1;L_2\mid Z)=0, equality of each replica source-label marginal with the original latent joint law, and the general two-coordinate chain-rule bound I(b;x\mid a)+I(b;y\mid a)\le2I(x;y\mid a)+I(b;x\mid y)+I(b;y\mid x)+2I(a;b\mid x,y) in bits (replica_total_chain_bound).

Expand the mutual information chain rule in two orders on both coordinates, use replica conditional independence, and discard the nonnegative remainders. See the page section.

Lean: NaturalLatents.General.replica_budget (NaturalLatents/General/Replica.lean) states only the inequality K\le2M+B, for every finite latent of a probability law; Lean defines neither C nor N and does not state the identity K=2M+B-C-2N. The replica law (Q3.2) is the probability law replicaJoint, and K, in nats, is replicaBudget, both NaturalLatents.General.* in NaturalLatents/General/Definitions.lean; there the posterior at a zero-probability cell is the zero vector rather than a probability vector, which changes no weighted sum. The proof in NaturalLatents/General/Replica.lean combines a two-coordinate chain-rule inequality (replica_total_chain_bound, stated for the bit-valued upstream conditional mutual informations and converted by nats in the proof of the natural-log budget) with the conditional independence of the two labels given Z (replica_replica_markov) and the replica marginal laws (replica_push_first, replica_push_second), dropping the nonnegative remainders as it goes instead of carrying them to an identity.