Entropy-region infrastructure for Theorem 4

This module packages the generic Fin n set-function surface used by the exact entropic-region closure form of Theorem 4: the n-ary entropy function entropyFnN, the generic cone predicates zhangYeungAtN and zhangYeungHoldsN, the Shannon and entropic region sets, and the restriction map from Fin n down to the first four coordinates. Witness-specific Fin n lemmas (the lifted witness and its cone membership / violation) live in ZhangYeung.Theorem4.

def ZhangYeung.IFN {n : ℕ} (F : Finset (Fin n) → ℝ) (α β : Finset (Fin n)) : ℝ

IF generalized to Finset (Fin n).

Equations

• ZhangYeung.IFN F α β = F α + F β - F (α ∪ β)

def ZhangYeung.condIFN {n : ℕ} (F : Finset (Fin n) → ℝ) (α β γ : Finset (Fin n)) : ℝ

condIF generalized to Finset (Fin n).

Equations

• ZhangYeung.condIFN F α β γ = F (α ∪ γ) + F (β ∪ γ) - F (α ∪ β ∪ γ) - F γ

def ZhangYeung.deltaFN {n : ℕ} (F : Finset (Fin n) → ℝ) (i j k l : Fin n) : ℝ

deltaF generalized to Finset (Fin n).

Equations

• ZhangYeung.deltaFN F i j k l = ZhangYeung.IFN F {i} {j} - ZhangYeung.condIFN F {i} {j} {k} - ZhangYeung.condIFN F {i} {j} {l}

def ZhangYeung.shannonConeN {n : ℕ} (F : Finset (Fin n) → ℝ) : Prop

Γ_n (paper eq. 11) as a predicate on Finset (Fin n) → ℝ.

Equations

• ZhangYeung.shannonConeN F = (F ∅ = 0 ∧ (∀ (α β : Finset (Fin n)), α ⊆ β → F α ≤ F β) ∧ ∀ (α β : Finset (Fin n)), F (α ∪ β) + F (α ∩ β) ≤ F α + F β)

def ZhangYeung.zhangYeungAtN {n : ℕ} (F : Finset (Fin n) → ℝ) (i j k l : Fin n) : Prop

The Zhang-Yeung inequality at a 4-tuple labeling over Fin n.

Equations

• One or more equations did not get rendered due to their size.

def ZhangYeung.zhangYeungHoldsN {n : ℕ} (F : Finset (Fin n) → ℝ) : Prop

The Fin n-indexed Zhang-Yeung cone tildeΓ_n: the Zhang-Yeung inequality holds at every ordered 4-tuple of pairwise distinct indices. This "pairwise-distinctness" presentation is extensionally equivalent to the paper's card-4 form (eq. 25) quantified over Equiv.Perm (Fin n) — every permutation yields a pairwise-distinct 4-tuple, and every pairwise-distinct 4-tuple extends to a permutation — but it is easier to manipulate in proofs, so the Fin n lift uses it in place of the Equiv.Perm form that zhangYeungHolds uses at n = 4. The point-level predicate zhangYeungAtN does agree definitionally with zhangYeungAt at n = 4 (pinned by Iff.rfl in the test module); the quantifier shapes of zhangYeungHoldsN and zhangYeungHolds differ, so their equivalence at n = 4 is extensional rather than definitional.

Equations

• ZhangYeung.zhangYeungHoldsN F = ∀ (i j k l : Fin n), i ≠ j → i ≠ k → i ≠ l → j ≠ k → j ≠ l → k ≠ l → ZhangYeung.zhangYeungAtN F i j k l

noncomputable def ZhangYeung.entropyFnN {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {S : Fin n → Type u} [(i : Fin n) → MeasurableSpace (S i)] (X : (i : Fin n) → Ω → S i) (μ : MeasureTheory.Measure Ω) : Finset (Fin n) → ℝ

The entropy function of an n-variable random-variable family X : ∀ i : Fin n, Ω → S i, expressed as a set function on Finset (Fin n).

Equations

• ZhangYeung.entropyFnN X μ α = H[fun (ω : Ω) (i : ↥α) => X (↑i) ω; μ]

@[reducible, inline]

noncomputable abbrev ZhangYeung.entropyFn {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] (X : (i : Fin 4) → Ω → S i) (μ : MeasureTheory.Measure Ω) : Finset (Fin 4) → ℝ

The original four-variable entropy function surface, now as the n = 4 specialization of entropyFnN.

Equations

• ZhangYeung.entropyFn X μ = ZhangYeung.entropyFnN X μ

def ZhangYeung.shannonRegionN (n : ℕ) : Set (Finset (Fin n) → ℝ)

The Shannon outer bound Γ_n, packaged as a set. Membership is definitionally shannonConeN.

Equations

• ZhangYeung.shannonRegionN n = {F : Finset (Fin n) → ℝ | ZhangYeung.shannonConeN F}

def ZhangYeung.entropyRegionN (n : ℕ) : Set (Finset (Fin n) → ℝ)

The entropic region Γ_n^*, packaged as the set of actual entropy functions of n discrete random variables. The quantified probability space and codomain family range over the ambient universe u, so a Type u realization is literally a member of the set.

Equations

• One or more equations did not get rendered due to their size.

def ZhangYeung.almostEntropicRegionN (n : ℕ) : Set (Finset (Fin n) → ℝ)

The almost-entropic region closure (Γ_n^*). Inherits the universe parameter from entropyRegionN: the closure is taken in the same ambient universe u, so a point witnessed by a Type u entropy function (or a limit of such) is literally a member of the set.

Equations

• ZhangYeung.almostEntropicRegionN n = closure (ZhangYeung.entropyRegionN n)

def ZhangYeung.restrictFirstFour {n : ℕ} (hn : 4 ≤ n) : (Finset (Fin n) → ℝ) → Finset (Fin 4) → ℝ

Restrict a set function on Fin n to its first four coordinates.

Equations

• ZhangYeung.restrictFirstFour hn F α = F (Finset.map (Fin.castLEEmb hn) α)

theorem ZhangYeung.restrictFirstFour_continuous {n : ℕ} (hn : 4 ≤ n) : Continuous (restrictFirstFour hn)

restrictFirstFour is continuous in the pointwise topology.

theorem ZhangYeung.entropyFnN_restrictFirstFour {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {S : Fin n → Type u} [(i : Fin n) → MeasurableSpace (S i)] [∀ (i : Fin n), Finite (S i)] [∀ (i : Fin n), MeasurableSingletonClass (S i)] {X : (i : Fin n) → Ω → S i} (hX : ∀ (i : Fin n), Measurable (X i)) (μ : MeasureTheory.Measure Ω) (hn : 4 ≤ n) : restrictFirstFour hn (entropyFnN X μ) = entropyFnN (fun (i : Fin 4) => X (Fin.castLE hn i)) μ

Restricting an n-variable entropy function to the first four coordinates agrees with taking the entropy function of the restricted family.

theorem ZhangYeung.restrictFirstFour_mem_entropyRegionN {n : ℕ} (hn : 4 ≤ n) {F : Finset (Fin n) → ℝ} (hF : F ∈ entropyRegionN n) : restrictFirstFour hn F ∈ entropyRegionN 4

Entropic points remain entropic after restriction to the first four coordinates.

theorem ZhangYeung.restrictFirstFour_mem_almostEntropicRegionN {n : ℕ} (hn : 4 ≤ n) {F : Finset (Fin n) → ℝ} (hF : F ∈ almostEntropicRegionN n) : restrictFirstFour hn F ∈ almostEntropicRegionN 4

Almost-entropic points remain almost entropic after restriction to the first four coordinates.