Inner-product facts

theorem CommutingRepetition.Resolver.Douglas.mulA {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (f g : 𝓗 →L[ℂ] 𝓗) (ξ : 𝓗) : (f * g) ξ = f (g ξ)

theorem CommutingRepetition.Resolver.Douglas.oneA {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (ξ : 𝓗) : 1 ξ = ξ

theorem CommutingRepetition.Resolver.Douglas.re_inner_star_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (T : 𝓗 →L[ℂ] 𝓗) (η : 𝓗) : (inner ℂ η ((star T * T) η)).re = ‖T η‖ ^ 2

theorem CommutingRepetition.Resolver.Douglas.nonneg_of_re_inner {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 →L[ℂ] 𝓗} (hT : IsSelfAdjoint T) (h : ∀ (ξ : 𝓗), 0 ≤ (inner ℂ (T ξ) ξ).re) : 0 ≤ T

Positivity of a self-adjoint operator from its quadratic form.

theorem CommutingRepetition.Resolver.Douglas.re_inner_nonneg_of_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 →L[ℂ] 𝓗} (hT : 0 ≤ T) (ξ : 𝓗) : 0 ≤ (inner ℂ ξ (T ξ)).re

theorem CommutingRepetition.Resolver.Douglas.norm_apply_le_of_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {x c : 𝓗 →L[ℂ] 𝓗} (h : star x * x ≤ star c * c) (η : 𝓗) : ‖x η‖ ≤ ‖c η‖

‖x η‖ ≤ ‖c η‖ when x* x ≤ c* c.

theorem CommutingRepetition.Resolver.Douglas.sum_sq_norm_apply_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {x : κ → 𝓗 →L[ℂ] 𝓗} {c : 𝓗 →L[ℂ] 𝓗} (h : ∑ k : κ, star (x k) * x k ≤ star c * c) (η : 𝓗) : ∑ k : κ, ‖(x k) η‖ ^ 2 ≤ ‖c η‖ ^ 2

theorem CommutingRepetition.Resolver.Douglas.le_of_sum_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {x : κ → 𝓗 →L[ℂ] 𝓗} {c : 𝓗 →L[ℂ] 𝓗} (h : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) : star (x k) * x k ≤ star c * c

The construction

noncomputable def CommutingRepetition.Resolver.Douglas.K {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (c : 𝓗 →L[ℂ] 𝓗) : Submodule ℂ 𝓗

The closure of the range of c.

Equations

• CommutingRepetition.Resolver.Douglas.K c = (↑c).range.topologicalClosure

theorem CommutingRepetition.Resolver.Douglas.range_le_K {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) : (↑c).range ≤ K c

instance CommutingRepetition.Resolver.Douglas.instHasOrthogonalProjectionComplexK {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) : (K c).HasOrthogonalProjection

theorem CommutingRepetition.Resolver.Douglas.apply_mem_K {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) (η : 𝓗) : c η ∈ K c

noncomputable def CommutingRepetition.Resolver.Douglas.incl {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) : ↥(↑c).range →L[ℂ] ↥(K c)

The inclusion range c → K.

Equations

• CommutingRepetition.Resolver.Douglas.incl c = (Submodule.inclusion ⋯).mkContinuous 1 ⋯

theorem CommutingRepetition.Resolver.Douglas.incl_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) (v : ↥(↑c).range) : ↑((incl c) v) = ↑v

theorem CommutingRepetition.Resolver.Douglas.denseRange_incl {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) : DenseRange ⇑(incl c)

theorem CommutingRepetition.Resolver.Douglas.isUniformInducing_incl {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) : IsUniformInducing ⇑(incl c)

noncomputable def CommutingRepetition.Resolver.Douglas.rep {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (c : 𝓗 →L[ℂ] 𝓗) (v : ↥(↑c).range) : 𝓗

A preimage under c of a range element.

Equations

• CommutingRepetition.Resolver.Douglas.rep c v = ⋯.choose

theorem CommutingRepetition.Resolver.Douglas.c_rep {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) (v : ↥(↑c).range) : c (rep c v) = ↑v

Invariance of K under commuting operators

theorem CommutingRepetition.Resolver.Douglas.K_invariant {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) {R : 𝓗 →L[ℂ] 𝓗} (hRc : R * c = c * R) {w : 𝓗} (hw : w ∈ K c) : R w ∈ K c

theorem CommutingRepetition.Resolver.Douglas.K_invariant_star {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) {R : 𝓗 →L[ℂ] 𝓗} (hRc' : star R * c = c * star R) {w : 𝓗} (hw : w ∈ K c) : (star R) w ∈ K c

theorem CommutingRepetition.Resolver.Douglas.Kperp_invariant {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (c : 𝓗 →L[ℂ] 𝓗) {R : 𝓗 →L[ℂ] 𝓗} (hRc' : star R * c = c * star R) {ζ : 𝓗} (hζ : ζ ∈ (K c)ᗮ) : R ζ ∈ (K c)ᗮ

theorem CommutingRepetition.Resolver.Douglas.welldef {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) {η η' : 𝓗} (h : c η = c η') : (x k) η = (x k) η'

noncomputable def CommutingRepetition.Resolver.Douglas.z₀ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) : ↥(↑c).range →L[ℂ] 𝓗

z on range c: c η ↦ x k η.

Equations

• CommutingRepetition.Resolver.Douglas.z₀ hx k = { toFun := fun (v : ↥(↑c).range) => (x k) (CommutingRepetition.Resolver.Douglas.rep c v), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem CommutingRepetition.Resolver.Douglas.z₀_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) (v : ↥(↑c).range) : (z₀ hx k) v = (x k) (rep c v)

theorem CommutingRepetition.Resolver.Douglas.z₀_apply_c {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) (η : 𝓗) : (z₀ hx k) ⟨c η, ⋯⟩ = (x k) η

noncomputable def CommutingRepetition.Resolver.Douglas.zK {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) : ↥(K c) →L[ℂ] 𝓗

z on K, by continuous extension.

Equations

• CommutingRepetition.Resolver.Douglas.zK hx k = (CommutingRepetition.Resolver.Douglas.z₀ hx k).extend (CommutingRepetition.Resolver.Douglas.incl c)

theorem CommutingRepetition.Resolver.Douglas.zK_incl {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) (v : ↥(↑c).range) : (zK hx k) ((incl c) v) = (z₀ hx k) v

noncomputable def CommutingRepetition.Resolver.Douglas.z {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) : 𝓗 →L[ℂ] 𝓗

The Douglas factor z k := zK k ∘ P_K.

Equations

• CommutingRepetition.Resolver.Douglas.z hx k = CommutingRepetition.Resolver.Douglas.zK hx k ∘SL (CommutingRepetition.Resolver.Douglas.K c).orthogonalProjectionOnto

theorem CommutingRepetition.Resolver.Douglas.z_apply_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) {w : 𝓗} (hw : w ∈ K c) : (z hx k) w = (zK hx k) ⟨w, hw⟩

theorem CommutingRepetition.Resolver.Douglas.z_apply_c {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) (η : 𝓗) : (z hx k) (c η) = (x k) η

theorem CommutingRepetition.Resolver.Douglas.z_mul_c {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) : z hx k * c = x k

z k * c = x k.

theorem CommutingRepetition.Resolver.Douglas.z_apply_orthogonal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (k : κ) {ζ : 𝓗} (hζ : ζ ∈ (K c)ᗮ) : (z hx k) ζ = 0

theorem CommutingRepetition.Resolver.Douglas.sum_sq_norm_zK_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (w : ↥(K c)) : ∑ k : κ, ‖(zK hx k) w‖ ^ 2 ≤ ‖w‖ ^ 2

The quadratic bound on K, by density.

theorem CommutingRepetition.Resolver.Douglas.sum_sq_norm_z_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) (ξ : 𝓗) : ∑ k : κ, ‖(z hx k) ξ‖ ^ 2 ≤ ‖ξ‖ ^ 2

theorem CommutingRepetition.Resolver.Douglas.sum_star_z_mul_z_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) : ∑ k : κ, star (z hx k) * z hx k ≤ 1

∑ₖ zₖ* zₖ ≤ 1.

Commutation transport

theorem CommutingRepetition.Resolver.Douglas.z_comm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hx : ∑ k : κ, star (x k) * x k ≤ star c * c) {R : 𝓗 →L[ℂ] 𝓗} (hRc : R * c = c * R) (hRc' : star R * c = c * star R) (hRx : ∀ (k : κ), R * x k = x k * R) (k : κ) : R * z hx k = z hx k * R

The singular-safe POVM

noncomputable def CommutingRepetition.Resolver.Douglas.Z {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) : 𝓗 →L[ℂ] 𝓗

Z := ∑ₖ zₖ* zₖ.

Equations

• CommutingRepetition.Resolver.Douglas.Z hxe = ∑ k : κ, star (CommutingRepetition.Resolver.Douglas.z ⋯ k) * CommutingRepetition.Resolver.Douglas.z ⋯ k

theorem CommutingRepetition.Resolver.Douglas.Z_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) : Z hxe ≤ 1

theorem CommutingRepetition.Resolver.Douglas.one_sub_Z_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) : 0 ≤ 1 - Z hxe

theorem CommutingRepetition.Resolver.Douglas.star_c_mul_Z_mul_c {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) : star c * Z hxe * c = star c * c

theorem CommutingRepetition.Resolver.Douglas.star_c_mul_one_sub_Z_mul_c {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) : star c * (1 - Z hxe) * c = 0

noncomputable def CommutingRepetition.Resolver.Douglas.povm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {A' : Type u_3} [DecidableEq A'] (lab : κ → A') (a₀ : A') {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) (a : A') : 𝓗 →L[ℂ] 𝓗

The POVM element for the answer a: the squares of the factors labelled a, plus the defect 1 − Z on the fallback answer.

Equations

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

theorem CommutingRepetition.Resolver.Douglas.povm_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {A' : Type u_3} [Fintype A'] [DecidableEq A'] (lab : κ → A') (a₀ : A') {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) (a : A') : 0 ≤ povm lab a₀ hxe a

theorem CommutingRepetition.Resolver.Douglas.sum_povm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {A' : Type u_3} [Fintype A'] [DecidableEq A'] (lab : κ → A') (a₀ : A') {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) : ∑ a : A', povm lab a₀ hxe a = 1

theorem CommutingRepetition.Resolver.Douglas.star_c_mul_povm_mul_c {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {κ : Type u_2} [Fintype κ] {A' : Type u_3} [Fintype A'] [DecidableEq A'] (lab : κ → A') (a₀ : A') {c : 𝓗 →L[ℂ] 𝓗} {x : κ → 𝓗 →L[ℂ] 𝓗} (hxe : ∑ k : κ, star (x k) * x k = star c * c) (a : A') : star c * povm lab a₀ hxe a * c = ∑ k : κ, if lab k = a then star (x k) * x k else 0