Natural latents: a bound below seven

3.1. 4. The ledger🔗

Units and conventions are those of section 0 of the contact page: entropies and informations are in nats, conditional sums range over positive-probability conditioning events, and D_p(f)=I(X;Y\mid f(Z))+H(f(Z)\mid X)+H(f(Z)\mid Y) is the deterministic score of a map f, so that T(p)=\min_fD_p(f) as in (D3). The random map F is the one of step 2 of the route, not the cap F of the cap page; Q=F(Z), U, A and \Delta below are local, and Q is not the reference of the race page.

Theorem3.1.1

uses 0

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 L4.1 (calibrated finite-map averaging and the ledger). Let X,Y,L be finite random variables, Z=(X,Y), and let p be the law of Z. Let F be a finite-valued random deterministic map from \mathrm{supp}\,p to the label set of L, independent of Z. Suppose \Pr(F(z)=i)=r_z(i)=\Pr(L=i\mid Z=z) for every positive source atom z. Put Q=F(Z), M=I(X;Y\mid L), B=I(L;X\mid Y)+I(L;Y\mid X), and

h=H(Q\mid X,F)+H(Q\mid Y,F),\qquad \Delta=I(F;X\mid Q)+I(F;Y\mid Q). \qquad \text{(L1)}

Then \Delta\ge0, and

\mathbb E_F D_p(F) =M-\frac B2+\frac{3h}{2}-\frac{\Delta}{2}, \qquad T(p)\le M-\frac B2+\frac{3h}{2}. \qquad \text{(L2)}

Here D_p(f) is the deterministic score of f(Z), as in section 0. No positivity, contact, optimality or distinct-component hypothesis is needed. Fix a label i_0 and extend every map by i_0 outside \mathrm{supp}\,p. This does not change Q, calibration, h, \Delta or any fixed-map score, and turns F into a random complete map, as used below.

Lean code for Theorem3.1.1●6 theorems

theoremdefined in NaturalLatents/General/Ledger.lean

complete

theorem NaturalLatents.General.T_le_ledger {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)
  (F : NaturalLatents.General.CalibratedSeededFamily L) :
  NaturalLatents.General.TNat p ≤
    NaturalLatents.General.mediation L -
        NaturalLatents.General.redundancy L / 2 +
      3 * NaturalLatents.General.seedEntropy F / 2

theorem NaturalLatents.General.T_le_ledger
  {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)
  (F :
    NaturalLatents.General.CalibratedSeededFamily
      L) :
  NaturalLatents.General.TNat p ≤
    NaturalLatents.General.mediation L -
        NaturalLatents.General.redundancy
            L /
          2 +
      3 *
          NaturalLatents.General.seedEntropy
            F /
        2

The ledger inequality, in nats: `TNat p ≤ mediation L - redundancy L / 2 + 3 seedEntropy F / 2` for a calibrated seeded family `F`
of a latent `L` of a probability law `p`.

theoremdefined in NaturalLatents/General/Ledger.lean

complete

theorem NaturalLatents.General.ledger_calibrated_graph {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)
  (F : NaturalLatents.General.CalibratedSeededFamily L) :
  stoch_to_det.push (fun w => (w.1 w.2, w.2))
      (NaturalLatents.General.seedSourceJoint F) =
    L.joint

theorem NaturalLatents.General.ledger_calibrated_graph
  {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)
  (F :
    NaturalLatents.General.CalibratedSeededFamily
      L) :
  stoch_to_det.push
      (fun w => (w.1 w.2, w.2))
      (NaturalLatents.General.seedSourceJoint
        F) =
    L.joint

theoremdefined in NaturalLatents/General/Ledger.lean

complete

theorem NaturalLatents.General.ledger_detScore_coordinate_identity.{u_1}
  {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {γ : Type u_1} [Fintype γ] [DecidableEq γ]
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p)
  (A : X × Y → γ) :
  stoch_to_det.detScore p A =
    stoch_to_det.Ixy p +
        3 / 2 *
          (stoch_to_det.condH A Prod.fst p +
            stoch_to_det.condH A Prod.snd p) -
      1 / 2 *
        (stoch_to_det.MI A Prod.fst p + stoch_to_det.MI A Prod.snd p)

theorem NaturalLatents.General.ledger_detScore_coordinate_identity.{u_1}
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {γ : Type u_1} [Fintype γ]
  [DecidableEq γ]
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p)
  (A : X × Y → γ) :
  stoch_to_det.detScore p A =
    stoch_to_det.Ixy p +
        3 / 2 *
          (stoch_to_det.condH A Prod.fst
              p +
            stoch_to_det.condH A Prod.snd
              p) -
      1 / 2 *
        (stoch_to_det.MI A Prod.fst p +
          stoch_to_det.MI A Prod.snd p)

theoremdefined in NaturalLatents/General/Ledger.lean

complete

theorem NaturalLatents.General.ledger_information_balance {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.mediation L -
      NaturalLatents.General.redundancy L / 2 =
    NaturalLatents.General.nats
      (stoch_to_det.Ixy p -
        (stoch_to_det.MI (fun v => v.1) (fun v => v.2.1) L.joint +
            stoch_to_det.MI (fun v => v.1) (fun v => v.2.2) L.joint) /
          2)

theorem NaturalLatents.General.ledger_information_balance
  {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.mediation L -
      NaturalLatents.General.redundancy
          L /
        2 =
    NaturalLatents.General.nats
      (stoch_to_det.Ixy p -
        (stoch_to_det.MI (fun v => v.1)
              (fun v => v.2.1) L.joint +
            stoch_to_det.MI (fun v => v.1)
              (fun v => v.2.2) L.joint) /
          2)

theoremdefined in NaturalLatents/General/Ledger.lean

complete

theorem NaturalLatents.General.ledger_average_MI_lower {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)
  (F : NaturalLatents.General.CalibratedSeededFamily L) {Γ : Type}
  [Fintype Γ] [DecidableEq Γ] (g : X × Y → Γ) :
  stoch_to_det.MI Prod.fst (fun w => g w.2) L.joint ≤
    ∑ A, F.seedLaw A * stoch_to_det.MI A g p

theorem NaturalLatents.General.ledger_average_MI_lower
  {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)
  (F :
    NaturalLatents.General.CalibratedSeededFamily
      L)
  {Γ : Type} [Fintype Γ] [DecidableEq Γ]
  (g : X × Y → Γ) :
  stoch_to_det.MI Prod.fst
      (fun w => g w.2) L.joint ≤
    ∑ A,
      F.seedLaw A * stoch_to_det.MI A g p

theoremdefined in NaturalLatents/Upstream/Functionals.lean

complete

theorem stoch_to_det.T_le_score.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (V : stoch_to_det.Latent p) (hV : V.IsDet) :
  stoch_to_det.T p ≤ V.score

theorem stoch_to_det.T_le_score.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (V : stoch_to_det.Latent p)
  (hV : V.IsDet) :
  stoch_to_det.T p ≤ V.score

The score of any single deterministic latent bounds `T` from above. This is
the final bound uses `T`: `exists_good_seed` exhibits one suitable seed.

Proof for Theorem 3.1.1

uses 0

Lean proves: T(p)\le M-B/2+3h/2 for a CalibratedSeededFamily, with the coordinate score and information-balance identities and the averaged mutual-information lower bound used to obtain it.

Use calibration and independence to identify the joint law, expand the entropy chain rules, and choose a map below the finite average. See the page section.

Lean: NaturalLatents.General.T_le_ledger (NaturalLatents/General/Ledger.lean) states only the inequality T(p)\le M-B/2+3h/2; Lean does not define \Delta or state the identity for \mathbb E_FD_p(F). The random map is a CalibratedSeededFamily L (NaturalLatents/General/Definitions.lean): a probability law on complete maps from all of X\times Y to the labels, calibrated at every cell of the support, whose independence from Z is the product law seedSourceJoint; h is seedEntropy in the same file, the form (L7). The steps are in NaturalLatents/General/Ledger.lean. (L5) is ledger_calibrated_graph. The final identity of (L4), in bits, is ledger_detScore_coordinate_identity; conversion by nats, through detScoreNat, gives its page form. The final identity of (L3) with U=L is ledger_information_balance, stated in nats through nats. ledger_average_MI_lower is bit-valued and states I(L;g(Z))\le\sum_f\Pr(F=f)I(f(Z);g(Z)) for every finite function g of the cell; applying it to each coordinate and converting by nats gives the lower bounds used from (L6), in place of the identities with \Delta. The proof averages T(p)\le D_p(f), from stoch_to_det.T_le_score (NaturalLatents/Upstream/Functionals.lean), over the seed.