InformationTheory

InformationTheory.Shannon.CondEntropyMemoryless

source

Imports 4

Conditional entropy on Fin n under strong memoryless DMC #

The Cover-Thomas route to the per-letter MI bound goes via entropy subadditivity, avoiding a false-statement h_yother_zero hypothesis that a hypothesis-form converse would require. The chain:

I(X^n; Y^n) = H(Y^n) - H(Y^n | X^n)
            ≤ ∑ H(Y_i) - H(Y^n | X^n)         -- subadditivity (encoder-agnostic)
            = ∑ H(Y_i) - ∑ H(Y_i | X_i)       -- strong memoryless
            = ∑ I(X_i; Y_i)

This file establishes the four building blocks:

The central theorem mutualInfo_le_sum_per_letter_of_memoryless_strong is then the direct combination: (I(X^n; Y^n)).toReal ≤ ∑ (I(X_i; Y_i)).toReal.

The two Markov axioms of IsMemorylessChannelStrong are taken as hypotheses (not as a single structure) to keep this file an upstream building block of InformationTheory/Shannon/ChannelCoding/ConverseMemorylessMarkov.lean, which defines that structure and supplies its two fields when invoking the theorem here.

Building block 1 — entropy subadditivity (encoder-agnostic) #

theorem

InformationTheory.Shannon.entropy_pi_le_sum_entropy

source
{Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {β : Type u_2} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Ys : Fin n → Ω → β) (hYs : ∀ (i : Fin n), Measurable (Ys i)) :
jointEntropy μ Ys ≤ ∑ i : Fin n, entropy μ (Ys i)

Entropy is subadditive on Fin n: H(Y^n) ≤ ∑ H(Y_i).

This is encoder-agnostic — holds for any family Ys : Fin n → Ω → β without any memoryless or independence assumption. Cover-Thomas.

Proof: combine the n-variable chain rule H(Y^n) = ∑ H(Y_i | Y^{<i}) (jointEntropy_chain_rule) with H(Y_i | Y^{<i}) ≤ H(Y_i) (entropy_ge_condEntropy, conditioning reduces entropy), summed over i.

Used by

    Building block 2 — conditional joint entropy chain rule #

    theorem

    InformationTheory.Shannon.condEntropy_pi_chain_rule_aux

    source
    {Ω : Type u_1} [MeasurableSpace Ω] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {n : ℕ} {χ : Type u_4} [Fintype χ] [Nonempty χ] [MeasurableSpace χ] [MeasurableSingletonClass χ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → χ) (Ys : Fin n → Ω → β) (hXs : Measurable Xs) (hYs : ∀ (i : Fin n), Measurable (Ys i)) :
    MeasureFano.condEntropy μ (fun (ω : Ω) (j : Fin n) => Ys j ω) Xs = ∑ i : Fin n, MeasureFano.condEntropy μ (Ys i) fun (ω : Ω) => (Xs ω, fun (j : Fin ↑i) => Ys ⟨↑j, ⋯⟩ ω)

    The conditional joint entropy chain rule on Fin n (generalized over an arbitrary conditioner type χ): H(Y^n | X) = ∑ i, H(Y_i | X, Y^{<i}).

    Generalizing the conditioner type allows the inductive step to apply the IH to the same Xs (whose type does not depend on n).

    Proof: induction on n. Base case n = 0: both sides reduce to 0 (the joint Y^0 has a singleton codomain, so H(Y^0 | X) = 0, and the sum is empty). Step n+1: split Y^{n+1} as (Y^n_prefix, Y_n), apply the 2-var conditional chain rule, apply IH to the prefix, and reassemble via Fin.sum_univ_castSucc.

    Used by
      theorem

      InformationTheory.Shannon.condEntropy_pi_chain_rule

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → Fin n → α) (Ys : Fin n → Ω → β) (hXs : Measurable Xs) (hYs : ∀ (i : Fin n), Measurable (Ys i)) :
      MeasureFano.condEntropy μ (fun (ω : Ω) (j : Fin n) => Ys j ω) Xs = ∑ i : Fin n, MeasureFano.condEntropy μ (Ys i) fun (ω : Ω) => (Xs ω, fun (j : Fin ↑i) => Ys ⟨↑j, ⋯⟩ ω)

      The conditional joint entropy chain rule on Fin n (specialization of condEntropy_pi_chain_rule_aux with conditioner Xs : Ω → (Fin n → α)). H(Y^n | X^n) = ∑ i, H(Y_i | X^n, Y^{<i}). Building Block 2 of Cover-Thomas.

      Used by

        Building block 3 — Markov drop of irrelevant conditioner #

        theorem

        InformationTheory.Shannon.condEntropy_drop_irrelevant_of_markov

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] {γ : Type u_4} [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] [StandardBorelSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Yo : Ω → β) (Zc : Ω → α) (Wc : Ω → γ) (hYo : Measurable Yo) (hZc : Measurable Zc) (hWc : Measurable Wc) (hmarkov : IsMarkovChain μ Yo Zc Wc) :
        (MeasureFano.condEntropy μ Yo fun (ω : Ω) => (Zc ω, Wc ω)) = MeasureFano.condEntropy μ Yo Zc

        The Markov-drop property for conditional entropy: under Markov chain Yo → Zc → Wc, H(Yo | Zc, Wc) = H(Yo | Zc).

        Direct consequence of condMutualInfo_eq_zero_of_markov via condMutualInfo_eq_condEntropy_sub_condEntropy: the Markov hypothesis forces I(Yo; Wc | Zc) = 0, and the bridge expresses this as the desired equality.

        Used by

          Building block 4 — H(Y^n | X^n) = ∑ H(Y_i | X_i) from strong memoryless #

          theorem

          InformationTheory.Shannon.isMarkovChain_swap

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [MeasurableSpace X'] [MeasurableSpace Y'] [MeasurableSpace Z'] [StandardBorelSpace X'] [Nonempty X'] [StandardBorelSpace Y'] [Nonempty Y'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X') (Zc : Ω → Z') (Yo : Ω → Y') (hXs : Measurable Xs) (hZc : Measurable Zc) (hYo : Measurable Yo) (hmarkov : IsMarkovChain μ Xs Zc Yo) :
          IsMarkovChain μ Yo Zc Xs

          A Markov chain is symmetric under swapping its endpoints: IsMarkovChain μ Xs Zc Yo ↔ IsMarkovChain μ Yo Zc Xs.

          The γ-form definition μ.map (Z, X, Y) = (μ.map Z) ⊗ₘ (K_X ×ₖ K_Y) is symmetric in X/Y: pushing both sides forward by the measurable equiv Z × (X × Y) ≃ᵐ Z × (Y × X) gives the analogous identity with X/Y swapped.

          • LHS μ.map (Z, X, Y) ↦ μ.map (Z, Y, X) via Measure.map_map.
          • RHS (μ.map Z) ⊗ₘ (K_X ×ₖ K_Y) ↦ (μ.map Z) ⊗ₘ ((K_X ×ₖ K_Y).map Prod.swap) via Measure.compProd_map, then Kernel.prodComm_prod to identify the inner pushforward as K_Y ×ₖ K_X.
          Used by
            theorem

            InformationTheory.Shannon.isMarkovChain_comp_conditioner_right

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {A' : Type u_4} {Z' : Type u_5} {W' : Type u_6} [MeasurableSpace A'] [MeasurableSpace Z'] [MeasurableSpace W'] [StandardBorelSpace A'] [Nonempty A'] [StandardBorelSpace W'] [Nonempty W'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (As : Ω → A') (Zc : Ω → Z') {f : Z' → W'} (hAs : Measurable As) (hZc : Measurable Zc) (hf : Measurable f) :
            IsMarkovChain μ As Zc fun (ω : Ω) => f (Zc ω)

            A Markov chain whose right endpoint is a deterministic function of the conditioner: As → Zc → f ∘ Zc.

            Given the conditioner Zc, the value f (Zc ω) is determined, so As and f ∘ Zc are trivially conditionally independent given Zc. Concretely condDistrib (f ∘ Zc) Zc μ collapses to the deterministic kernel (condDistrib_comp_self), and the joint distribution of (Zc, As, f ∘ Zc) factorizes through the graph map (z, a) ↦ (z, a, f z).

            Used by
              theorem

              InformationTheory.Shannon.kernel_compProd_prodMkRight_eq_prod

              source
              {Z' : Type u_4} {A' : Type u_5} {B' : Type u_6} [MeasurableSpace Z'] [MeasurableSpace A'] [MeasurableSpace B'] (κ : ProbabilityTheory.Kernel Z' A') [ProbabilityTheory.IsSFiniteKernel κ] (Q : ProbabilityTheory.Kernel Z' B') [ProbabilityTheory.IsSFiniteKernel Q] :
              κ.compProd (ProbabilityTheory.Kernel.prodMkRight A' Q) = κ.prod Q
              Used by
                theorem

                InformationTheory.Shannon.isMarkovChain_of_append

                source
                {Ω : Type u_1} [MeasurableSpace Ω] {A' : Type u_4} {Z' : Type u_5} {B' : Type u_6} [MeasurableSpace A'] [MeasurableSpace Z'] [MeasurableSpace B'] [StandardBorelSpace A'] [Nonempty A'] [StandardBorelSpace B'] [Nonempty B'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (As : Ω → A') (Zc : Ω → Z') (Bs : Ω → B') (hAs : Measurable As) (hZc : Measurable Zc) (hBs : Measurable Bs) (Q : ProbabilityTheory.Kernel Z' B') [ProbabilityTheory.IsMarkovKernel Q] (h_app : MeasureTheory.Measure.map (fun (ω : Ω) => ((Zc ω, As ω), Bs ω)) μ = (MeasureTheory.Measure.map (fun (ω : Ω) => (Zc ω, As ω)) μ).compProd (ProbabilityTheory.Kernel.prodMkRight A' Q)) :
                IsMarkovChain μ As Zc Bs

                If the target Bs is generated from the conditioner Zc by a Markov kernel Q that ignores As, then As → Zc → Bs is a Markov chain. This is the stochastic analogue of isMarkovChain_comp_conditioner_right, whose right endpoint is only a deterministic function of the conditioner.

                Used by
                  theorem

                  InformationTheory.Shannon.condEntropy_pi_eq_sum_of_memoryless_strong

                  source
                  {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (μ : 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_per_letter_markov : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) (j : Fin n) => Xs j ω) (Xs i) (Ys i)) (h_outputs_cond_indep : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) (j : { j : Fin n // j ≠ i }) => Ys (↑j) ω) (fun (ω : Ω) (j : Fin n) => Xs j ω) (Ys i)) :
                  (MeasureFano.condEntropy μ (fun (ω : Ω) (j : Fin n) => Ys j ω) fun (ω : Ω) (j : Fin n) => Xs j ω) = ∑ i : Fin n, MeasureFano.condEntropy μ (Ys i) (Xs i)

                  The conditional joint entropy of outputs given inputs under a strong memoryless DMC: H(Y^n | X^n) = ∑ i, H(Y_i | X_i).

                  Combines condEntropy_pi_chain_rule (Building Block 2) with the per-summand collapse H(Y_i | X^n, Y^{<i}) = H(Y_i | X_i). The collapse uses the two Markov axioms (taken as hypotheses, not as IsMemorylessChannelStrong to avoid circular import — the caller in ChannelCoding/ConverseMemorylessMarkov.lean unpacks the structure):

                  • h_outputs_cond_indep (≈ outputs_cond_indep): Y_i ⫫ Y^{<i} | X^n ⇒ can drop Y^{<i} from conditioner.
                  • h_per_letter_markov (≈ per_letter_markov): Y_i ⫫ X^{≠i} | X_i ⇒ can drop X^{≠i} from conditioner.

                  Each collapse is one application of condEntropy_drop_irrelevant_of_markov.

                  Used by

                    Central theorem — Cover-Thomas bound #

                    theorem

                    InformationTheory.Shannon.mutualInfo_le_sum_per_letter_of_memoryless_strong

                    source
                    {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (μ : 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_per_letter_markov : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) (j : Fin n) => Xs j ω) (Xs i) (Ys i)) (h_outputs_cond_indep : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) (j : { j : Fin n // j ≠ i }) => Ys (↑j) ω) (fun (ω : Ω) (j : Fin n) => Xs j ω) (Ys i)) :
                    (mutualInfo μ (fun (ω : Ω) (j : Fin n) => Xs j ω) fun (ω : Ω) (j : Fin n) => Ys j ω).toReal ≤ ∑ i : Fin n, (mutualInfo μ (Xs i) (Ys i)).toReal

                    The per-letter mutual-information bound from a strong memoryless DMC (Cover-Thomas): (I(X^n; Y^n)).toReal ≤ ∑ i, (I(X_i; Y_i)).toReal.

                    The encoder-agnostic Cover-Thomas chain:

                    I(X^n; Y^n) = H(Y^n) - H(Y^n | X^n)
            ≤ ∑ H(Y_i) - H(Y^n | X^n)             -- subadditivity (Block 1)
            = ∑ H(Y_i) - ∑ H(Y_i | X_i)           -- strong memoryless (Block 4)
            = ∑ (H(Y_i) - H(Y_i | X_i))
            = ∑ I(X_i; Y_i)                       -- Bridge

                    This avoids the false-statement h_yother_zero route used in D-2' channel_coding_converse_general_memoryless. The two Markov axioms of IsMemorylessChannelStrong are taken as hypotheses (caller unpacks the structure).

                    Used by