def CommutingRepetition.Density.IsTraceClassFunctional {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (φ : (K →L[ℂ] K) →ₗ[ℂ] ℂ) : Prop

A functional on B(K) of trace-class form ∑ ⟪vₖ, T wₖ⟫ with ∑ ‖vₖ‖‖wₖ‖ < ∞ (these are exactly the normal functionals).

Equations

• CommutingRepetition.Density.IsTraceClassFunctional φ = ∃ (v : ℕ → K) (w : ℕ → K), (Summable fun (i : ℕ) => ‖v i‖ * ‖w i‖) ∧ ∀ (T : K →L[ℂ] K), φ T = ∑' (i : ℕ), inner ℂ (v i) (T (w i))

theorem CommutingRepetition.Density.IsTraceClassFunctional.smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {φ : (K →L[ℂ] K) →ₗ[ℂ] ℂ} (hφ : IsTraceClassFunctional φ) (c : ℂ) : IsTraceClassFunctional (c • φ)

noncomputable def CommutingRepetition.Density.nv {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (u : ℕ → K) (k : ℕ) : K

The normalized sequence uₖ / (1 + ‖uₖ‖).

Equations

• CommutingRepetition.Density.nv u k = ↑(1 + ‖u k‖)⁻¹ • u k

theorem CommutingRepetition.Density.norm_nv_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (k : ℕ) : ‖nv u k‖ ≤ 1

theorem CommutingRepetition.Density.map_nv_eq_zero_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) (k : ℕ) : T (nv u k) = 0 ↔ T (u k) = 0

noncomputable def CommutingRepetition.Density.wt (k : ℕ) : ℝ

The weights 2⁻ᵏ.

Equations

• CommutingRepetition.Density.wt k = (1 / 2) ^ k

theorem CommutingRepetition.Density.wt_nonneg (k : ℕ) : 0 ≤ wt k

theorem CommutingRepetition.Density.wt_pos (k : ℕ) : 0 < wt k

theorem CommutingRepetition.Density.summable_wt : Summable wt

theorem CommutingRepetition.Density.norm_inner_nv_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) (k : ℕ) : ‖inner ℂ (nv u k) (T (nv u k))‖ ≤ ‖T‖

theorem CommutingRepetition.Density.summable_term {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : Summable fun (k : ℕ) => ↑(wt k) * inner ℂ (nv u k) (T (nv u k))

noncomputable def CommutingRepetition.Density.preState {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) : (K →L[ℂ] K) →ₗ[ℂ] ℂ

The unnormalized functional T ↦ ∑ₖ 2⁻ᵏ ⟪vₖ, T vₖ⟫.

Equations

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

theorem CommutingRepetition.Density.preState_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : (preState u) T = ∑' (k : ℕ), ↑(wt k) * inner ℂ (nv u k) (T (nv u k))

theorem CommutingRepetition.Density.summable_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : Summable fun (k : ℕ) => wt k * ‖T (nv u k)‖ ^ 2

theorem CommutingRepetition.Density.preState_star_mul_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : (preState u) (star T * T) = ↑(∑' (k : ℕ), wt k * ‖T (nv u k)‖ ^ 2)

noncomputable def CommutingRepetition.Density.Z {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (u : ℕ → K) : ℝ

The normalization constant Z = ∑ₖ 2⁻ᵏ ‖vₖ‖².

Equations

• CommutingRepetition.Density.Z u = ∑' (k : ℕ), CommutingRepetition.Density.wt k * ‖CommutingRepetition.Density.nv u k‖ ^ 2

theorem CommutingRepetition.Density.Z_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) : 0 ≤ Z u

theorem CommutingRepetition.Density.Z_pos {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (hne : ∃ (k : ℕ), u k ≠ 0) : 0 < Z u

theorem CommutingRepetition.Density.preState_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) : (preState u) 1 = ↑(Z u)

noncomputable def CommutingRepetition.Density.faithfulState {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) : (K →L[ℂ] K) →ₗ[ℂ] ℂ

The faithful state Z⁻¹ · preState.

Equations

• CommutingRepetition.Density.faithfulState u = ↑(CommutingRepetition.Density.Z u)⁻¹ • CommutingRepetition.Density.preState u

theorem CommutingRepetition.Density.faithfulState_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : (faithfulState u) T = ↑(Z u)⁻¹ * (preState u) T

theorem CommutingRepetition.Density.faithfulState_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (hne : ∃ (k : ℕ), u k ≠ 0) : (faithfulState u) 1 = 1

theorem CommutingRepetition.Density.faithfulState_star_mul_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : (faithfulState u) (star T * T) = ↑((Z u)⁻¹ * ∑' (k : ℕ), wt k * ‖T (nv u k)‖ ^ 2)

theorem CommutingRepetition.Density.faithfulState_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (T : K →L[ℂ] K) : 0 ≤ (faithfulState u) (star T * T)

theorem CommutingRepetition.Density.faithfulState_faithful {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (hu : DenseRange u) (hne : ∃ (k : ℕ), u k ≠ 0) (T : K →L[ℂ] K) (h : (faithfulState u) (star T * T) = 0) : T = 0

Faithfulness: φ(T*T) = 0 forces T = 0, since u is dense.

theorem CommutingRepetition.Density.faithfulState_traceClass {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) : IsTraceClassFunctional (faithfulState u)

theorem CommutingRepetition.Density.norm_faithfulState_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : ℕ → K) (hne : ∃ (k : ℕ), u k ≠ 0) (T : K →L[ℂ] K) : ‖(faithfulState u) T‖ ≤ ‖T‖

|φ(T)| ≤ ‖T‖.