Skip to content

InformationTheory.Shannon.WynerZiv.RateMonotonicity

Imports 3

Wyner–Ziv rate monotonicity and affine plumbing #

Monotonicity of the Wyner–Ziv rate function in the distortion budget, together with the affine building blocks and boundedness facts used by the convexity development in FactorizableRate.lean.

Main statements #

WynerZivConstraint_mono_in_D — the constraint set grows with D.
wynerZivRatePmf_antitone, wynerZivRatePmf_antitone_of_feasible — D ≤ D' ⟹ R_WZ(D') ≤ R_WZ(D), with the BddBelow/non-emptiness side conditions discharged for the feasibility-witness form.
wzMarginalXY_add, wzMarginalXY_smul, wzMarginalXY_convex_combination — affinity of the (X,Y)-marginal in the joint pmf.
wynerZivObjective_image_bddBelow — the objective image is bounded below.

Notation #

U is the auxiliary alphabet (carried as an argument). The variable qf denotes a pair (q, f) : (α × β × U → ℝ) × (U × β → γ) — the joint pmf and the decoder. The first projection of the constraint set lies in the standard simplex, the entry point for both the BddBelow argument and the convex_stdSimplex re-export.

theorem

InformationTheory.Shannon.WynerZivConstraint_mono_in_D

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) {D D' : ℝ} (hD : D ≤ D') :

WynerZivConstraint U P_XY d D ⊆ WynerZivConstraint U P_XY d D'

Constraint set is monotone in D. Increasing the distortion budget can only enlarge the set of feasible (q, f)-pairs: every point feasible at the lower threshold D is also feasible at the higher threshold D'.

Used by

theorem

InformationTheory.Shannon.wynerZivObjective_image_mono_in_D

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) {D D' : ℝ} (hD : D ≤ D') :

(fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D ⊆ (fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D'

Image-of-constraint monotonicity. A direct consequence of WynerZivConstraint_mono_in_D: the objective-image at the smaller threshold is contained in the objective-image at the larger threshold.

Used by

theorem

InformationTheory.Shannon.wynerZivRatePmf_antitone

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) {D D' : ℝ} (hD : D ≤ D') (h_ne : ((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D).Nonempty) (h_bdd : BddBelow ((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D')) :

wynerZivRatePmf U P_XY d D' ≤ wynerZivRatePmf U P_XY d D

The Wyner–Ziv rate function is antitone in D: for D ≤ D', if the smaller-threshold objective image is non-empty and the larger-threshold image is BddBelow, then wynerZivRatePmf U P_XY d D' ≤ wynerZivRatePmf U P_XY d D.

The non-emptiness condition is genuinely required because of Mathlib's Real.sInf_empty = 0 convention: without it, sInf (image D') ≤ sInf (image D) = 0 could fail when the smaller image is empty and the larger one is non-empty with a negative infimum. The BddBelow side condition is supplied automatically by the wynerZivRatePmf_antitone_of_nonempty corollary below via the simplex projection.

Used by

theorem

InformationTheory.Shannon.wzMarginalXY_add

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (q₁ q₂ : α × β × U → ℝ) :

wzMarginalXY U (q₁ + q₂) = wzMarginalXY U q₁ + wzMarginalXY U q₂

wzMarginalXY is additive in q.

Used by

theorem

InformationTheory.Shannon.wzMarginalXY_smul

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (c : ℝ) (q : α × β × U → ℝ) :

wzMarginalXY U (c • q) = c • wzMarginalXY U q

wzMarginalXY is homogeneous in q.

Used by

theorem

InformationTheory.Shannon.wzExpectedDistortion_add

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (d : α → γ → ℝ) (q₁ q₂ : α × β × U → ℝ) (f : U × β → γ) :

wzExpectedDistortion U d (q₁ + q₂) f = wzExpectedDistortion U d q₁ f + wzExpectedDistortion U d q₂ f

wzExpectedDistortion (for fixed decoder f) is additive in q.

Used by

theorem

InformationTheory.Shannon.wzExpectedDistortion_smul

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (d : α → γ → ℝ) (c : ℝ) (q : α × β × U → ℝ) (f : U × β → γ) :

wzExpectedDistortion U d (c • q) f = c * wzExpectedDistortion U d q f

wzExpectedDistortion (for fixed decoder f) is homogeneous in q.

Used by

theorem

InformationTheory.Shannon.convex_stdSimplex_wynerZiv

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (U : Type u_3) [Fintype U] :

Convex ℝ (stdSimplex ℝ (α × β × U))

convex_stdSimplex re-exported for the Wyner–Ziv ambient simplex stdSimplex ℝ (α × β × U).

Used by

theorem

InformationTheory.Shannon.wynerZivConstraint_fst_subset_stdSimplex

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) :

(fun (qf : (α × β × U → ℝ) × (U × β → γ)) => qf.1) '' WynerZivConstraint U P_XY d D ⊆ stdSimplex ℝ (α × β × U)

The first projection of the Wyner–Ziv constraint set is contained in the standard simplex on α × β × U. This is the natural pmf-level containment for the joint pmf component.

Used by

theorem

InformationTheory.Shannon.wynerZivObjective_image_bddBelow

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) :

BddBelow ((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D)

The Wyner–Ziv objective image is bounded below.

Used by

theorem

InformationTheory.Shannon.wynerZivRatePmf_antitone_of_nonempty

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) {D D' : ℝ} (hD : D ≤ D') (h_ne : ((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D).Nonempty) :

wynerZivRatePmf U P_XY d D' ≤ wynerZivRatePmf U P_XY d D

D-antitone, with BddBelow discharged in the body. The non-emptiness side condition remains: the user must supply at least one feasible (q, f) at the smaller threshold D.

Used by

theorem

InformationTheory.Shannon.wynerZivObjective_image_nonempty_of_feasible

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) {qf : (α × β × U → ℝ) × (U × β → γ)} (hqf : qf ∈ WynerZivConstraint U P_XY d D) :

((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D).Nonempty

Image non-emptiness from feasibility witness. If a feasible (q, f) ∈ WynerZivConstraint U P_XY d D exists, the Wyner–Ziv objective image at D is non-empty. Trivial unwrapping.

Used by

theorem

InformationTheory.Shannon.wynerZivRatePmf_antitone_of_feasible

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) {D D' : ℝ} (hD : D ≤ D') {qf : (α × β × U → ℝ) × (U × β → γ)} (hqf : qf ∈ WynerZivConstraint U P_XY d D) :

wynerZivRatePmf U P_XY d D' ≤ wynerZivRatePmf U P_XY d D

D-antitone, feasibility-witness form. Given a feasible (q, f) ∈ WynerZivConstraint U P_XY d D at the smaller threshold D, the Wyner–Ziv rate is antitone: R_WZ(D') ≤ R_WZ(D) for any D' ≥ D. Both the non-emptiness and the BddBelow side conditions are discharged internally, so only a feasibility witness is required.

Used by

theorem

InformationTheory.Shannon.stdSimplex_convex_combination_mem

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] {q₁ q₂ : α × β × U → ℝ} (hq₁ : q₁ ∈ stdSimplex ℝ (α × β × U)) (hq₂ : q₂ ∈ stdSimplex ℝ (α × β × U)) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

a • q₁ + b • q₂ ∈ stdSimplex ℝ (α × β × U)

A convex combination of two simplex points lies in the simplex, on the Wyner–Ziv ambient simplex α × β × U.

Used by

theorem

InformationTheory.Shannon.wzMarginalXY_convex_combination

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) {q₁ q₂ : α × β × U → ℝ} (h1 : wzMarginalXY U q₁ = P_XY) (h2 : wzMarginalXY U q₂ = P_XY) {a b : ℝ} (hab : a + b = 1) :

wzMarginalXY U (a • q₁ + b • q₂) = P_XY

wzMarginalXY is preserved under convex combinations: if both q₁, q₂ have wzMarginalXY = P_XY, then so does any convex combination.

Used by

theorem

InformationTheory.Shannon.wzExpectedDistortion_convex_combination

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (d : α → γ → ℝ) (q₁ q₂ : α × β × U → ℝ) (f : U × β → γ) {a b : ℝ} :

wzExpectedDistortion U d (a • q₁ + b • q₂) f = a * wzExpectedDistortion U d q₁ f + b * wzExpectedDistortion U d q₂ f

wzExpectedDistortion (for fixed decoder f) is linear under convex combinations of q.

Used by