Scalar Bernoulli polynomial helpers for pasting

Purely scalar inequalities used by the matrix Chernoff comparison.

noncomputable def MIPStarRE.LDT.Pasting.scalarBernoulliTail (k degree : ℕ) (p : Error) : Error

Scalar Bernoulli tail polynomial F(p) = ∑_{r=degree+1}^k C(k,r) p^r (1-p)^{k-r} from lem:chernoff-bernoulli-matrix.

Equations

• MIPStarRE.LDT.Pasting.scalarBernoulliTail k degree p = ∑ r ∈ Finset.Icc (degree + 1) k, ↑(k.choose r) * (p ^ r * (1 - p) ^ (k - r))

noncomputable def MIPStarRE.LDT.Pasting.bernoulliTailLowerAffine (theta c p : Error) : Error

The affine lower envelope used in the matrix Chernoff reduction.

Equations

• MIPStarRE.LDT.Pasting.bernoulliTailLowerAffine theta c p = 1 - c - 1 / (1 - theta) * (1 - p)

theorem MIPStarRE.LDT.Pasting.scalarBernoulliTail_hoeffding_lower_bound (k degree : ℕ) {p : Error} (hpd : ↑degree / ↑k ≤ p) (hp1 : p ≤ 1) : 1 - Real.exp (-(2 * (p - ↑degree / ↑k) ^ 2 * ↑k)) ≤ scalarBernoulliTail k degree p

The scalar Bernoulli tail satisfies the additive Hoeffding lower bound used by lem:chernoff-bernoulli-matrix.

theorem MIPStarRE.LDT.Pasting.bernoulliTailLowerAffine_le_scalarBernoulliTail (theta : Error) (k degree : ℕ) (hθ0 : 0 < theta) (hθ1 : theta < 1) (hk : 2 * ↑degree / theta ≤ ↑k) {p : Error} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : bernoulliTailLowerAffine theta (Real.exp (-(theta ^ 2 * ↑k) / 2)) p ≤ scalarBernoulliTail k degree p

Pointwise lower bound on [0,1] combining the scalar Hoeffding estimate with k ≥ 2d/θ.