Stinespring dilation: simple considerations involving 1x1 matrices

theorem Complex.sqrt_nonneg (α : ℂ) (h : 0 ≤ α) : 0 ≤ α.sqrt

noncomputable def Complex.sqrt' (z : ℂ) : ℂ

Equations

• z.sqrt' = z ^ (1 / 2)

theorem complex_sq_sqrt {x : ℂ} : x.sqrt ^ 2 = x

theorem complex_sqrt_nonneg {x : ℂ} (hx : 0 ≤ x) : 0 ≤ x.sqrt

theorem matrix_1x1_sqrt (α : ℂ) (h₀ : 0 ≤ α) : CFC.sqrt !![α] = !![α.sqrt]

theorem matrix_sqrt_eq_complex_sqrt (α : ℂ) (h₀ : 0 ≤ α) : CFC.sqrt !![α] 0 0 = α.sqrt

theorem krausCompletion_I' (z : ℂ) (hz : star z * z ≤ 1) : have K := fun (x : Fin 1) => !![z]; (krausCompletion K).conjTranspose * krausCompletion K = 1

Feb 5, 2026 The Stinespring dilation as an isometry, in the case where 𝓚 is a single complex number.