English
The map of a completely positive map on a nonnegative matrix is nonnegative.
Русский
Отображение полностью положительного отображения на неотрицатной матрице даёт неотрицательное изображение.
LaTeX
$$map_cstarMatrix_nonneg {n} (φ : CompletelyPositiveMap A₁ A₂) (M : CStarMatrix n n A₁) (hM : 0 ≤ M) : 0 ≤ M.map φ$$
Lean4
theorem map_cstarMatrix_nonneg {n : Type*} [Fintype n] (φ : A₁ →CP A₂) (M : CStarMatrix n n A₁) (hM : 0 ≤ M) :
0 ≤ M.map φ := by
let k := Fintype.card n
let e := Fintype.equivFinOfCardEq (rfl : Fintype.card n = k)
have hmain : 0 ≤ (reindexₐ ℂ A₁ e M).mapₗ (φ : A₁ →ₗ[ℂ] A₂) :=
by
simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk]
exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)
rw [← mapₗ_reindexₐ] at hmain
have hrw : reindexₐ ℂ A₂ e.symm ((reindexₐ ℂ A₂ e) (M.map (φ : A₁ → A₂))) = M.map (φ : A₁ → A₂) := by simp
rw [← hrw]
exact map_nonneg _ hmain
