Bounded strong convergence

def CommutingRepetition.VN.TendstoStrongBdd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_3} (l : Filter ι) (T : ι → H →L[ℂ] H) (L : H →L[ℂ] H) : Prop

T i → L strongly (pointwise) along l, with ‖T i‖ uniformly bounded.

Equations

• CommutingRepetition.VN.TendstoStrongBdd l T L = ((∃ (C : ℝ), ∀ (i : ι), ‖T i‖ ≤ C) ∧ ∀ (ξ : H), Filter.Tendsto (fun (i : ι) => (T i) ξ) l (nhds (L ξ)))

theorem CommutingRepetition.VN.TendstoStrongBdd.bdd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (h : TendstoStrongBdd l T L) : ∃ (C : ℝ), ∀ (i : ι), ‖T i‖ ≤ C

theorem CommutingRepetition.VN.TendstoStrongBdd.tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (ξ : H) : Filter.Tendsto (fun (i : ι) => (T i) ξ) l (nhds (L ξ))

theorem CommutingRepetition.VN.TendstoStrongBdd.const {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} (L : H →L[ℂ] H) : TendstoStrongBdd l (fun (x : ι) => L) L

theorem CommutingRepetition.VN.TendstoStrongBdd.mul_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (A : H →L[ℂ] H) : TendstoStrongBdd l (fun (i : ι) => A * T i) (A * L)

theorem CommutingRepetition.VN.TendstoStrongBdd.mul_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (A : H →L[ℂ] H) : TendstoStrongBdd l (fun (i : ι) => T i * A) (L * A)

theorem CommutingRepetition.VN.TendstoStrongBdd.add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T S : ι → H →L[ℂ] H} {L M : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (h' : TendstoStrongBdd l S M) : TendstoStrongBdd l (fun (i : ι) => T i + S i) (L + M)

theorem CommutingRepetition.VN.TendstoStrongBdd.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (c : ℂ) : TendstoStrongBdd l (fun (i : ι) => c • T i) (c • L)

theorem CommutingRepetition.VN.TendstoStrongBdd.mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} {l : Filter ι} {T S : ι → H →L[ℂ] H} {L M : H →L[ℂ] H} (h : TendstoStrongBdd l T L) (h' : TendstoStrongBdd l S M) : TendstoStrongBdd l (fun (i : ι) => T i * S i) (L * M)

Multiplication is jointly continuous along bounded strongly convergent nets.

Normal functionals and maps

def CommutingRepetition.VN.IsNormalFun {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (φ : (H →L[ℂ] H) → ℂ) : Prop

A functional on B(H) is normal if it is continuous along bounded strongly convergent nets (indexed by a Type).

Equations

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

def CommutingRepetition.VN.IsNormalMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (Φ : (H →L[ℂ] H) → K →L[ℂ] K) : Prop

A map B(H) → B(K) is normal if it preserves bounded strong convergence.

Equations

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

theorem CommutingRepetition.VN.IsNormalFun.add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ ψ : (H →L[ℂ] H) → ℂ} (hφ : IsNormalFun φ) (hψ : IsNormalFun ψ) : IsNormalFun fun (T : H →L[ℂ] H) => φ T + ψ T

theorem CommutingRepetition.VN.IsNormalFun.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) → ℂ} (hφ : IsNormalFun φ) (c : ℂ) : IsNormalFun fun (T : H →L[ℂ] H) => c * φ T

theorem CommutingRepetition.VN.IsNormalFun.const {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : ℂ) : IsNormalFun fun (x : H →L[ℂ] H) => c

theorem CommutingRepetition.VN.IsNormalFun.comp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {φ : (H →L[ℂ] H) → ℂ} (hφ : IsNormalFun φ) {Φ : (K →L[ℂ] K) → H →L[ℂ] H} (hΦ : IsNormalMap Φ) : IsNormalFun fun (T : K →L[ℂ] K) => φ (Φ T)

theorem CommutingRepetition.VN.IsNormalFun.inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ η : H) : IsNormalFun fun (T : H →L[ℂ] H) => Inner.inner ℂ ξ (T η)

The vector functionals T ↦ ⟪ξ, T η⟫ are normal.

theorem CommutingRepetition.VN.IsNormalMap.id {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : IsNormalMap fun (T : H →L[ℂ] H) => T

theorem CommutingRepetition.VN.IsNormalMap.comp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Φ : (H →L[ℂ] H) → K →L[ℂ] K} {K' : Type u_3} [NormedAddCommGroup K'] [InnerProductSpace ℂ K'] [CompleteSpace K'] {Ψ : (K →L[ℂ] K) → K' →L[ℂ] K'} (hΨ : IsNormalMap Ψ) (hΦ : IsNormalMap Φ) : IsNormalMap fun (T : H →L[ℂ] H) => Ψ (Φ T)

Trace-class functionals are normal

theorem CommutingRepetition.VN.isNormalFun_of_traceClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : Density.IsTraceClassFunctional φ) : IsNormalFun ⇑φ