LeanPool.Monlib4.QuantumGraph.Degree #

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

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)

source

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

source

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

Real (QuantumSet.subset r A) (f.toSubsetQuantumSet r r) ↔ Real A f

source

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 : Real A f) :

0 ≤ inner ℂ 1 (f 1)

source

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

inner ℂ 1 (f 1) = 0 ↔ f = 0

source

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

inner ℂ 1 (f 1) = 0 ↔ f = 0

source

theorem QuantumGraph.real_iff_complement'_real {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ ] A} :

Real A f ↔ Real A (Qam.complement' f)

source

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 : Real A f) [kms : Fact (k A = -(1 / 2))] :

inner ℂ 1 (f 1) = ↑‖1‖ ^ 4 ↔ f = ↑(((rankOne ℂ) 1) 1)

source

theorem QuantumGraph.Real.innerOne_map_one_eq_norm_pow_four_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ ] A} (h : Real A f) :

inner ℂ 1 (f 1) = ↑‖1‖ ^ 4 ↔ f = ↑(((rankOne ℂ) 1) 1)

source

noncomputable def QuantumGraph.outDegree {A : Type u_1} [starAlgebra A] [QuantumSet A] :

(A →ₗ[ℂ ] A) →ₗ[ℂ ] A →ₗ[ℂ ] A

Out-degree operator of a quantum graph.

Equations

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

Instances For

source

@[simp]

theorem QuantumGraph.outDegree_apply {A : Type u_1} [starAlgebra A] [QuantumSet A] (f : A →ₗ[ℂ ] A) :

outDegree f = LinearMap.mul' ℂ A ∘ₗ LinearMap.rTensor A f ∘ₗ LinearMap.rTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.lid ℂ A).symm

source

theorem QuantumGraph.outDegree_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ ] A} :

outDegree f = lmul (f 1)

source

noncomputable def QuantumGraph.inDegree {A : Type u_1} [starAlgebra A] [QuantumSet A] :

(A →ₗ[ℂ ] A) →ₗ⋆[ℂ ] A →ₗ[ℂ ] A

In-degree operator of a quantum graph.

Equations

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

Instances For

source

@[simp]

theorem QuantumGraph.inDegree_apply {A : Type u_1} [starAlgebra A] [QuantumSet A] (f : A →ₗ[ℂ ] A) :

inDegree f = LinearMap.mul' ℂ A ∘ₗ LinearMap.lTensor A (LinearMap.adjoint f) ∘ₗ LinearMap.lTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.rid ℂ A).symm

source

theorem QuantumGraph.inDegree_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ ] A} :

inDegree f = rmul ((LinearMap.adjoint f) 1)

source

theorem QuantumGraph.outDegree_real_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {x : A →ₗ[ℂ ] A} :

(outDegree x).real = inDegree ((symmMap ℂ A A) x)

source

theorem QuantumGraph.inDegree_real_eq {A : Type u_1} [starAlgebra A] [QuantumSet A] {x : A →ₗ[ℂ ] A} :

(inDegree x).real = outDegree ((symmMap ℂ A A).symm x)

source

theorem QuantumGraph.outDegree_eq' {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ ] A} :

outDegree f = ↑(TensorProduct.lid ℂ A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ ↑(PhiMap f) ∘ₗ LinearMap.rTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.lid ℂ A).symm

source

theorem QuantumGraph.inDegree_eq' {A : Type u_1} [starAlgebra A] [QuantumSet A] (gns : k A = 0) {f : A →ₗ[ℂ ] A} :

inDegree f = ↑(TensorProduct.rid ℂ A) ∘ₗ LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ ↑(PhiMap f.real) ∘ₗ LinearMap.lTensor A (Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.rid ℂ A).symm

source

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

outDegree (f₁ •ₛ f₂) = (f₁ ∘ₗ (symmMap ℂ A A) f₂) •ₛ 1

source

theorem QuantumGraph.inDegree_apply_schurMul {A : Type u_1} [starAlgebra A] [QuantumSet A] (gns : k A = 0) (f₁ f₂ : A →ₗ[ℂ ] A) :

inDegree (f₁ •ₛ f₂) = 1 •ₛ LinearMap.adjoint f₂ ∘ₗ f₁.real

source

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

Prop

A quantum graph is regular of degree d when both f and its adjoint send 1 to d • 1.

Equations

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

Instances For

source

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

d = ↑d.re

source

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

source

theorem ContinuousLinearMap.isPositive_iff_complex' {E' : Type u_1} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] (T : E' →L[ℂ ] E') :

T.IsPositive ↔ ∀ (x : E'), 0 ≤ inner ℂ (T x) x

source

theorem ContinuousLinearMap.isPositive_iff_complex'' {E' : Type u_1} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] (T : E' →L[ℂ ] E') :

T.IsPositive ↔ ∀ (x : E'), 0 ≤ inner ℂ x (T x)

source

theorem ContinuousLinearMap.le_iff_complex_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p q : E →L[ℂ ] E} :

p ≤ q ↔ ∀ (x : E), inner ℂ x (p x) ≤ inner ℂ x (q x)

source

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

source

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

orthogonalProjection' U ≤ 1

source

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

p ≤ 1

source

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

LinearMap.toContinuousLinearMap ↑(PhiMap f) ≤ 1

source

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

inner ℂ 1 (f 1) ≤ ↑‖1‖ ^ 4

source

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 : Real A f) (d : ℂ) (h2 : ⋯.IsRegular d) :

0 ≤ d ∧ d ≤ ↑‖1‖ ^ 2

source

theorem StarOrderedRing.nonneg_iff_toQuantumSetSubset {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder 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

source

theorem Coalgebra.comul_comp_mul_quantumSetSubset {A : Type u_1} [starAlgebra A] [QuantumSet A] (r : ℝ) :

source

theorem QuantumGraph.toSubset_isRegular_iff {A : Type u_1} [starAlgebra A] [QuantumSet A] {f : A →ₗ[ℂ ] A} (r : ℝ) (h : QuantumGraph A f) (d : ℂ) :

have h' := ⋯; h.IsRegular d ↔ h'.IsRegular d

source

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 : Real A f) (d : ℂ) (h2 : ⋯.IsRegular d) :

0 ≤ d ∧ d ≤ ↑‖1‖ ^ 2