Section 12 pasting: matrix Chernoff comparison

Continuous-functional-calculus form of the Bernoulli matrix Chernoff lemma: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/MatrixChernoff.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The two functional-calculus identities mention no state, so they are stated over any C⋆-algebra: they serve the local algebra 𝔓 (the vendored Op ι) and K →L[ℂ] K alike. The vendored entrywise ext i j; simp closing the first of them is Nat.cast_smul_eq_nsmul here. The Chernoff comparison chernoffBernoulliMatrix evaluates an operator on the space of its state, so its vendored one-space state ψ : QuantumState ι and operator X : Op ι are a vector state V : VecState K and an operator X : K →L[ℂ] K, as in ChernoffBernoulliMatrixStatement of Co/Pasting/Statements.lean. The hypothesis hnorm : ψ.IsNormalized is dropped: a vector state is normalized (V.ev_one_of_isNormalized).

The scalar Bernoulli tail polynomial, its affine lower envelope and the pointwise comparison of the two are classical and imported from the vendored Pasting/Bernoulli/Scalar.lean through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

Nothing: every vendored declaration has a counterpart of the same name.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/ld-pasting.tex

theorem MIPRE.LIDT.Co.Pasting.cfc_scalarBernoulliTail_eq_bernoulliTailOperator {A : Type u_1} [CStarAlgebra A] (X : A) (hA : IsSelfAdjoint X) (k degree : ℕ) : cfc (MIPStarRE.LDT.Pasting.scalarBernoulliTail k degree) X = bernoulliTailOperator k degree X

The scalar Bernoulli tail polynomial lifted through continuous functional calculus is exactly the matrix Bernoulli tail operator.

theorem MIPRE.LIDT.Co.Pasting.cfc_bernoulliTailLowerAffine_eq {A : Type u_1} [CStarAlgebra A] (X : A) (hA : IsSelfAdjoint X) (theta c : ℝ) : cfc (MIPStarRE.LDT.Pasting.bernoulliTailLowerAffine theta c) X = (1 - c) • 1 - (1 / (1 - theta)) • (1 - X)

Continuous functional calculus sends the affine lower envelope to the expected affine operator expression.

theorem MIPRE.LIDT.Co.Pasting.chernoffBernoulliMatrix {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (theta : ℝ) (k degree : ℕ) (X : K →L[ℂ] K) (kappa : ℝ) (hθ0 : 0 < theta) (hθ1 : theta < 1) (hk : 2 * ↑degree / theta ≤ ↑k) (hXpsd : 0 ≤ X) (hXleOne : X ≤ 1) (hcomplete : V.CompletenessAtLeast { outcome := fun (x : Unit) => X, total := X, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := hXleOne } (1 - kappa)) : ChernoffBernoulliMatrixStatement V theta k degree X kappa hXpsd hXleOne

lem:chernoff-bernoulli-matrix.

Continuous functional calculus compares the Bernoulli-tail polynomial F(X) against an affine lower envelope, and the scalar Hoeffding estimate is the classical bernoulliTailLowerAffine_le_scalarBernoulliTail.