Documentation

MIPRE.Foundations.StateModel

A state on a represented `⋆`-algebra #

The state calculus of MIPRE/Foundations/OpCalculus.lean is about operators on a Hilbert space. The analyses write their operators in an algebra: matrices on ℂ^N, or elements of the players' algebras. A state model (StateModel 𝒞) is the bridge: a complex Hilbert space H with a state ψ, and a ⋆-algebra 𝒞 represented on H by a ⋆-homomorphism π. Its state norm, bound and quadratic form are those of π T:

M.snorm T = ‖π T ψ‖,
M.Bnd T K, the bound ‖π T v‖ ≤ K ‖v‖ for every v,
M.qform T = Re ⟨ψ, π T ψ⟩,

with the rules of the calculus restated in 𝒞, so that a chain of estimates about products and sums in 𝒞 never has to push π through them by hand.

The matrix calculus of MIPRE/Foundations/OpBound.lean is this calculus in the model StateModel.mat v: 𝒞 = M_N(ℂ) acting on EuclideanSpace ℂ N through Matrix.toEuclideanCLM, with the state v. Its state norm is literally the matrix one (snorm_mat), and so are its products and sums: a matrix statement is the generic statement in that model, with no operator pushed through anything. This is why the algebra is a parameter rather than always H →L[ℂ] H: the elaborator never has to move Matrix.toEuclideanCLM across a product.

structure MIPRE.StateModel (𝒞 : Type v) [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] :

Type (max (u + 1) v)

A state model: a complex Hilbert space with a state, and a ⋆-algebra represented on it by a ⋆-homomorphism.

H : Type u
The Hilbert space.
normedAddCommGroup : NormedAddCommGroup self.H
innerProductSpace : InnerProductSpace ℂ self.H
completeSpace : CompleteSpace self.H
ψ : self.H
The state.
π : 𝒞 →⋆ₐ[ℂ ] self.H →L[ℂ ] self.H
The representation of the algebra.

Instances For

The calculus #

def MIPRE.StateModel.snorm {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) :

‖π T ψ‖.

Equations

M.snorm T = MIPRE.Op.snorm M.ψ (M.π T)

Instances For

def MIPRE.StateModel.qform {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) :

Re ⟨ψ, π T ψ⟩.

Equations

M.qform T = MIPRE.Op.qform M.ψ (M.π T)

Instances For

def MIPRE.StateModel.Bnd {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) (K : ℝ) :

‖π T v‖ ≤ K ‖v‖ for every v.

Equations

M.Bnd T K = MIPRE.Op.Bnd (M.π T) K

Instances For

theorem MIPRE.StateModel.snorm_nonneg {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) :

0 ≤ M.snorm T

theorem MIPRE.StateModel.snorm_add_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T T' : 𝒞) :

M.snorm (T + T') ≤ M.snorm T + M.snorm T'

theorem MIPRE.StateModel.snorm_sub_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T T' : 𝒞) :

M.snorm (T - T') ≤ M.snorm T + M.snorm T'

theorem MIPRE.StateModel.snorm_sub_comm {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T T' : 𝒞) :

M.snorm (T - T') = M.snorm (T' - T)

theorem MIPRE.StateModel.snorm_smul {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (c : ℂ) (T : 𝒞) :

M.snorm (c • T) = ‖c‖ * M.snorm T

theorem MIPRE.StateModel.snorm_neg {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) :

M.snorm (-T) = M.snorm T

theorem MIPRE.StateModel.snorm_zero {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) :

M.snorm 0 = 0

theorem MIPRE.StateModel.snorm_one {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) :

M.snorm 1 = 1

theorem MIPRE.StateModel.snorm_sum_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_1} (s : Finset ι) (f : ι → 𝒞) :

M.snorm (∑ i ∈ s, f i) ≤ ∑ i ∈ s, M.snorm (f i)

The triangle inequality over a finite sum.

theorem MIPRE.StateModel.snorm_mul_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} {K : ℝ} (h : M.Bnd T K) (T' : 𝒞) :

M.snorm (T * T') ≤ K * M.snorm T'

A bound in front of anything.

theorem MIPRE.StateModel.star_π_mul_self {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} (h : star T * T = 1) :

star (M.π T) * M.π T = 1

An isometry of 𝒞 is represented by an isometry.

theorem MIPRE.StateModel.snorm_mul_of_isometry {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} (h : star T * T = 1) (T' : 𝒞) :

M.snorm (T * T') = M.snorm T'

An isometry in front changes nothing.

theorem MIPRE.StateModel.snorm_mul_swap {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {W WD Z : 𝒞} {δ K : ℝ} (hWD : star WD * WD = 1) (hcomm : WD * Z = Z * WD) (hZ : M.Bnd Z K) (hK : 0 ≤ K) (hd : M.snorm (W - WD) ≤ δ) :

M.snorm (Z * W) ≤ M.snorm Z + K * δ

Replacing an operator by an isometry it is close to, in front of anything.

theorem MIPRE.StateModel.qform_add {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T T' : 𝒞) :

M.qform (T + T') = M.qform T + M.qform T'

theorem MIPRE.StateModel.qform_sub {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T T' : 𝒞) :

M.qform (T - T') = M.qform T - M.qform T'

theorem MIPRE.StateModel.qform_smul_real {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (r : ℝ) (T : 𝒞) :

M.qform (↑r • T) = r * M.qform T

theorem MIPRE.StateModel.qform_zero {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) :

M.qform 0 = 0

theorem MIPRE.StateModel.qform_sum {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_1} (s : Finset ι) (f : ι → 𝒞) :

M.qform (∑ i ∈ s, f i) = ∑ i ∈ s, M.qform (f i)

theorem MIPRE.StateModel.qform_one {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) :

M.qform 1 = 1

theorem MIPRE.StateModel.snorm_sq_eq_qform {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) :

M.snorm T ^ 2 = M.qform (star T * T)

The squared state norm is the quadratic form of T* T.

theorem MIPRE.StateModel.qform_nonneg {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} (h : 0 ≤ M.π T) :

0 ≤ M.qform T

The quadratic form of an element represented by a positive operator is nonnegative.

theorem MIPRE.StateModel.Bnd.add {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T T' : 𝒞} {K L : ℝ} (h : M.Bnd T K) (h' : M.Bnd T' L) :

M.Bnd (T + T') (K + L)

theorem MIPRE.StateModel.Bnd.sub {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T T' : 𝒞} {K L : ℝ} (h : M.Bnd T K) (h' : M.Bnd T' L) :

M.Bnd (T - T') (K + L)

theorem MIPRE.StateModel.Bnd.mul {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T T' : 𝒞} {K L : ℝ} (hK : 0 ≤ K) (h : M.Bnd T K) (h' : M.Bnd T' L) :

M.Bnd (T * T') (K * L)

theorem MIPRE.StateModel.bnd_one_of_isometry {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} (h : star T * T = 1) :

M.Bnd T 1

theorem MIPRE.StateModel.bnd_one_of_isStarProjection {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {P : 𝒞} (hP : IsStarProjection P) :

M.Bnd P 1

An orthogonal projection of 𝒞 is bounded by one.

Triangle inequalities for families #

theorem MIPRE.StateModel.sum_snorm_sq_triangle {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_1} (s : Finset ι) (P Q R : ι → 𝒞) :

∑ i ∈ s, M.snorm (P i - R i) ^ 2 ≤ 2 * ∑ i ∈ s, M.snorm (P i - Q i) ^ 2 + 2 * ∑ i ∈ s, M.snorm (Q i - R i) ^ 2

The triangle inequality for a family of deviations, at the usual cost of a factor two.

theorem MIPRE.StateModel.sum_snorm_sq_triangle3 {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_1} (s : Finset ι) (P Q R T : ι → 𝒞) :

∑ o ∈ s, M.snorm (P o - T o) ^ 2 ≤ 3 * ∑ o ∈ s, M.snorm (P o - Q o) ^ 2 + 3 * ∑ o ∈ s, M.snorm (Q o - R o) ^ 2 + 3 * ∑ o ∈ s, M.snorm (R o - T o) ^ 2

The three-term triangle inequality for a family of deviations.

Column contractions #

fact:add-a-proj of the paper: a family with ∑_i F_i† F_i ≤ 1 costs nothing in front of a deviation. The hypothesis is stated on the represented operators, where it is an inequality of operators on H: a player's algebra need not be ordered in a way that proves it, while for the elements of a POVM it holds in B(H) because t² ≤ t there.

def MIPRE.StateModel.IsColContraction {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_1} [Fintype ι] (F : ι → 𝒞) :

∑_i π(F_i)† π(F_i) ≤ 1: the family F is a contraction as a column of operators on H.

Equations

M.IsColContraction F = (∑ i : ι, star (M.π (F i)) * M.π (F i) ≤ 1)

Instances For

theorem MIPRE.StateModel.sum_snorm_sq_mul_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_1} [Fintype ι] (F : ι → 𝒞) (hF : M.IsColContraction F) (T : 𝒞) :

∑ i : ι, M.snorm (F i * T) ^ 2 ≤ M.snorm T ^ 2

A column contraction costs nothing in front (fact:add-a-proj): the family contributes its index to the sum and the operator behind it is unchanged.

An ordered algebra #

When 𝒞 is a star-ordered ring, π is monotone (a ⋆-homomorphism of star-ordered rings is), so an inequality in 𝒞 is one between operators.

theorem MIPRE.StateModel.π_nonneg {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {T : 𝒞} (h : 0 ≤ T) :

0 ≤ M.π T

A nonnegative element is represented by a positive operator.

theorem MIPRE.StateModel.qform_nonneg_of_nonneg {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {T : 𝒞} (h : 0 ≤ T) :

0 ≤ M.qform T

theorem MIPRE.StateModel.qform_mono {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {T T' : 𝒞} (h : T ≤ T') :

M.qform T ≤ M.qform T'

The quadratic form is monotone.

theorem MIPRE.StateModel.bnd_one_of_star_mul_self_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {T : 𝒞} (h : star T * T ≤ 1) :

M.Bnd T 1

An element with T* T ≤ 1 is represented by a contraction.

theorem MIPRE.StateModel.isColContraction_of_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {ι : Type u_1} [Fintype ι] {F : ι → 𝒞} (hF : ∑ i : ι, star (F i) * F i ≤ 1) :

M.IsColContraction F

An inequality ∑ F_i* F_i ≤ 1 in 𝒞 makes F a column contraction.

theorem MIPRE.StateModel.sum_snorm_sq_mul_le_of_le {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {ι : Type u_1} [Fintype ι] (F : ι → 𝒞) (hF : ∑ i : ι, star (F i) * F i ≤ 1) (T : 𝒞) :

∑ i : ι, M.snorm (F i * T) ^ 2 ≤ M.snorm T ^ 2

fact:add-a-proj with the hypothesis in 𝒞.

theorem MIPRE.StateModel.snorm_sq_mul_le_of_contraction {𝒞 : Type v} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) [PartialOrder 𝒞] [StarOrderedRing 𝒞] {P : 𝒞} (hP : star P * P ≤ 1) (T : 𝒞) :

M.snorm (P * T) ^ 2 ≤ M.snorm T ^ 2

A contraction in front costs nothing.

The matrix model #

noncomputable def MIPRE.StateModel.mat {N : Type u_1} [Fintype N] [DecidableEq N] (v : N → ℂ) :

StateModel (Matrix N N ℂ)

The matrix model of a vector v of ℂ^N: matrices acting on EuclideanSpace ℂ N.

Equations

One or more equations did not get rendered due to their size.

Instances For