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 https://www.isa-afp.org/entries/Deep_Learning.html

References

• https://en.wikipedia.org/wiki/Tensor_rank_decomposition

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.

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

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

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 (_ : HolorIndex ds₁ = HolorIndex ds₂) { val := is, property := h }) = is

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

instance Holor.instModuleHolorInstAddCommMonoidHolorToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiring {α : Type} {ds : List ℕ} [Semiring α] : Module α (Holor α 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.

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

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

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

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 := (_ : List.Forall₂ (fun x x_1 => x < x_1) [] []) } • 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.

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

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

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 := (_ : List.Forall₂ (fun x x_1 => x < x_1) (i :: is) (d :: ds)) }) → 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 => Holor.mul (Holor.unitVec d ↑i) (Holor.slice x ↑i (_ : Nat.succ ↑i ≤ d))) = 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

• 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)

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

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

• 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)

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.

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 : β), x ∈ s → Holor.CPRankMax n (f x)) → Holor.CPRankMax (Finset.card s * 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.

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