The discrete law of the high set

This file packages the product weights used in the proof of Theorem 2.1 as an actual probability measure on Finset (Fin m). It also identifies the probability of the rejection event with twoPointRejectionMass, so the finite two-point calibration result can be stated directly as a probability bound.

@[instance_reducible]

noncomputable instance Feige.highSetMeasurableSpace (m : ℕ) : MeasurableSpace (Finset (Fin m))

Equations

• Feige.highSetMeasurableSpace m = ⊤

noncomputable def Feige.highSetPMF {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) : PMF (Finset (Fin m))

The probability mass function of the independent high set.

Equations

• Feige.highSetPMF p hp0 hp1 = PMF.ofFintype (fun (S : Finset (Fin m)) => ENNReal.ofReal (Feige.highSetMass p S)) ⋯

noncomputable def Feige.highSetMeasure {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) : MeasureTheory.Measure (Finset (Fin m))

The high-set probability measure.

Equations

• Feige.highSetMeasure p hp0 hp1 = (Feige.highSetPMF p hp0 hp1).toMeasure

instance Feige.highSetMeasure.isProbabilityMeasure {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) : MeasureTheory.IsProbabilityMeasure (highSetMeasure p hp0 hp1)

@[simp]

theorem Feige.highSetPMF_apply {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) (S : Finset (Fin m)) : (highSetPMF p hp0 hp1) S = ENNReal.ofReal (highSetMass p S)

theorem Feige.highSetMeasure_apply_finset {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) (A : Finset (Finset (Fin m))) : (highSetMeasure p hp0 hp1) ↑A = ∑ S ∈ A, ENNReal.ofReal (highSetMass p S)

Probability of a finite collection of high sets.

theorem Feige.highSetMeasure_real_apply_finset {m : ℕ} (p : Fin m → ℝ) (hp0 : ∀ (i : Fin m), 0 ≤ p i) (hp1 : ∀ (i : Fin m), p i ≤ 1) (A : Finset (Finset (Fin m))) : (highSetMeasure p hp0 hp1).real ↑A = ∑ S ∈ A, highSetMass p S

Real-valued probability of a finite collection of high sets.

noncomputable def Feige.twoPointRejectionEvent {m : ℕ} (γ β : Fin m → ℝ) (α : ℝ) : Finset (Finset (Fin m))

The rejection event in the high-set sample space.

Equations

• Feige.twoPointRejectionEvent γ β α = {S : Finset (Fin m) | Feige.twoPointKFinset γ β S ≤ α}

theorem Feige.highSetMeasure_rejectionEvent {m : ℕ} (γ β : Fin m → ℝ) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 < β i) (α : ℝ) : (highSetMeasure (twoPointHighProbability γ β) ⋯ ⋯).real ↑(twoPointRejectionEvent γ β α) = twoPointRejectionMass γ β α

Its actual probability is the finite two-point rejection mass.

noncomputable def Feige.canonicalTwoPointVector {m : ℕ} (γ β : Fin m → ℝ) (S : Finset (Fin m)) (i : Fin m) : ℝ

Canonical two-point random vector on the high-set probability space.

Equations

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

theorem Feige.canonicalTwoPoint_coordinate_mean_one {m : ℕ} (γ β : Fin m → ℝ) (i : Fin m) (h : γ i + β i ≠ 0) : highProbability (γ i) (β i) * canonicalTwoPointVector γ β {i} i + (1 - highProbability (γ i) (β i)) * canonicalTwoPointVector γ β ∅ i = 1

Each coordinate of the canonical two-point vector has mean one. This is the scalar identity underlying the product construction.

def Feige.canonicalTwoPointPiVector {m : ℕ} (γ β : Fin m → ℝ) (ω : Fin m → Bool) (i : Fin m) : ℝ

Equivalent product-Bool realization of the canonical two-point vector. This model makes coordinate independence available directly from the product-measure API.

Equations

• Feige.canonicalTwoPointPiVector γ β ω i = if ω i = true then Feige.highValue (β i) else Feige.lowValue (γ i)

theorem Feige.iIndepFun_canonicalTwoPointPiVector {m : ℕ} (γ β : Fin m → ℝ) (μ : Fin m → MeasureTheory.Measure Bool) [∀ (i : Fin m), MeasureTheory.IsProbabilityMeasure (μ i)] : ProbabilityTheory.iIndepFun (fun (i : Fin m) (ω : Fin m → Bool) => canonicalTwoPointPiVector γ β ω i) (MeasureTheory.Measure.pi μ)

The coordinates of the canonical two-point vector are independent under any product law on the underlying Boolean coordinates.