Mean-one two-point systems

This file develops the two-point reduction used in the formal proof of Theorem 2.1. It records the canonical parametrization

Yᵢ ∈ {1 - γᵢ, 1 + βᵢ}, P(Yᵢ = 1 + βᵢ) = γᵢ / (γᵢ + βᵢ)

and proves the required Boolean-lattice monotonicity. The latter is obtained directly from the coordinatewise antitonicity of the exponential Dirichlet statistic.

noncomputable def Feige.highProbability (γ β : ℝ) : ℝ

Probability of the high value in a mean-one two-point law.

Equations

• Feige.highProbability γ β = γ / (γ + β)

def Feige.lowValue (γ : ℝ) : ℝ

The low value in the mean-one two-point parametrization.

Equations

• Feige.lowValue γ = 1 - γ

def Feige.highValue (β : ℝ) : ℝ

The high value in the mean-one two-point parametrization.

Equations

• Feige.highValue β = 1 + β

theorem Feige.highProbability_nonneg {γ β : ℝ} (hγ : 0 ≤ γ) (hβ : 0 < β) : 0 ≤ highProbability γ β

theorem Feige.highProbability_le_one {γ β : ℝ} (hγ : 0 ≤ γ) (hβ : 0 < β) : highProbability γ β ≤ 1

theorem Feige.one_sub_highProbability {γ β : ℝ} (h : γ + β ≠ 0) : 1 - highProbability γ β = β / (γ + β)

The complementary probability in symmetric form.

theorem Feige.twoPoint_mean_one {γ β : ℝ} (h : γ + β ≠ 0) : highProbability γ β * highValue β + (1 - highProbability γ β) * lowValue γ = 1

The parametrized two-point law has mean exactly one.

noncomputable def Feige.twoPointVector {ι : Type u_1} (γ β : ι → ℝ) (S : Set ι) (i : ι) : ℝ

The vector encoded by a high set S: coordinates in S take their high value, and all remaining coordinates take their low value.

Equations

• Feige.twoPointVector γ β S i = if i ∈ S then Feige.highValue (β i) else Feige.lowValue (γ i)

noncomputable def Feige.twoPointK {ι : Type u_1} [Fintype ι] (γ β : ι → ℝ) (S : Set ι) : ℝ

The Dirichlet statistic at the two-point vector encoded by S.

Equations

• Feige.twoPointK γ β S = Feige.dirichletK (Feige.twoPointVector γ β S)

theorem Feige.twoPointK_empty {ι : Type u_1} [Fintype ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 ≤ γ i) : twoPointK γ β ∅ = 1

At the bottom of the Boolean lattice every coefficient in the internal exponential event is nonpositive, so the defining event is certain.

theorem Feige.twoPointVector_mono {ι : Type u_1} {γ β : ι → ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 ≤ β i) : Monotone (twoPointVector γ β)

theorem Feige.twoPointK_antitone {ι : Type u_1} [Fintype ι] {γ β : ι → ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 ≤ β i) : Antitone (twoPointK γ β)

Moving upward in the Boolean lattice can only decrease the Dirichlet statistic.

def Feige.highSetMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (S : Finset ι) : ℝ

Product-law mass of a high set.

Equations

• Feige.highSetMass p S = (∏ i ∈ S, p i) * ∏ i ∈ Finset.univ \ S, (1 - p i)

theorem Feige.highSetMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} (hp0 : ∀ (i : ι), 0 ≤ p i) (hp1 : ∀ (i : ι), p i ≤ 1) (S : Finset ι) : 0 ≤ highSetMass p S

theorem Feige.sum_highSetMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) : ∑ S ∈ Finset.univ.powerset, highSetMass p S = 1

The product masses over all Boolean-lattice states sum to one.

noncomputable def Feige.twoPointKFinset {ι : Type u_1} [Fintype ι] (γ β : ι → ℝ) (S : Finset ι) : ℝ

Finset-indexed version of Kₘ(S), convenient for finite products and maximal-chain constructions.

Equations

• Feige.twoPointKFinset γ β S = Feige.twoPointK γ β ↑S

theorem Feige.twoPointKFinset_antitone {ι : Type u_1} [Fintype ι] {γ β : ι → ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 ≤ β i) : Antitone (twoPointKFinset γ β)

noncomputable def Feige.twoPointHighProbability {ι : Type u_1} (γ β : ι → ℝ) (i : ι) : ℝ

Coordinatewise high probabilities in the two-point parametrization.

Equations

• Feige.twoPointHighProbability γ β i = Feige.highProbability (γ i) (β i)

noncomputable def Feige.twoPointRejectionMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (α : ℝ) : ℝ

Rejection probability under the independent two-point product law, written as a finite sum over high sets.

Equations

• Feige.twoPointRejectionMass γ β α = ∑ S ∈ Finset.univ.powerset with Feige.twoPointKFinset γ β S ≤ α, Feige.highSetMass (Feige.twoPointHighProbability γ β) S

theorem Feige.twoPointHighProbability_nonneg {ι : Type u_1} {γ β : ι → ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 < β i) (i : ι) : 0 ≤ twoPointHighProbability γ β i

theorem Feige.twoPointHighProbability_le_one {ι : Type u_1} {γ β : ι → ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 < β i) (i : ι) : twoPointHighProbability γ β i ≤ 1

theorem Feige.twoPointRejectionMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ι → ℝ} {α : ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 < β i) : 0 ≤ twoPointRejectionMass γ β α

theorem Feige.twoPointRejectionMass_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ι → ℝ} {α : ℝ} (hγ : ∀ (i : ι), 0 ≤ γ i) (hβ : ∀ (i : ι), 0 < β i) : twoPointRejectionMass γ β α ≤ 1