InformationTheory.Shannon.BrascampLieb

Imports 3

Brascamp–Lieb inequality (combinatorial form) and hypercube product projection bound #

Generalizes the Loomis–Whitney inequality (LoomisWhitney.lean) to an arbitrary cover family S : ι → Finset (Fin n) where each j : Fin n is covered at least k times: $| A |^{k} \leq \prod_{i : ι} | π_{S_{i}} (A) | .$

Main definitions #

projectionSubset S A — restriction of A : Finset (Fin n → α) to a subset S : Finset (Fin n) of coordinates, returning a Finset (↥S → α).

Main statements #

brascamp_lieb_finset — Brascamp–Lieb inequality for arbitrary cover families.
hypercube_product_projection_bound — singleton-cover corollary: |A| ≤ ∏ i, |π_{{i}}(A)|.

Implementation notes #

The proof routes through shearer_inequality from LoomisWhitney.lean as the entropic engine, then peels off the logarithm via Real.log_le_log_iff.

Loomis–Whitney (loomis_whitney) is the special case S i := univ.filter (· ≠ i) (each j covered n-1 times), but the existing LoomisWhitney.lean shape is preserved to avoid changing projectionExcept and loomis_whitney.

Projection onto a coordinate subset #

def

InformationTheory.Shannon.projectionSubset

source

{n : ℕ} {α : Type u_1} [DecidableEq α] (S : Finset (Fin n)) (A : Finset (Fin n → α)) :

Finset (↥S → α)

The image of A : Finset (Fin n → α) under restriction to coordinates in S : Finset (Fin n).

Equations

InformationTheory.Shannon.projectionSubset S A = Finset.image (fun (x : Fin n → α) (j : ↥S) => x ↑j) A

Instances For

Used by

theorem

InformationTheory.Shannon.jointEntropySubset_le_log_projectionSubset_card

source

{n : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {A : Finset (Fin n → α)} (hA : A.Nonempty) (S : Finset (Fin n)) :

jointEntropySubset (ProbabilityTheory.uniformOn ↑A) (fun (i : Fin n) (ω : Fin n → α) => ω i) S ≤ Real.log ↑(projectionSubset S A).card

For A equipped with the uniform measure, the joint entropy over coordinates S is bounded by log |projectionSubset S A|.

Used by

Brascamp–Lieb inequality #

theorem