InformationTheory

InformationTheory.Shannon.RateDistortion.ConverseNLetter

source

Imports 11

Rate-distortion converse (n-letter form) #

The converse for an n-letter block lossy code with an i.i.d. source:

∀ block lossy code (encoder, decoder),  i.i.d. source P_X^n,
  c.expectedBlockDistortion P_X d ≤ D ⟹
    (1/n) · (rateDistortionFunction d P_X D).toReal ≤ (1/n) · Real.log M.

Main statements #

Implementation notes #

The single-letterized form composes per-letter feasibility R(Dᵢ) ≤ I(Xᵢ; X̂ᵢ), mutual-information superadditivity ∑ I(Xᵢ; X̂ᵢ) ≤ I(Xⁿ; X̂ⁿ), an n-way Jensen bound built by induction from the binary convexity rateDistortionFunction_convexOn, the block-distortion identity expectedBlockDistortion = (1/n) ∑ Dᵢ (via the i.i.d. product law), and antitonicity. The superadditivity step is built in-project from entropy_pi_eq_sum_of_indep, the gateway condEntropy_pi_le_sum_condEntropy_per_letter, and the MI↔entropy bridge mutualInfo_eq_entropy_sub_condEntropy; the independence of the source is a genuine precondition (a counterexample arises at n = 2, X₁ = X₂).

Block-level n-letter converse #

theorem

InformationTheory.Shannon.rate_distortion_converse_n_letter_block

source
{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {M n : ℕ} [NeZero M] (c : LossyCode M n α β) (hencoder : Measurable c.encoder) (hdecoder : Measurable c.decoder) (d : DistortionFn α β) (P_X : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P_X] {D : ℝ} (hD : c.expectedBlockDistortion P_X d ≤ D) (hMI_W_finite : (mutualInfo (MeasureTheory.Measure.pi fun (x : Fin n) => P_X) id fun (x : Fin n → α) => c.encoder x) ≠ ⊤) :
(rateDistortionFunction (fun (x : Fin n → α) (y : Fin n → β) => blockDistortion d n x y) (MeasureTheory.Measure.pi fun (x : Fin n) => P_X) D).toReal ≤ Real.log ↑(Fintype.card (Fin M))

Rate-distortion theorem (converse, n-letter block form).

For any block lossy code c : LossyCode M n α β (with encoder : (Fin n → α) → Fin M, decoder : Fin M → (Fin n → β)) and i.i.d. source P_X on α, if c.expectedBlockDistortion P_X d ≤ D then the block-level rate-distortion function satisfies

(rateDistortionFunction (fun x y => blockDistortion d n x y)
  (Measure.pi (fun _ => P_X)) D).toReal ≤ Real.log M.

This is a direct (α := Fin n → α, β := Fin n → β, M := Fin M) instantiation of rate_distortion_converse_single_shot_specified with the block distortion as the distortion measure.

Used by

    Block-level MI ≤ log M #

    theorem

    InformationTheory.Shannon.mutualInfo_block_le_log_card

    source
    {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {M n : ℕ} [NeZero M] (c : LossyCode M n α β) (hencoder : Measurable c.encoder) (hdecoder : Measurable c.decoder) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs_block : Ω → Fin n → α) (hXs_block : Measurable Xs_block) (hMI_W_finite : (mutualInfo μ Xs_block fun (ω : Ω) => c.encoder (Xs_block ω)) ≠ ⊤) :
    (mutualInfo μ Xs_block fun (ω : Ω) => c.decoder (c.encoder (Xs_block ω))).toReal ≤ Real.log ↑(Fintype.card (Fin M))

    Block-level MI ≤ log M. For any block lossy code c : LossyCode M n α β and i.i.d. source μ on Ω with X^n-projection Xs_block : Ω → (Fin n → α), the mutual information between X^n and the reconstruction X̂^n := decoder ∘ encoder ∘ X^n satisfies

    (mutualInfo μ X^n X̂^n).toReal ≤ Real.log (Fintype.card (Fin M)).

    Same DPI + max-entropy chain as rate_distortion_converse_single_shot's steps 1-3, extracted as a standalone lemma.

    Used by

      Single-letterized form #

      theorem

      InformationTheory.Shannon.rateDistortionFunction_le_mutualInfo_perLetter

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {α' : Type u_4} {β' : Type u_5} [MeasurableSpace α'] [MeasurableSpace β'] (μ : MeasureTheory.Measure Ω) (X : Ω → α') (Xh : Ω → β') (hX : Measurable X) (hXh : Measurable Xh) (d : α' → β' → ℝ) (hd : Measurable fun (p : α' × β') => d p.1 p.2) :
      rateDistortionFunction d (MeasureTheory.Measure.map X μ) (∫ (ω : Ω), d (X ω) (Xh ω) ∂μ) ≤ mutualInfo μ X Xh

      Per-letter feasible feed: for fixed i, the joint νᵢ := μ.map (Xs i, X̂s i) is feasible for the per-letter R(Dᵢ) at threshold Dᵢ := ∫ d(Xs i ω) (X̂s i ω) ∂μ, so R(Dᵢ) ≤ klDiv νᵢ ((νᵢ.map fst).prod (νᵢ.map snd)) = mutualInfo μ (Xs i) (X̂s i).

      Used by

        n-way Jensen for R(D) from binary convexity #

        MI superadditivity for an independent source #

        theorem

        InformationTheory.Shannon.condEntropy_pi_le_sum_condEntropy_per_letter

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_5} [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (Xhs : Fin n → Ω → β) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hXhs : ∀ (i : Fin n), Measurable (Xhs i)) :
        (MeasureFano.condEntropy μ (fun (ω : Ω) (j : Fin n) => Xs j ω) fun (ω : Ω) (j : Fin n) => Xhs j ω) ≤ ∑ i : Fin n, MeasureFano.condEntropy μ (Xs i) (Xhs i)

        Conditional-entropy subadditivity on the block: for any Xs : Fin n → Ω → α and any reconstruction family Xhs : Fin n → Ω → β,

        H(X^n | X̂^n) ≤ ∑ i, H(X_i | X̂_i).

        Encoder/decoder-agnostic; no independence needed.

        @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.mutualInfo_superadditive_of_indep

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_5} [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (Xhs : Fin n → Ω → β) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hXhs : ∀ (i : Fin n), Measurable (Xhs i)) (hindep : ProbabilityTheory.iIndepFun (fun (i : Fin n) => Xs i) μ) :
          ∑ i : Fin n, (mutualInfo μ (Xs i) (Xhs i)).toReal ≤ (mutualInfo μ (fun (ω : Ω) (j : Fin n) => Xs j ω) fun (ω : Ω) (j : Fin n) => Xhs j ω).toReal

          Mutual-information superadditivity for an independent source: for Xs : Fin n → Ω → α mutually independent and any reconstruction family Xhs : Fin n → Ω → β,

          ∑ i, (I(X_i; X̂_i)).toReal ≤ (I(X^n; X̂^n)).toReal.

          The independence hypothesis hindep is a genuine precondition: it is consumed inside entropy_pi_eq_sum_of_indep to collapse H(X^n) to ∑ H(Xᵢ), and dropping it makes the claim false (X₁ = X₂ ⇒ ∑ I > I_joint).

          @audit:ok

          Used by
            theorem

            InformationTheory.Shannon.rate_distortion_converse_n_letter_singleLetter

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSingletonClass β] {M n : ℕ} [NeZero M] (hn : 0 < n) (c : LossyCode M n α β) (hencoder : Measurable c.encoder) (hdecoder : Measurable c.decoder) (d : DistortionFn α β) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hindep : ProbabilityTheory.iIndepFun (fun (i : Fin n) => Xs i) μ) (P_X : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P_X] (hXs_law : ∀ (i : Fin n), MeasureTheory.Measure.map (Xs i) μ = P_X) (h_MI_block_finite : (mutualInfo μ (fun (ω : Ω) (i : Fin n) => Xs i ω) fun (ω : Ω) => c.encoder fun (j : Fin n) => Xs j ω) ≠ ⊤) (h_MI_perletter_finite : ∀ (i : Fin n), (mutualInfo μ (Xs i) fun (ω : Ω) => c.decoder (c.encoder fun (j : Fin n) => Xs j ω) i) ≠ ⊤) {D : ℝ} (hD : c.expectedBlockDistortion P_X d ≤ D) :
            (rateDistortionFunction (fun (a : α) (b : β) => ↑(d a b)) P_X D).toReal ≤ 1 / ↑n * Real.log ↑(Fintype.card (Fin M))

            Rate-distortion theorem (converse, n-letter single-letterized form).

            Given a block lossy code, an i.i.d. source P_X, and a probability space (Ω, μ) where Xs i : Ω → α are i.i.d. copies of P_X (mutual independence hindep + identical marginals hXs_law) and X̂ᵢ := (decoder ∘ encoder ∘ X^n)ᵢ, the single-letter rate-distortion function satisfies

            (rateDistortionFunction (d as ℝ-valued) P_X D).toReal ≤ (1/n) · Real.log M.

            The independence and i.i.d. preconditions (hindep + hXs_law) are genuine: the conclusion is false without them (n = 2, X₁ = X₂ gives R = log 2 > (1/2)log 2). The finiteness preconditions h_MI_block_finite / h_MI_perletter_finite are needed for the ENNReal.toReal monotonicity steps.

            @audit:ok

            Used by