@[reducible, inline]

abbrev PiQ {ι : Type u_1} (A : ι → Type u_3) [Fintype ι] [(i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : Type (max u_1 u_3)

Equations

• PiQ A = PiLp 2 A

@[defaultInstance 1000]

instance instRingPiQ {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : Ring (PiQ A)

Equations

• instRingPiQ = Pi.ring

@[defaultInstance 1000]

instance instAlgebraComplexPiQ {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : Algebra ℂ (PiQ A)

Equations

• instAlgebraComplexPiQ = Pi.algebra ι A

@[defaultInstance 1000]

instance instStarRingPiQ {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : StarRing (PiQ A)

Equations

• instStarRingPiQ = Pi.instStarRingForall

@[defaultInstance 1000]

instance instStarModuleComplexPiQ {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : StarModule ℂ (PiQ A)

Equations

• ⋯ = ⋯

theorem PiLp.mul_apply {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (x : PiQ A) (y : PiQ A) (i : ι) : (x * y) i = x i * y i

def Pi.modAut {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (r : ℝ) : PiQ A ≃ₐ[ℂ] PiQ A

Equations

• Pi.modAut r = AlgEquiv.Pi fun (i : ι) => modAut r

theorem Pi.modAut_apply {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (r : ℝ) (x : PiQ A) (i : ι) : (Pi.modAut r) x i = (modAut r) (x i)

def piStarAlgebra {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : starAlgebra (PiQ A)

Equations

• piStarAlgebra = starAlgebra.mk (fun (r : ℝ) => Pi.modAut r) ⋯ ⋯

theorem piStarAlgebra.modAut {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (r : ℝ) (x : PiQ A) (i : ι) : (modAut r) x i = (modAut r) (x i)

noncomputable instance piInnerProductAlgebra {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] : InnerProductAlgebra (PiQ A)

Equations

• piInnerProductAlgebra = InnerProductAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

theorem piInnerProductAlgebra.inner_apply {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (a : PiQ A) (b : PiQ A) : inner a b = ∑ i : ι, inner (a i) (b i)

noncomputable instance Pi.quantumSet {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [hA : (i : ι) → QuantumSet (A i)] [gns : Fact (∀ (i : ι), k (A i) = 0)] : QuantumSet (PiQ A)

Equations

• Pi.quantumSet = QuantumSet.mk ⋯ 0 ⋯ ⋯ ((i : ι) × n (A i)) inferInstance (Classical.typeDecidableEq ((i : ι) × n (A i))) (Pi.orthonormalBasis fun (i : ι) => onb)