Removing strict positivity from the finite two-point bound

noncomputable def Feige.boundaryEpsilon (n : ℕ) : ℝ

A positive perturbation parameter tending to zero.

Equations

• Feige.boundaryEpsilon n = 1 / (↑n + 1)

noncomputable def Feige.strictGammaApprox {m : ℕ} (γ : Fin m → ℝ) (n : ℕ) (i : Fin m) : ℝ

A strictly positive approximation to a nonnegative lower displacement.

Equations

• Feige.strictGammaApprox γ n i = (1 - Feige.boundaryEpsilon n) * γ i + Feige.boundaryEpsilon n / 2

theorem Feige.boundaryEpsilon_pos (n : ℕ) : 0 < boundaryEpsilon n

theorem Feige.boundaryEpsilon_le_one (n : ℕ) : boundaryEpsilon n ≤ 1

theorem Feige.strictGammaApprox_pos {m : ℕ} {γ : Fin m → ℝ} (hγ : ∀ (i : Fin m), 0 ≤ γ i) (n : ℕ) (i : Fin m) : 0 < strictGammaApprox γ n i

theorem Feige.strictGammaApprox_le_one {m : ℕ} {γ : Fin m → ℝ} (hγ1 : ∀ (i : Fin m), γ i ≤ 1) (n : ℕ) (i : Fin m) : strictGammaApprox γ n i ≤ 1

theorem Feige.tendsto_boundaryEpsilon : Filter.Tendsto boundaryEpsilon Filter.atTop (nhds 0)

theorem Feige.tendsto_strictGammaApprox {m : ℕ} (γ : Fin m → ℝ) : Filter.Tendsto (strictGammaApprox γ) Filter.atTop (nhds γ)

theorem Feige.tendsto_twoPointKFinset_strictGammaApprox {m : ℕ} (γ β : Fin m → ℝ) (S : Finset (Fin m)) : Filter.Tendsto (fun (n : ℕ) => twoPointKFinset (strictGammaApprox γ n) β S) Filter.atTop (nhds (twoPointKFinset γ β S))

theorem Feige.tendsto_twoPointHighProbability_strictGammaApprox {m : ℕ} (γ β : Fin m → ℝ) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 < β i) (i : Fin m) : Filter.Tendsto (fun (n : ℕ) => twoPointHighProbability (strictGammaApprox γ n) β i) Filter.atTop (nhds (twoPointHighProbability γ β i))

theorem Feige.tendsto_highSetMass_strictGammaApprox {m : ℕ} (γ β : Fin m → ℝ) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 < β i) (S : Finset (Fin m)) : Filter.Tendsto (fun (n : ℕ) => highSetMass (twoPointHighProbability (strictGammaApprox γ n) β) S) Filter.atTop (nhds (highSetMass (twoPointHighProbability γ β) S))

theorem Feige.eventually_rejectionFinset_subset_strictApprox {m : ℕ} (γ β : Fin m → ℝ) (α δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ S ∈ {S : Finset (Fin m) | twoPointKFinset γ β S ≤ α}, twoPointKFinset (strictGammaApprox γ n) β S ≤ α + δ

Every state rejected at the limiting parameter is, uniformly over the finite Boolean state space, eventually rejected at threshold α + δ by the strict approximants.

theorem Feige.twoPointRejectionMass_le_add_delta {m : ℕ} (γ β : Fin m → ℝ) (hγ0 : ∀ (i : Fin m), 0 ≤ γ i) (hγ1 : ∀ (i : Fin m), γ i ≤ 1) (hβ : ∀ (i : Fin m), 0 < β i) {α δ : ℝ} (hα : 0 ≤ α) (hδ : 0 < δ) : twoPointRejectionMass γ β α ≤ α + δ

theorem Feige.twoPointRejectionMass_le_alpha {m : ℕ} (γ β : Fin m → ℝ) (hγ0 : ∀ (i : Fin m), 0 ≤ γ i) (hγ1 : ∀ (i : Fin m), γ i ≤ 1) (hβ : ∀ (i : Fin m), 0 < β i) {α : ℝ} (hα : 0 ≤ α) : twoPointRejectionMass γ β α ≤ α

Closed-boundary two-point rejection estimate.

theorem Feige.twoPointRejectionBound : TwoPointRejectionBound

The fully discharged finite two-point rejection hypothesis used by the conditional-mixture calibration theorem.