The state calculus on a Hilbert space

The estimates of the rigidity arguments are chains of bounds ‖T ψ‖ ≤ … for operators T in front of a fixed state ψ. This file is that calculus for bounded operators on any complex inner product space:

• Op.snorm ψ T = ‖T ψ‖, with the triangle inequality, scalars, a bound in front and an isometry in front;
• Op.Bnd T K, the bound ‖T v‖ ≤ K ‖v‖ for every v, closed under sums, products and scalars;
• Op.qform ψ T = Re ⟨ψ, T ψ⟩, additive in T, with ‖T ψ‖² = qform ψ (T* T).

It is the first piece of the operator calculus of Phase 1(b) of planning/mipco-track.md, which restates the matrix calculus over H →L[ℂ] H so that the stage analyses can be read in any model with two commuting families of measurements. The matrix calculus of MIPRE/Foundations/OpBound.lean is its instance on EuclideanSpace ℂ N through Matrix.toEuclideanCLM, and its lemmas are proved from these.

As in the matrix calculus, the bound is a relation rather than the operator norm, and nothing here uses the Loewner order on operators: the estimates need neither.

The bound

def MIPRE.Op.Bnd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) (K : ℝ) : Prop

‖T v‖ ≤ K ‖v‖ for every v: the operator norm of T is at most K, as a relation.

Equations

• MIPRE.Op.Bnd T K = ∀ (v : H), ‖T v‖ ≤ K * ‖v‖

theorem MIPRE.Op.Bnd.add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T T' : H →L[ℂ] H} {K L : ℝ} (h : Bnd T K) (h' : Bnd T' L) : Bnd (T + T') (K + L)

theorem MIPRE.Op.Bnd.sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T T' : H →L[ℂ] H} {K L : ℝ} (h : Bnd T K) (h' : Bnd T' L) : Bnd (T - T') (K + L)

theorem MIPRE.Op.Bnd.mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T T' : H →L[ℂ] H} {K L : ℝ} (hK : 0 ≤ K) (h : Bnd T K) (h' : Bnd T' L) : Bnd (T * T') (K * L)

theorem MIPRE.Op.bnd_of_norm_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →L[ℂ] H} {K : ℝ} (h : ‖T‖ ≤ K) : Bnd T K

An operator of norm at most K is bounded by K.

The norm on a fixed state

def MIPRE.Op.snorm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T : H →L[ℂ] H) : ℝ

‖T ψ‖, for a fixed state ψ.

Equations

• MIPRE.Op.snorm ψ T = ‖T ψ‖

theorem MIPRE.Op.snorm_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T : H →L[ℂ] H) : 0 ≤ snorm ψ T

theorem MIPRE.Op.snorm_add_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T T' : H →L[ℂ] H) : snorm ψ (T + T') ≤ snorm ψ T + snorm ψ T'

theorem MIPRE.Op.snorm_sub_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T T' : H →L[ℂ] H) : snorm ψ (T - T') ≤ snorm ψ T + snorm ψ T'

theorem MIPRE.Op.snorm_sub_comm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T T' : H →L[ℂ] H) : snorm ψ (T - T') = snorm ψ (T' - T)

theorem MIPRE.Op.snorm_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (c : ℂ) (T : H →L[ℂ] H) : snorm ψ (c • T) = ‖c‖ * snorm ψ T

theorem MIPRE.Op.snorm_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (hψ : ‖ψ‖ = 1) : snorm ψ 1 = 1

theorem MIPRE.Op.snorm_mul_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) {T : H →L[ℂ] H} {K : ℝ} (h : Bnd T K) (T' : H →L[ℂ] H) : snorm ψ (T * T') ≤ K * snorm ψ T'

A bound in front of anything.

theorem MIPRE.Op.snorm_sum_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) {ι : Type u_2} (s : Finset ι) (f : ι → H →L[ℂ] H) : snorm ψ (∑ i ∈ s, f i) ≤ ∑ i ∈ s, snorm ψ (f i)

The triangle inequality over a finite sum.

The quadratic form

def MIPRE.Op.qform {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T : H →L[ℂ] H) : ℝ

Re ⟨ψ, T ψ⟩.

Equations

• MIPRE.Op.qform ψ T = (inner ℂ ψ (T ψ)).re

theorem MIPRE.Op.qform_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T T' : H →L[ℂ] H) : qform ψ (T + T') = qform ψ T + qform ψ T'

theorem MIPRE.Op.qform_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (T T' : H →L[ℂ] H) : qform ψ (T - T') = qform ψ T - qform ψ T'

theorem MIPRE.Op.qform_smul_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (r : ℝ) (T : H →L[ℂ] H) : qform ψ (↑r • T) = r * qform ψ T

theorem MIPRE.Op.qform_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) : qform ψ 0 = 0

theorem MIPRE.Op.qform_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) {ι : Type u_2} (s : Finset ι) (f : ι → H →L[ℂ] H) : qform ψ (∑ i ∈ s, f i) = ∑ i ∈ s, qform ψ (f i)

theorem MIPRE.Op.qform_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (hψ : ‖ψ‖ = 1) : qform ψ 1 = 1

theorem MIPRE.Op.qform_one_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) : qform ψ 1 = ‖ψ‖ ^ 2

Re ⟨ψ, ψ⟩ = ‖ψ‖².

theorem MIPRE.Op.qform_nonneg_of_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) [CompleteSpace H] {T : H →L[ℂ] H} (h : 0 ≤ T) : 0 ≤ qform ψ T

The quadratic form of a positive operator is nonnegative.

theorem MIPRE.Op.qform_mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) [CompleteSpace H] {T T' : H →L[ℂ] H} (h : T ≤ T') : qform ψ T ≤ qform ψ T'

The quadratic form is monotone.

Isometries and adjoints

theorem MIPRE.Op.norm_apply_of_isometry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →L[ℂ] H} (h : star T * T = 1) (v : H) : ‖T v‖ = ‖v‖

An isometry preserves the norm.

theorem MIPRE.Op.bnd_one_of_isometry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →L[ℂ] H} (h : star T * T = 1) : Bnd T 1

theorem MIPRE.Op.bnd_one_of_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsStarProjection P) : Bnd P 1

An orthogonal projection is bounded by one.

theorem MIPRE.Op.bnd_one_of_star_mul_self_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →L[ℂ] H} (h : star T * T ≤ 1) : Bnd T 1

An operator with T* T ≤ 1 is bounded by one: ‖T v‖² = Re ⟨v, T* T v⟩ ≤ ‖v‖².

theorem MIPRE.Op.snorm_mul_of_isometry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) {T : H →L[ℂ] H} (h : star T * T = 1) (T' : H →L[ℂ] H) : snorm ψ (T * T') = snorm ψ T'

An isometry in front changes nothing.

theorem MIPRE.Op.snorm_mul_swap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) {W WD Z : H →L[ℂ] H} {δ K : ℝ} (hWD : star WD * WD = 1) (hcomm : WD * Z = Z * WD) (hZ : Bnd Z K) (hK : 0 ≤ K) (hd : snorm ψ (W - WD) ≤ δ) : snorm ψ (Z * W) ≤ snorm ψ Z + K * δ

Replacing an operator by an isometry it is close to, in front of anything. If W and the isometry WD agree on the state to within δ, and WD commutes with Z, then Z W is within K δ of Z, where K bounds Z.

theorem MIPRE.Op.snorm_sq_eq_qform {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (T : H →L[ℂ] H) : snorm ψ T ^ 2 = qform ψ (star T * T)

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