theorem schurProjection.innerOne_map_one_nonneg {A : Type u_1} {B : Type u_2} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] [PartialOrder A] [PartialOrder B] [StarOrderedRing A] [StarOrderedRing B] (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) (h₂ : ∀ ⦃a : B⦄, 0 ≤ a ↔ ∃ (b : B), a = star b * b) {f : A →ₗ[ℂ] B} (h : schurProjection f) : 0 ≤ inner 1 (f 1)

theorem QuantumGraph.real_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.Real A f ↔ f •ₛ f = f ∧ LinearMap.IsReal f

theorem quantumGraph_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph A f ↔ f •ₛ f = f

theorem QuantumGraph.toSubset_iff {A : Type u_1} [starAlgebra A] [h : QuantumSet A] {f : A →ₗ[ℂ] A} (r : ℝ) : QuantumGraph (QuantumSet.subset r A) (f.toSubsetQuantumSet r r) ↔ QuantumGraph A f

theorem QuantumGraph.real_toSubset_iff {A : Type u_1} [starAlgebra A] [h : QuantumSet A] {f : A →ₗ[ℂ] A} (r : ℝ) : QuantumGraph.Real (QuantumSet.subset r A) (f.toSubsetQuantumSet r r) ↔ QuantumGraph.Real A f

theorem QuantumGraph.Real.innerOne_map_one_nonneg {A : Type u_1} [starAlgebra A] [hA : QuantumSet A] [PartialOrder A] [StarOrderedRing A] (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) : 0 ≤ inner 1 (f 1)

theorem QuantumGraph.Real.innerOne_map_one_eq_zero_iff_of_kms {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) [kms : Fact (k A = -(1 / 2))] : inner 1 (f 1) = 0 ↔ f = 0

theorem QuantumGraph.Real.innerOne_map_one_eq_zero_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) : inner 1 (f 1) = 0 ↔ f = 0

theorem QuantumGraph.real_iff_complement'_real {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.Real A f ↔ QuantumGraph.Real A (Qam.complement' f)

theorem QuantumGraph.Real.innerOne_map_one_eq_norm_pow_four_iff_of_kms {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) [kms : Fact (k A = -(1 / 2))] : inner 1 (f 1) = ↑‖1‖ ^ 4 ↔ f = ↑(((rankOne ℂ) 1) 1)

theorem QuantumGraph.Real.innerOne_map_one_eq_norm_pow_four_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) : inner 1 (f 1) = ↑‖1‖ ^ 4 ↔ f = ↑(((rankOne ℂ) 1) 1)

noncomputable def QuantumGraph.outDegree {A : Type u_1} [starAlgebra A] [QuantumSet A] : (A →ₗ[ℂ] A) →ₗ[ℂ] A →ₗ[ℂ] A

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumGraph.outDegree_apply {A : Type u_1} [starAlgebra A] [QuantumSet A] (f : A →ₗ[ℂ] A) : QuantumGraph.outDegree f = LinearMap.mul' ℂ A ∘ₗ LinearMap.rTensor A f ∘ₗ LinearMap.rTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.lid ℂ A).symm

theorem QuantumGraph.outDegree_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.outDegree f = lmul (f 1)

noncomputable def QuantumGraph.inDegree {A : Type u_1} [starAlgebra A] [QuantumSet A] : (A →ₗ[ℂ] A) →ₗ⋆[ℂ] A →ₗ[ℂ] A

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumGraph.inDegree_apply {A : Type u_1} [starAlgebra A] [QuantumSet A] (f : A →ₗ[ℂ] A) : QuantumGraph.inDegree f = LinearMap.mul' ℂ A ∘ₗ LinearMap.lTensor A (LinearMap.adjoint f) ∘ₗ LinearMap.lTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.rid ℂ A).symm

theorem QuantumGraph.inDegree_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.inDegree f = rmul ((LinearMap.adjoint f) 1)

theorem QuantumGraph.outDegree_real_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {x : A →ₗ[ℂ] A} : (QuantumGraph.outDegree x).real = QuantumGraph.inDegree ((symmMap ℂ A A) x)

theorem QuantumGraph.inDegree_real_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {x : A →ₗ[ℂ] A} : (QuantumGraph.inDegree x).real = QuantumGraph.outDegree ((symmMap ℂ A A).symm x)

theorem QuantumGraph.outDegree_eq' {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.outDegree f = ↑(TensorProduct.lid ℂ A) ∘ₗ LinearMap.rTensor A Coalgebra.counit ∘ₗ ↑(PhiMap f) ∘ₗ LinearMap.rTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.lid ℂ A).symm

theorem QuantumGraph.inDegree_eq' {A : Type u_1} [starAlgebra A] [QuantumSet A] (gns : k A = 0) {f : A →ₗ[ℂ] A} : QuantumGraph.inDegree f = ↑(TensorProduct.rid ℂ A) ∘ₗ LinearMap.lTensor A Coalgebra.counit ∘ₗ ↑(PhiMap f.real) ∘ₗ LinearMap.lTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.rid ℂ A).symm

theorem QuantumGraph.outDegree_apply_schurMul {A : Type u_1} [starAlgebra A] [QuantumSet A] (gns : k A = 0) (f₁ : A →ₗ[ℂ] A) (f₂ : A →ₗ[ℂ] A) : QuantumGraph.outDegree (f₁ •ₛ f₂) = (f₁ ∘ₗ (symmMap ℂ A A) f₂) •ₛ 1

theorem QuantumGraph.inDegree_apply_schurMul {A : Type u_1} [starAlgebra A] [QuantumSet A] (gns : k A = 0) (f₁ : A →ₗ[ℂ] A) (f₂ : A →ₗ[ℂ] A) : QuantumGraph.inDegree (f₁ •ₛ f₂) = 1 •ₛ LinearMap.adjoint f₂ ∘ₗ f₁.real

def QuantumGraph.IsRegular {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (_h : QuantumGraph A f) (d : ℂ) : Prop

Equations

• _h.IsRegular d = (f 1 = d • 1 ∧ (LinearMap.adjoint f) 1 = d • 1)

theorem QuantumGraph.degree_is_real_of_real {A : Type u_1} [starAlgebra A] [QuantumSet A] [Nontrivial A] {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) (d : ℂ) (h2 : ⋯.IsRegular d) : d = ↑d.re

theorem PhiMap_apply_one_one {A : Type u_1} {B : Type u_2} [starAlgebra B] [starAlgebra A] [QuantumSet A] [QuantumSet B] : ↑(PhiMap ↑(((rankOne ℂ) 1) 1)) = 1

theorem ContinuousLinearMap.isPositive_iff_complex' {E' : Type u_1} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [CompleteSpace E'] (T : E' →L[ℂ] E') : T.IsPositive ↔ ∀ (x : E'), 0 ≤ inner (T x) x

theorem ContinuousLinearMap.isPositive_iff_complex'' {E' : Type u_1} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [CompleteSpace E'] (T : E' →L[ℂ] E') : T.IsPositive ↔ ∀ (x : E'), 0 ≤ inner x (T x)

theorem ContinuousLinearMap.le_iff_complex_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {p : E →L[ℂ] E} {q : E →L[ℂ] E} : p ≤ q ↔ ∀ (x : E), inner x (p x) ≤ inner x (q x)

theorem isOrthogonalProjection_iff_exists {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {p : E →L[ℂ] E} : p.IsOrthogonalProjection ↔ ∃ (U : Submodule ℂ E), orthogonalProjection' U = p

theorem orthogonalProjection'_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [CompleteSpace ↥⊤] (U : Submodule ℂ E) [CompleteSpace ↥U] : orthogonalProjection' U ≤ 1

theorem isOrthogonalProjection_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {p : E →L[ℂ] E} (hp : p.IsOrthogonalProjection) : p ≤ 1

theorem QuantumGraph.Real.gns_le_one {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (hf : QuantumGraph.Real A f) (gns : k A = 0) : LinearMap.toContinuousLinearMap ↑(PhiMap f) ≤ 1

theorem QuantumGraph.Real.innerOne_map_one_le_norm_one_pow_four_of_gns {A : Type u_1} [starAlgebra A] [QuantumSet A] [Nontrivial A] [PartialOrder A] [StarOrderedRing A] (gns : k A = 0) (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) : inner 1 (f 1) ≤ ↑‖1‖ ^ 4

theorem QuantumGraph.zero_le_degree_le_norm_one_sq_of_gns {A : Type u_1} [starAlgebra A] [QuantumSet A] [Nontrivial A] [PartialOrder A] [StarOrderedRing A] (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) (gns : k A = 0) {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) (d : ℂ) (h2 : ⋯.IsRegular d) : 0 ≤ d ∧ d ≤ ↑‖1‖ ^ 2

theorem StarOrderedRing.nonneg_iff_toQuantumSetSubset {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] (r : ℝ) : (∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) ↔ ∀ ⦃a : QuantumSet.subset r A⦄, 0 ≤ a ↔ ∃ (b : QuantumSet.subset r A), a = star b * b

theorem Coalgebra.comul_comp_mul_quantumSetSubset {A : Type u_1} [starAlgebra A] [QuantumSet A] (r : ℝ) : Coalgebra.comul ∘ₗ LinearMap.mul' ℂ (QuantumSet.subset r A) = TensorProduct.map (QuantumSet.toSubset_algEquiv r).toLinearMap (QuantumSet.toSubset_algEquiv r).toLinearMap ∘ₗ (Coalgebra.comul ∘ₗ LinearMap.mul' ℂ A) ∘ₗ TensorProduct.map (QuantumSet.toSubset_algEquiv r).symm.toLinearMap (QuantumSet.toSubset_algEquiv r).symm.toLinearMap

theorem QuantumGraph.toSubset_isRegular_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ] A} (r : ℝ) (h : QuantumGraph A f) (d : ℂ) : let h' := ⋯; h.IsRegular d ↔ h'.IsRegular d

theorem QuantumGraph.zero_le_degree_le_norm_one_sq {A : Type u_1} [starAlgebra A] [QuantumSet A] [Nontrivial A] [PartialOrder A] [StarOrderedRing A] (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {f : A →ₗ[ℂ] A} (h : QuantumGraph.Real A f) (d : ℂ) (h2 : ⋯.IsRegular d) : 0 ≤ d ∧ d ≤ ↑‖1‖ ^ 2