InformationTheory

InformationTheory.Shannon.MIChainRule

source

Imports 5

Mutual information chain rule (n-variable) and i.i.d. corollary #

MeasurableEquiv invariance, the n-variable chain rule, additivity under product distributions, and the entropy-MI bridge identity.

Main statements #

mutualInfo invariance under MeasurableEquiv reshape #

theorem

InformationTheory.Shannon.mutualInfo_map_left_measurableEquiv

source
{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {X' : Type u_4} [MeasurableSpace X'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Xs : Ω → X) (Yo : Ω → Y) (hXs : Measurable Xs) (hYo : Measurable Yo) (e : X ≃ᵐ X') :
mutualInfo μ (fun (ω : Ω) => e (Xs ω)) Yo = mutualInfo μ Xs Yo

Mutual information is invariant under a MeasurableEquiv reshape of the left random variable: I(e ∘ X; Y) = I(X; Y). Reduces to klDiv_map_measurableEquiv applied to the product equivalence e × id.

Used by

    n-variable chain rule #

    theorem

    InformationTheory.Shannon.mutualInfo_chain_rule_fin

    source
    {Ω : Type u_1} [MeasurableSpace Ω] {Y : Type u_3} [MeasurableSpace Y] {α : Type u_4} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Nonempty α] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Y] [Nonempty Y] (Xs : Fin n → Ω → α) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (Yo : Ω → Y) (hYo : Measurable Yo) :
    mutualInfo μ (fun (ω : Ω) (i : Fin n) => Xs i ω) Yo = ∑ i : Fin n, condMutualInfo μ (Xs i) Yo fun (ω : Ω) (j : Fin ↑i) => Xs ⟨↑j, ⋯⟩ ω

    n-variable chain rule for mutual information: I(X_0, …, X_{n-1}; Y) = ∑ i, I(X_i; Y | (X_0, …, X_{i-1})).

    Induction on n. base n=0: LHS = mutualInfo of a constant Fin 0 → α-valued RV, which is independent of anything ⇒ 0; RHS is the empty sum. step n+1: split via MeasurableEquiv.piFinSuccAbove (Fin.last n) so that Fin (n+1) → α ≃ᵐ α × (Fin n → α), then prodComm so we land on (prefix, last), apply mutualInfo_map_left_measurableEquiv, then the 2-variable mutualInfo_chain_rule with Zc := prefix, Xs_arg := last, then IH on the Fin n prefix, then Fin.sum_univ_castSucc.

    Used by

      i.i.d. corollary #

      theorem

      InformationTheory.Shannon.klDiv_prod_eq_add

      source
      {α' : Type u_6} {β' : Type u_7} [MeasurableSpace α'] [MeasurableSpace β'] (μ₁ μ₂ : MeasureTheory.Measure α') [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (ν₁ ν₂ : MeasureTheory.Measure β') [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₂] :
      klDiv (μ₁.prod ν₁) (μ₂.prod ν₂) = klDiv μ₁ μ₂ + klDiv ν₁ ν₂

      KL divergence of product measures is additive: if both μ₁, μ₂ are probability measures on α and ν₁, ν₂ are finite measures on β, then klDiv (μ₁.prod ν₁) (μ₂.prod ν₂) = klDiv μ₁ μ₂ + klDiv ν₁ ν₂. Derived from klDiv_compProd_eq_add (Mathlib) with constant kernels + klDiv_prod_const_left.

      Used by
        theorem

        InformationTheory.Shannon.klDiv_pi_eq_sum

        source
        {n : ℕ} {α' : Fin n → Type u_6} [(i : Fin n) → MeasurableSpace (α' i)] (μs νs : (i : Fin n) → MeasureTheory.Measure (α' i)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μs i)] [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (νs i)] :
        klDiv (MeasureTheory.Measure.pi μs) (MeasureTheory.Measure.pi νs) = ∑ i : Fin n, klDiv (μs i) (νs i)

        KL divergence of Measure.pi measures is additive over the index set: klDiv (Measure.pi μs) (Measure.pi νs) = ∑ i, klDiv (μs i) (νs i).

        Proven by induction on n using measurePreserving_piFinSuccAbove (to split Measure.pi of length n+1 into μ_{last} × Measure.pi prefix) + klDiv_map_measurableEquiv + klDiv_prod_eq_add + Fin.sum_univ_castSucc.

        Used by
          theorem

          InformationTheory.Shannon.mutualInfo_pi_eq_sum

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_iid_joint : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => (Xs i ω, Ys i ω)) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (fun (ω : Ω) => (Xs i ω, Ys i ω)) μ) (h_iid_X : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => Xs i ω) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (Xs i) μ) (h_iid_Y : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => Ys i ω) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (Ys i) μ) :
          (mutualInfo μ (fun (ω : Ω) (i : Fin n) => Xs i ω) fun (ω : Ω) (i : Fin n) => Ys i ω) = ∑ i : Fin n, mutualInfo μ (Xs i) (Ys i)

          MI additivity under product joint distribution: if the joint μ.map (fun ω i ↦ (X_i ω, Y_i ω)) factors as the product Measure.pi (i ↦ μ.map (X_i, Y_i)) and the marginals factor similarly, then I(X^n; Y^n) = ∑ I(X_i; Y_i).

          Strategy: reshape via MeasurableEquiv.arrowProdEquivProdArrow so that both joint and product-of-marginals (defining mutualInfo) become Measure.pi-shaped, then apply klDiv_pi_eq_sum to get the sum.

          Used by
            theorem

            InformationTheory.Shannon.mutualInfo_iid_eq_nsmul

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] {n : ℕ} (hn : 0 < n) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_iid_joint : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => (Xs i ω, Ys i ω)) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (fun (ω : Ω) => (Xs i ω, Ys i ω)) μ) (h_iid_X : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => Xs i ω) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (Xs i) μ) (h_iid_Y : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => Ys i ω) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (Ys i) μ) (h_copy : ∀ (i : Fin n), MeasureTheory.Measure.map (fun (ω : Ω) => (Xs i ω, Ys i ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Xs ⟨0, hn⟩ ω, Ys ⟨0, hn⟩ ω)) μ) (h_copy_X : ∀ (i : Fin n), MeasureTheory.Measure.map (Xs i) μ = MeasureTheory.Measure.map (Xs ⟨0, hn⟩) μ) (h_copy_Y : ∀ (i : Fin n), MeasureTheory.Measure.map (Ys i) μ = MeasureTheory.Measure.map (Ys ⟨0, hn⟩) μ) :
            (mutualInfo μ (fun (ω : Ω) (i : Fin n) => Xs i ω) fun (ω : Ω) (i : Fin n) => Ys i ω) = n • mutualInfo μ (Xs ⟨0, hn⟩) (Ys ⟨0, hn⟩)

            i.i.d. corollary: all (X_i, Y_i) jointly i.i.d. with common law implies I(X^n; Y^n) = n · I(X_0; Y_0).

            Used by

              Entropy ↔ MI three-term bridge #

              For a joint probability measure on a finite-alphabet product space α × β, the standard identity I(X; Y) = H(X) + H(Y) − H(X, Y) connects the klDiv-based mutualInfo to the Shannon-entropy entropy. This rewrites the joint-AEP exponent H(X, Y) − H(X) − H(Y) as −I(p; W).

              theorem

              InformationTheory.Shannon.mutualInfo_eq_entropy_add_entropy_sub_jointEntropy

              source
              {α : Type u_4} {β : Type u_5} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (joint : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure joint] :
              (mutualInfo joint Prod.fst Prod.snd).toReal = entropy joint Prod.fst + entropy joint Prod.snd - entropy joint id

              The mutual-information ↔ entropy three-term identity (joint-distribution level). For any probability measure joint on a finite-alphabet product α × β, the klDiv-based mutual information of its coordinates equals the standard three-term form H(X) + H(Y) − H(X, Y), where H(X, Y) := entropy joint id is the joint entropy on α × β.

              Strategy: mutualInfo_comm to put Prod.snd first, then Bridge mutualInfo_eq_entropy_sub_condEntropy to convert MI to entropy minus conditional entropy; finally entropy_pair_eq_entropy_add_condEntropy applied to the identity pair (z.1, z.2) = z to expand the joint entropy.

              Used by