Basic properties of holors

Holors are indexed collections of tensor coefficients. Confusingly, they are often called tensors in physics and in the neural network community.

A holor is simply a multidimensional array of values. The size of a holor is specified by a List ℕ, whose length is called the dimension of the holor.

The tensor product of x₁ : Holor α ds₁ and x₂ : Holor α ds₂ is the holor given by (x₁ ⊗ x₂) (i₁ ++ i₂) = x₁ i₁ * x₂ i₂. A holor is "of rank at most 1" if it is a tensor product of one-dimensional holors. The CP rank of a holor x is the smallest N such that x is the sum of N holors of rank at most 1.

Based on the tensor library found in

References

def HolorIndex (ds : List ℕ) : Type

HolorIndex ds is the type of valid index tuples used to identify an entry of a holor of dimensions ds.

Equations

• HolorIndex ds = { is : List ℕ // List.Forall₂ (fun (x x_1 : ℕ) => x < x_1) is ds }

def HolorIndex.take {ds₂ : List ℕ} {ds₁ : List ℕ} : HolorIndex (ds₁ ++ ds₂) → HolorIndex ds₁

Equations

• HolorIndex.take x = match x✝, x with | ds, is => { val := List.take (List.length ds) ↑is, property := ⋯ }

def HolorIndex.drop {ds₂ : List ℕ} {ds₁ : List ℕ} : HolorIndex (ds₁ ++ ds₂) → HolorIndex ds₂

Equations

• HolorIndex.drop x = match x✝, x with | ds, is => { val := List.drop (List.length ds) ↑is, property := ⋯ }

theorem HolorIndex.cast_type {ds₁ : List ℕ} {ds₂ : List ℕ} (is : List ℕ) (eq : ds₁ = ds₂) (h : List.Forall₂ (fun (x x_1 : ℕ) => x < x_1) is ds₁) : ↑(cast ⋯ { val := is, property := h }) = is

def HolorIndex.assocRight {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} : HolorIndex (ds₁ ++ ds₂ ++ ds₃) → HolorIndex (ds₁ ++ (ds₂ ++ ds₃))

Equations

• HolorIndex.assocRight = cast ⋯

def HolorIndex.assocLeft {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} : HolorIndex (ds₁ ++ (ds₂ ++ ds₃)) → HolorIndex (ds₁ ++ ds₂ ++ ds₃)

Equations

• HolorIndex.assocLeft = cast ⋯

theorem HolorIndex.take_take {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) : HolorIndex.take (HolorIndex.assocRight t) = HolorIndex.take (HolorIndex.take t)

theorem HolorIndex.drop_take {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) : HolorIndex.take (HolorIndex.drop (HolorIndex.assocRight t)) = HolorIndex.drop (HolorIndex.take t)

theorem HolorIndex.drop_drop {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) : HolorIndex.drop (HolorIndex.drop (HolorIndex.assocRight t)) = HolorIndex.drop t

def Holor (α : Type u) (ds : List ℕ) : Type u

Holor (indexed collections of tensor coefficients)

Equations

• Holor α ds = (HolorIndex ds → α)

instance Holor.instInhabitedHolor {α : Type} {ds : List ℕ} [Inhabited α] : Inhabited (Holor α ds)

Equations

• Holor.instInhabitedHolor = { default := fun (x : HolorIndex ds) => default }

instance Holor.instZeroHolor {α : Type} {ds : List ℕ} [Zero α] : Zero (Holor α ds)

Equations

• Holor.instZeroHolor = { zero := fun (x : HolorIndex ds) => 0 }

instance Holor.instAddHolor {α : Type} {ds : List ℕ} [Add α] : Add (Holor α ds)

Equations

• Holor.instAddHolor = { add := fun (x y : Holor α ds) (t : HolorIndex ds) => x t + y t }

instance Holor.instNegHolor {α : Type} {ds : List ℕ} [Neg α] : Neg (Holor α ds)

Equations

• Holor.instNegHolor = { neg := fun (a : Holor α ds) (t : HolorIndex ds) => -a t }

instance Holor.instAddSemigroupHolor {α : Type} {ds : List ℕ} [AddSemigroup α] : AddSemigroup (Holor α ds)

Equations

• Holor.instAddSemigroupHolor = Pi.addSemigroup

instance Holor.instAddCommSemigroupHolor {α : Type} {ds : List ℕ} [AddCommSemigroup α] : AddCommSemigroup (Holor α ds)

Equations

• Holor.instAddCommSemigroupHolor = Pi.addCommSemigroup

instance Holor.instAddMonoidHolor {α : Type} {ds : List ℕ} [AddMonoid α] : AddMonoid (Holor α ds)

Equations

• Holor.instAddMonoidHolor = Pi.addMonoid

instance Holor.instAddCommMonoidHolor {α : Type} {ds : List ℕ} [AddCommMonoid α] : AddCommMonoid (Holor α ds)

Equations

• Holor.instAddCommMonoidHolor = Pi.addCommMonoid

instance Holor.instAddGroupHolor {α : Type} {ds : List ℕ} [AddGroup α] : AddGroup (Holor α ds)

Equations

• Holor.instAddGroupHolor = Pi.addGroup

instance Holor.instAddCommGroupHolor {α : Type} {ds : List ℕ} [AddCommGroup α] : AddCommGroup (Holor α ds)

Equations

• Holor.instAddCommGroupHolor = Pi.addCommGroup

instance Holor.instSMulHolor {α : Type} {ds : List ℕ} [Mul α] : SMul α (Holor α ds)

Equations

• Holor.instSMulHolor = { smul := fun (a : α) (x : Holor α ds) (t : HolorIndex ds) => a * x t }

instance Holor.instModuleHolorInstAddCommMonoidHolorToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiring {α : Type} {ds : List ℕ} [Semiring α] : Module α (Holor α ds)

Equations

• Holor.instModuleHolorInstAddCommMonoidHolorToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiring = Pi.module (HolorIndex ds) (fun (a : HolorIndex ds) => α) α

def Holor.mul {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} [Mul α] (x : Holor α ds₁) (y : Holor α ds₂) : Holor α (ds₁ ++ ds₂)

The tensor product of two holors.

Equations

• Holor.mul x y t = x (HolorIndex.take t) * y (HolorIndex.drop t)

theorem Holor.cast_type {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} (eq : ds₁ = ds₂) (a : Holor α ds₁) : cast ⋯ a = fun (t : HolorIndex ds₂) => a (cast ⋯ t)

def Holor.assocRight {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} : Holor α (ds₁ ++ ds₂ ++ ds₃) → Holor α (ds₁ ++ (ds₂ ++ ds₃))

Equations

• Holor.assocRight = cast ⋯

def Holor.assocLeft {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} : Holor α (ds₁ ++ (ds₂ ++ ds₃)) → Holor α (ds₁ ++ ds₂ ++ ds₃)

Equations

• Holor.assocLeft = cast ⋯

theorem Holor.mul_assoc0 {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) : Holor.mul (Holor.mul x y) z = Holor.assocLeft (Holor.mul x (Holor.mul y z))

theorem Holor.mul_assoc {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} {ds₃ : List ℕ} [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) : HEq (Holor.mul (Holor.mul x y) z) (Holor.mul x (Holor.mul y z))

theorem Holor.mul_left_distrib {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} [Distrib α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₂) : Holor.mul x (y + z) = Holor.mul x y + Holor.mul x z

theorem Holor.mul_right_distrib {α : Type} {ds₁ : List ℕ} {ds₂ : List ℕ} [Distrib α] (x : Holor α ds₁) (y : Holor α ds₁) (z : Holor α ds₂) : Holor.mul (x + y) z = Holor.mul x z + Holor.mul y z

@[simp]

theorem Holor.zero_mul {ds₁ : List ℕ} {ds₂ : List ℕ} {α : Type} [Ring α] (x : Holor α ds₂) : Holor.mul 0 x = 0

@[simp]

theorem Holor.mul_zero {ds₁ : List ℕ} {ds₂ : List ℕ} {α : Type} [Ring α] (x : Holor α ds₁) : Holor.mul x 0 = 0

theorem Holor.mul_scalar_mul {α : Type} {ds : List ℕ} [Monoid α] (x : Holor α []) (y : Holor α ds) : Holor.mul x y = x { val := [], property := ⋯ } • y

def Holor.slice {α : Type} {d : ℕ} {ds : List ℕ} (x : Holor α (d :: ds)) (i : ℕ) (h : i < d) : Holor α ds

A slice is a subholor consisting of all entries with initial index i.

Equations

• Holor.slice x i h is = x { val := i :: ↑is, property := ⋯ }

def Holor.unitVec {α : Type} [Monoid α] [AddMonoid α] (d : ℕ) (j : ℕ) : Holor α [d]

The 1-dimensional "unit" holor with 1 in the jth position.

Equations

• Holor.unitVec d j ti = if ↑ti = [j] then 1 else 0

theorem Holor.holor_index_cons_decomp {d : ℕ} {ds : List ℕ} (p : HolorIndex (d :: ds) → Prop) (t : HolorIndex (d :: ds)) : (∀ (i : ℕ) (is : List ℕ) (h : ↑t = i :: is), p { val := i :: is, property := ⋯ }) → p t

theorem Holor.slice_eq {α : Type} {d : ℕ} {ds : List ℕ} (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) (h : Holor.slice x = Holor.slice y) : x = y

Two holors are equal if all their slices are equal.

theorem Holor.slice_unitVec_mul {α : Type} {d : ℕ} {ds : List ℕ} [Ring α] {i : ℕ} {j : ℕ} (hid : i < d) (x : Holor α ds) : Holor.slice (Holor.mul (Holor.unitVec d j) x) i hid = if i = j then x else 0

theorem Holor.slice_add {α : Type} {d : ℕ} {ds : List ℕ} [Add α] (i : ℕ) (hid : i < d) (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) : Holor.slice x i hid + Holor.slice y i hid = Holor.slice (x + y) i hid

theorem Holor.slice_zero {α : Type} {d : ℕ} {ds : List ℕ} [Zero α] (i : ℕ) (hid : i < d) : Holor.slice 0 i hid = 0

theorem Holor.slice_sum {α : Type} {d : ℕ} {ds : List ℕ} [AddCommMonoid α] {β : Type} (i : ℕ) (hid : i < d) (s : Finset β) (f : β → Holor α (d :: ds)) : (Finset.sum s fun (x : β) => Holor.slice (f x) i hid) = Holor.slice (Finset.sum s fun (x : β) => f x) i hid

@[simp]

theorem Holor.sum_unitVec_mul_slice {α : Type} {d : ℕ} {ds : List ℕ} [Ring α] (x : Holor α (d :: ds)) : (Finset.sum (Finset.attach (Finset.range d)) fun (i : { x : ℕ // x ∈ Finset.range d }) => Holor.mul (Holor.unitVec d ↑i) (Holor.slice x ↑i ⋯)) = x

The original holor can be recovered from its slices by multiplying with unit vectors and summing up.

inductive Holor.CPRankMax1 {α : Type} [Mul α] {ds : List ℕ} : Holor α ds → Prop

CPRankMax1 x means x has CP rank at most 1, that is, it is the tensor product of 1-dimensional holors.

• nil: ∀ {α : Type} [inst : Mul α] (x : Holor α []), Holor.CPRankMax1 x
• cons: ∀ {α : Type} [inst : Mul α] {d : ℕ} {ds : List ℕ} (x : Holor α [d]) (y : Holor α ds), Holor.CPRankMax1 y → Holor.CPRankMax1 (Holor.mul x y)

inductive Holor.CPRankMax {α : Type} [Mul α] [AddMonoid α] : ℕ → {ds : List ℕ} → Holor α ds → Prop

CPRankMax N x means x has CP rank at most N, that is, it can be written as the sum of N holors of rank at most 1.

• zero: ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α] {ds : List ℕ}, Holor.CPRankMax 0 0
• succ: ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α] (n : ℕ) {ds : List ℕ} (x y : Holor α ds), Holor.CPRankMax1 x → Holor.CPRankMax n y → Holor.CPRankMax (n + 1) (x + y)

theorem Holor.cprankMax_nil {α : Type} [Monoid α] [AddMonoid α] (x : Holor α []) : Holor.CPRankMax 1 x

theorem Holor.cprankMax_1 {α : Type} {ds : List ℕ} [Monoid α] [AddMonoid α] {x : Holor α ds} (h : Holor.CPRankMax1 x) : Holor.CPRankMax 1 x

theorem Holor.cprankMax_add {α : Type} {ds : List ℕ} [Monoid α] [AddMonoid α] {m : ℕ} {n : ℕ} {x : Holor α ds} {y : Holor α ds} : Holor.CPRankMax m x → Holor.CPRankMax n y → Holor.CPRankMax (m + n) (x + y)

theorem Holor.cprankMax_mul {α : Type} {d : ℕ} {ds : List ℕ} [Ring α] (n : ℕ) (x : Holor α [d]) (y : Holor α ds) : Holor.CPRankMax n y → Holor.CPRankMax n (Holor.mul x y)

theorem Holor.cprankMax_sum {α : Type} {ds : List ℕ} [Ring α] {β : Type u_1} {n : ℕ} (s : Finset β) (f : β → Holor α ds) : (∀ x ∈ s, Holor.CPRankMax n (f x)) → Holor.CPRankMax (s.card * n) (Finset.sum s fun (x : β) => f x)

theorem Holor.cprankMax_upper_bound {α : Type} [Ring α] {ds : List ℕ} (x : Holor α ds) : Holor.CPRankMax (List.prod ds) x

noncomputable def Holor.cprank {α : Type} {ds : List ℕ} [Ring α] (x : Holor α ds) : ℕ

The CP rank of a holor x: the smallest N such that x can be written as the sum of N holors of rank at most 1.

Equations

• Holor.cprank x = Nat.find ⋯

theorem Holor.cprank_upper_bound {α : Type} [Ring α] {ds : List ℕ} (x : Holor α ds) : Holor.cprank x ≤ List.prod ds