The weights

noncomputable def CommutingRepetition.Density.wgt (ε : ℝ) : ℕ → ℝ

The probability weight w₀ = 1 − ε, w_{k+1} = ε·2^{-(k+1)}.

Equations

• CommutingRepetition.Density.wgt ε 0 = 1 - ε
• CommutingRepetition.Density.wgt ε k.succ = ε * (1 / 2) ^ (k + 1)

theorem CommutingRepetition.Density.wgt_zero (ε : ℝ) : wgt ε 0 = 1 - ε

theorem CommutingRepetition.Density.wgt_succ (ε : ℝ) (k : ℕ) : wgt ε (k + 1) = ε * (1 / 2) ^ (k + 1)

theorem CommutingRepetition.Density.wgt_pos {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (k : ℕ) : 0 < wgt ε k

theorem CommutingRepetition.Density.summable_wgt_succ {ε : ℝ} : Summable fun (k : ℕ) => wgt ε (k + 1)

theorem CommutingRepetition.Density.tsum_wgt_succ {ε : ℝ} : ∑' (k : ℕ), wgt ε (k + 1) = ε

theorem CommutingRepetition.Density.summable_wgt {ε : ℝ} : Summable (wgt ε)

The sequence

noncomputable def CommutingRepetition.Density.vseq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (u : ℕ → H) : ℕ → H

The unit-ball sequence v₀ = ψ, v_{k+1} = nv uₖ.

Equations

• CommutingRepetition.Density.vseq ψ u 0 = ψ
• CommutingRepetition.Density.vseq ψ u k.succ = CommutingRepetition.Density.nv u k

theorem CommutingRepetition.Density.vseq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) : vseq ψ u 0 = ψ

theorem CommutingRepetition.Density.vseq_succ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (k : ℕ) : vseq ψ u (k + 1) = nv u k

theorem CommutingRepetition.Density.norm_vseq_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) (k : ℕ) : ‖vseq ψ u k‖ ≤ 1

noncomputable def CommutingRepetition.Density.Zc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (u : ℕ → H) (ε : ℝ) : ℝ

The normalizing constant Z = ∑ₖ wₖ ‖vₖ‖².

Equations

• CommutingRepetition.Density.Zc ψ u ε = ∑' (k : ℕ), CommutingRepetition.Density.wgt ε k * ‖CommutingRepetition.Density.vseq ψ u k‖ ^ 2

theorem CommutingRepetition.Density.wgt_mul_norm_sq_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (k : ℕ) : wgt ε k * ‖vseq ψ u k‖ ^ 2 ≤ wgt ε k

theorem CommutingRepetition.Density.wgt_mul_norm_sq_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (k : ℕ) : 0 ≤ wgt ε k * ‖vseq ψ u k‖ ^ 2

theorem CommutingRepetition.Density.summable_wgt_mul_norm_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : Summable fun (k : ℕ) => wgt ε k * ‖vseq ψ u k‖ ^ 2

theorem CommutingRepetition.Density.tsum_wgt (ε : ℝ) : ∑' (k : ℕ), wgt ε k = 1

theorem CommutingRepetition.Density.Zc_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : Zc ψ u ε ≤ 1

theorem CommutingRepetition.Density.Zc_ge {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : 1 - ε ≤ Zc ψ u ε

theorem CommutingRepetition.Density.Zc_pos {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : 0 < Zc ψ u ε

noncomputable def CommutingRepetition.Density.gvec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (u : ℕ → H) (ε : ℝ) (k : ℕ) : H

The sequence gₖ = √(wₖ/Z) • vₖ realizing the perturbed state.

Equations

• CommutingRepetition.Density.gvec ψ u ε k = ↑√(CommutingRepetition.Density.wgt ε k / CommutingRepetition.Density.Zc ψ u ε) • CommutingRepetition.Density.vseq ψ u k

theorem CommutingRepetition.Density.norm_gvec_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (k : ℕ) : ‖gvec ψ u ε k‖ ^ 2 = wgt ε k / Zc ψ u ε * ‖vseq ψ u k‖ ^ 2

theorem CommutingRepetition.Density.summable_norm_gvec_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : Summable fun (k : ℕ) => ‖gvec ψ u ε k‖ ^ 2

theorem CommutingRepetition.Density.tsum_norm_gvec_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : ∑' (k : ℕ), ‖gvec ψ u ε k‖ ^ 2 = 1

The perturbed state

noncomputable def CommutingRepetition.Density.gvecState {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (u : ℕ → H) (ε : ℝ) (T : H →L[ℂ] H) : ℂ

The state φ(T) = ∑ₖ ⟪gₖ, T gₖ⟫.

Equations

• CommutingRepetition.Density.gvecState ψ u ε T = ∑' (k : ℕ), inner ℂ (CommutingRepetition.Density.gvec ψ u ε k) (T (CommutingRepetition.Density.gvec ψ u ε k))

theorem CommutingRepetition.Density.norm_inner_gvec_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (ε : ℝ) (T : H →L[ℂ] H) (k : ℕ) : ‖inner ℂ (gvec ψ u ε k) (T (gvec ψ u ε k))‖ ≤ ‖T‖ * ‖gvec ψ u ε k‖ ^ 2

theorem CommutingRepetition.Density.summable_inner_gvec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (T : H →L[ℂ] H) : Summable fun (k : ℕ) => inner ℂ (gvec ψ u ε k) (T (gvec ψ u ε k))

theorem CommutingRepetition.Density.inner_gvec_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (ε : ℝ) (k : ℕ) : inner ℂ (gvec ψ u ε k) (1 (gvec ψ u ε k)) = ↑(‖gvec ψ u ε k‖ ^ 2)

theorem CommutingRepetition.Density.gvecState_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : gvecState ψ u ε 1 = 1

Faithfulness

theorem CommutingRepetition.Density.inner_gvec_star_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (ε : ℝ) (T : H →L[ℂ] H) (k : ℕ) : inner ℂ (gvec ψ u ε k) ((star T * T) (gvec ψ u ε k)) = ↑(‖T (gvec ψ u ε k)‖ ^ 2)

theorem CommutingRepetition.Density.gvec_ne_zero_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) {ε : ℝ} (hψ : ‖ψ‖ = 1) (hε0 : 0 < ε) (hε1 : ε < 1) (k : ℕ) (T : H →L[ℂ] H) (h : T (gvec ψ u ε k) = 0) : T (vseq ψ u k) = 0

theorem CommutingRepetition.Density.gvecState_faithful {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (hu : DenseRange u) (T : H →L[ℂ] H) (h : gvecState ψ u ε (star T * T) = 0) : T = 0

Closeness to the vector state of ψ

theorem CommutingRepetition.Density.tsum_norm_gvec_sq_succ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : ∑' (k : ℕ), ‖gvec ψ u ε (k + 1)‖ ^ 2 = 1 - (1 - ε) / Zc ψ u ε

theorem CommutingRepetition.Density.tsum_norm_gvec_sq_succ_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : ∑' (k : ℕ), ‖gvec ψ u ε (k + 1)‖ ^ 2 ≤ ε / (1 - ε)

theorem CommutingRepetition.Density.norm_gvecState_sub_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (u : ℕ → H) (hψ : ‖ψ‖ = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (T : H →L[ℂ] H) : ‖gvecState ψ u ε T - inner ℂ ψ (T ψ)‖ ≤ 2 * ε * ‖T‖ / (1 - ε)

The perturbed state is 2ε/(1−ε)-close to the vector state of ψ on the unit ball of B(H).