LeanPool.Monlib4.QuantumGraph.OfClassicalGraph

Imported Lean Pool material for LeanPool.Monlib4.QuantumGraph.OfClassicalGraph.

@[implicit_reducible]

noncomputable instance instStarAlgebraPiQComplex {n : Type u_1} : starAlgebra (PiQ fun (x : n) => ℂ)

Equations

• instStarAlgebraPiQComplex = piStarAlgebra

@[implicit_reducible]

noncomputable instance instQuantumSetPiQComplexOfFintype {n : Type u_1} [Fintype n] : QuantumSet (PiQ fun (x : n) => ℂ)

Equations

• instQuantumSetPiQComplexOfFintype = inferInstance

theorem EuclideanSpace.comul_eq {n : Type u_1} [Fintype n] [DecidableEq n] (x : PiQ fun (x : n) => ℂ) : have e := fun (i : n) => PiLp.single 2 i 1; CoalgebraStruct.comul x = ∑ i : n, x.ofLp i • e i ⊗ₜ[ℂ] e i

theorem SimpleGraph.toQuantumGraph {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : QuantumGraph (EuclideanSpace ℂ V) (Matrix.toEuclideanLin (adjMatrix ℂ G))

a finite simple graph is a quantum graph

theorem quantumGraph_numOfEdges_of_classical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : QuantumGraph.NumOfEdges (Matrix.toEuclideanLin (SimpleGraph.adjMatrix ℂ G)) = ∑ i : V, ∑ j : V, SimpleGraph.adjMatrix ℂ G i j

theorem SimpleGraph.conjTranspose_adjMatrix {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [NonAssocSemiring α] [StarRing α] : (adjMatrix α G).conjTranspose = adjMatrix α G

theorem SimpleGraph.adjMatrix_toEuclideanLin_isReal {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : LinearMap.IsReal (Matrix.toEuclideanLin (adjMatrix ℂ G))

theorem SimpleGraph.adjMatrix_toEuclideanLin_symmMap {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : (symmMap ℂ (EuclideanSpace ℂ V) (EuclideanSpace ℂ V)) (Matrix.toEuclideanLin (adjMatrix ℂ G)) = Matrix.toEuclideanLin (adjMatrix ℂ G)

theorem SimpleGraph.adjMatrix_irreflexive {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : Matrix.toEuclideanLin (adjMatrix ℂ G) •ₛ 1 = 0