Section 12 pasting: matrix Chernoff comparison #
Continuous-functional-calculus form of the Bernoulli matrix Chernoff lemma.
theorem
MIPStarRE.LDT.Pasting.chernoffBernoulliMatrix
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(ψ : QuantumState ι)
(hnorm : ψ.IsNormalized)
(theta : Error)
(k degree : ℕ)
(X : Quantum.Op ι)
(kappa : Error)
(hθ0 : 0 < theta)
(hθ1 : theta < 1)
(hk : 2 * ↑degree / theta ≤ ↑k)
(hXpsd : 0 ≤ X)
(hXleOne : X ≤ 1)
(hcomplete :
CompletenessAtLeast ψ
{ outcome := fun (x : Unit) => X, total := X, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := hXleOne }
(1 - kappa))
:
ChernoffBernoulliMatrixStatement ψ theta k degree X kappa hXpsd hXleOne
lem:chernoff-bernoulli-matrix.
The operator-level reduction is now fully internal: continuous functional
calculus compares the Bernoulli-tail polynomial F(X) against an affine lower
envelope, and the scalar Hoeffding estimate is proved locally in
Bernoulli/Scalar.lean.