mathlib3 documentation

monlib / quantum_graph.to_projections

Quantum graphs as projections #

This file contains the definition of a quantum graph as a projection, and the proof that the

source
noncomputable def block_diag'_kronecker_equiv {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} (hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map) :
matrix (Σ (i : p), n i × n i) (Σ (i : p), n i × n i) ℂ ≃ₗ[ℂ] tensor_product ℂ {x // x.is_block_diagonal} {x // x.is_block_diagonal}
Equations
source
theorem linear_equiv.coe_one {R : Type u_1} [semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] :
↑1 = 1
source
theorem matrix.conj_conj_transpose' {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [has_involutive_star R] (A : matrix n₁ n₂ R) :
A.conj_transpose.transpose.conj_transpose = A.transpose
source
theorem to_matrix_mul_left_mul_right_adjoint {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} (hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map) (x y : Π (i : p), matrix (n i) (n i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) (linear_map.mul_left ℂ x * ⇑linear_map.adjoint (linear_map.mul_right ℂ y)) = matrix.block_diagonal' (λ (i : p), matrix.kronecker_map has_mul.mul (x i) (⇑(_.sig (1 / 2)) (y i)).conj)
source
def pi.linear_map.apply {ι₁ : Type u_1} {ι₂ : Type u_2} {E₁ : ι₁ → Type u_3} [decidable_eq ι₁] [fintype ι₁] [Π (i : ι₁), add_comm_monoid (E₁ i)] [Π (i : ι₁), module ℂ (E₁ i)] {E₂ : ι₂ → Type u_4} [Π (i : ι₂), add_comm_monoid (E₂ i)] [Π (i : ι₂), module ℂ (E₂ i)] (i : ι₁) (j : ι₂) :
((Π (a : ι₁), E₁ a) →ₗ[ℂ] Π (a : ι₂), E₂ a) →ₗ[ℂ] E₁ i →ₗ[ℂ] E₂ j
Equations
source
@[simp]
theorem pi.linear_map.apply_apply_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {E₁ : ι₁ → Type u_3} [decidable_eq ι₁] [fintype ι₁] [Π (i : ι₁), add_comm_monoid (E₁ i)] [Π (i : ι₁), module ℂ (E₁ i)] {E₂ : ι₂ → Type u_4} [Π (i : ι₂), add_comm_monoid (E₂ i)] [Π (i : ι₂), module ℂ (E₂ i)] (i : ι₁) (j : ι₂) (x : (Π (a : ι₁), E₁ a) →ₗ[ℂ] Π (a : ι₂), E₂ a) (a : E₁ i) :
⇑(⇑(pi.linear_map.apply i j) x) a = ⇑x (⇑(linear_map.single i) a) j
source
theorem rank_one_Psi_transpose_to_lin {n : Type u_1} [decidable_eq n] [fintype n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ) :
⇑(_.to_matrix.symm) (⇑tensor_product.to_kronecker (⇑(tensor_product.map 1 (matrix.transpose_alg_equiv n ℂ ℂ).symm.to_linear_map) (⇑(_.Psi 0 (1 / 2)) ↑(rank_one x y)))) = linear_map.mul_left ℂ x * ⇑linear_map.adjoint (linear_map.mul_right ℂ y)
source
theorem rank_one_to_matrix_transpose_Psi_symm {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix p p ℂ) :
⇑((_.Psi 0 (1 / 2)).symm) (⇑(tensor_product.map 1 (matrix.transpose_alg_equiv p ℂ ℂ).to_linear_map) (⇑matrix.kronecker_to_tensor_product (⇑(_.to_matrix) ↑(rank_one x y)))) = linear_map.mul_left ℂ (x.mul φ.matrix) * ⇑linear_map.adjoint (linear_map.mul_right ℂ (φ.matrix.mul y))
source
theorem orthogonal_projection_iff_lm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] [finite_dimensional 𝕜 E] {p : E →ₗ[𝕜] E} :
(∃ (U : submodule 𝕜 E), ↑(orthogonal_projection' U) = p) ↔ is_self_adjoint p ∧ is_idempotent_elem p
source
theorem matrix.conj_eq_transpose_conj_transpose {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [has_star R] (A : matrix n₁ n₂ R) :
A.conj = A.transpose.conj_transpose
source
theorem matrix.conj_eq_conj_transpose_transpose {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [has_star R] (A : matrix n₁ n₂ R) :
A.conj = A.conj_transpose.transpose
source
noncomputable def one_map_transpose {p : Type u_1} [fintype p] [decidable_eq p] :
tensor_product ℂ (matrix p p ℂ) (matrix p p ℂ)ᵐᵒᵖ ≃⋆ₐ[ℂ] matrix (p × p) (p × p) ℂ
Equations
source
theorem one_map_transpose_eq {p : Type u_1} [fintype p] [decidable_eq p] (x : tensor_product ℂ (matrix p p ℂ) (matrix p p ℂ)ᵐᵒᵖ) :
⇑one_map_transpose x = ⇑tensor_product.to_kronecker (⇑(tensor_product.map 1 (matrix.transpose_alg_equiv p ℂ ℂ).symm.to_linear_map) x)
source
theorem one_map_transpose_symm_eq {p : Type u_1} [fintype p] [decidable_eq p] (x : matrix (p × p) (p × p) ℂ) :
⇑(one_map_transpose.symm) x = ⇑(tensor_product.map 1 (matrix.transpose_alg_equiv p ℂ ℂ).to_linear_map) (⇑matrix.kronecker_to_tensor_product x)
source
theorem one_map_transpose_apply {p : Type u_1} [fintype p] [decidable_eq p] (x y : matrix p p ℂ) :
⇑one_map_transpose (x ⊗ₜ[ℂ] mul_opposite.op y) = matrix.kronecker_map has_mul.mul x y.transpose
source
theorem to_matrix''_map_star {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
⇑(_.to_matrix) (⇑linear_map.adjoint x) = has_star.star (⇑(_.to_matrix) x)
source
theorem to_matrix''_symm_map_star {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix (p × p) (p × p) ℂ) :
⇑(_.to_matrix.symm) (has_star.star x) = ⇑linear_map.adjoint (⇑(_.to_matrix.symm) x)
source
theorem qam.idempotent_and_real_iff_exists_ortho_proj {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
⇑(⇑(qam.refl_idempotent _) A) A = A ∧ A.is_real ↔ ∃ (U : submodule ℂ (matrix p p ℂ)), ↑(orthogonal_projection' U) = ⇑(_.to_matrix.symm) (⇑tensor_product.to_kronecker (⇑(tensor_product.map 1 (matrix.transpose_alg_equiv p ℂ ℂ).symm.to_linear_map) (⇑(_.Psi 0 (1 / 2)) A)))
source
noncomputable def qam.submodule_of_idempotent_and_real {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA1 : ⇑(⇑(qam.refl_idempotent qam.submodule_of_idempotent_and_real._proof_1) A) A = A) (hA2 : A.is_real) :
submodule ℂ (matrix p p ℂ)
Equations
source
theorem qam.orthogonal_projection'_eq {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA1 : ⇑(⇑(qam.refl_idempotent _) A) A = A) (hA2 : A.is_real) :
↑(orthogonal_projection' (qam.submodule_of_idempotent_and_real hA1 hA2)) = ⇑(_.to_matrix.symm) (⇑tensor_product.to_kronecker (⇑(tensor_product.map 1 (matrix.transpose_alg_equiv p ℂ ℂ).symm.to_linear_map) (⇑(_.Psi 0 (1 / 2)) A)))
source
noncomputable def qam.onb_of_idempotent_and_real {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA1 : ⇑(⇑(qam.refl_idempotent qam.onb_of_idempotent_and_real._proof_1) A) A = A) (hA2 : A.is_real) :
orthonormal_basis (fin (finite_dimensional.finrank ℂ ↥(qam.submodule_of_idempotent_and_real hA1 hA2))) ℂ ↥(qam.submodule_of_idempotent_and_real hA1 hA2)
Equations
source
theorem qam.idempotent_and_real.eq {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA1 : ⇑(⇑(qam.refl_idempotent _) A) A = A) (hA2 : A.is_real) :
A = finset.univ.sum (λ (i : fin (finite_dimensional.finrank ℂ ↥(qam.submodule_of_idempotent_and_real hA1 hA2))), linear_map.mul_left ℂ (↑(⇑(qam.onb_of_idempotent_and_real hA1 hA2) i).mul φ.matrix) * ⇑linear_map.adjoint (linear_map.mul_right ℂ (φ.matrix.mul ↑(⇑(qam.onb_of_idempotent_and_real hA1 hA2) i))))
source
def real_qam {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} (hφ : φ.is_faithful_pos_map) (A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
Prop
Equations
source
theorem real_qam.add_iff {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A B : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA : real_qam _ A) (hB : real_qam _ B) :
real_qam _ (A + B) ↔ ⇑(⇑(qam.refl_idempotent _) A) B + ⇑(⇑(qam.refl_idempotent _) B) A = 0
source
def real_qam.zero {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
real_qam _ 0
source
@[instance]
noncomputable def real_qam.has_zero {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
has_zero {x // real_qam real_qam.has_zero._proof_1 x}
Equations
source
theorem qam.refl_idempotent_zero {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (a : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
⇑(⇑(qam.refl_idempotent _) a) 0 = 0
source
theorem qam.zero_refl_idempotent {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (a : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
⇑(⇑(qam.refl_idempotent _) 0) a = 0
source
noncomputable def real_qam.edges {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hx : real_qam real_qam.edges._proof_1 x) :
ℕ
Equations
source
noncomputable def real_qam.edges' {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
{x // real_qam real_qam.edges'._proof_1 x} → ℕ
Equations
source
theorem real_qam.edges_eq {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA : real_qam _ A) :
↑(hA.edges) = (⇑A (φ.matrix)⁻¹).trace
source
theorem complete_graph_real_qam {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
real_qam _ (qam.complete_graph (matrix p p ℂ))
source
theorem qam.complete_graph_edges {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
complete_graph_real_qam.edges = finite_dimensional.finrank ℂ ↥⊤
source
theorem qam.trivial_graph_real_qam {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial p] :
real_qam _ (qam.trivial_graph hφ rfl)
source
theorem qam.trivial_graph_edges {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial p] :
qam.trivial_graph_real_qam.edges = 1
source
theorem real_qam.edges_eq_zero_iff {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA : real_qam _ A) :
hA.edges = 0 ↔ A = 0
source
theorem orthogonal_projection_of_top {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space ↥⊤] :
orthogonal_projection' ⊤ = 1
source
theorem Psi_apply_complete_graph {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {t s : ℝ} :
⇑(_.Psi t s) ↑(rank_one 1 1) = 1
source
theorem real_qam.edges_eq_dim_iff {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA : real_qam _ A) :
hA.edges = finite_dimensional.finrank ℂ ↥⊤ ↔ A = ↑(rank_one 1 1)
source
theorem real_qam.edges_eq_one_iff {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hA : real_qam _ A) :
hA.edges = 1 ↔ ∃ (x : {x // x ≠ 0}), A = (1 / ↑‖↑x‖ ^ 2) • (linear_map.mul_left ℂ (↑x.mul φ.matrix) * ⇑linear_map.adjoint (linear_map.mul_right ℂ (φ.matrix.mul ↑x)))