# 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 #

def HolorIndex (ds : ) :

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

Equations
Instances For
def HolorIndex.take {ds₂ : } {ds₁ : } :
HolorIndex (ds₁ ++ ds₂)HolorIndex ds₁
Equations
• x.take = match x✝, x with | ds, is => List.take ds.length is,
Instances For
def HolorIndex.drop {ds₂ : } {ds₁ : } :
HolorIndex (ds₁ ++ ds₂)HolorIndex ds₂
Equations
• x.drop = match x✝, x with | ds, is => List.drop ds.length is,
Instances For
theorem HolorIndex.cast_type {ds₁ : } {ds₂ : } (is : ) (eq : ds₁ = ds₂) (h : List.Forall₂ (fun (x x_1 : ) => x < x_1) is ds₁) :
(cast is, h) = is
def HolorIndex.assocRight {ds₁ : } {ds₂ : } {ds₃ : } :
HolorIndex (ds₁ ++ ds₂ ++ ds₃)HolorIndex (ds₁ ++ (ds₂ ++ ds₃))
Equations
• HolorIndex.assocRight = cast
Instances For
def HolorIndex.assocLeft {ds₁ : } {ds₂ : } {ds₃ : } :
HolorIndex (ds₁ ++ (ds₂ ++ ds₃))HolorIndex (ds₁ ++ ds₂ ++ ds₃)
Equations
• HolorIndex.assocLeft = cast
Instances For
theorem HolorIndex.take_take {ds₁ : } {ds₂ : } {ds₃ : } (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) :
t.assocRight.take = t.take.take
theorem HolorIndex.drop_take {ds₁ : } {ds₂ : } {ds₃ : } (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) :
t.assocRight.drop.take = t.take.drop
theorem HolorIndex.drop_drop {ds₁ : } {ds₂ : } {ds₃ : } (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) :
t.assocRight.drop.drop = t.drop
def Holor (α : Type u) (ds : ) :

Holor (indexed collections of tensor coefficients)

Equations
Instances For
instance Holor.instInhabited {α : Type} {ds : } [] :
Equations
• Holor.instInhabited = { default := fun (x : ) => default }
instance Holor.instZero {α : Type} {ds : } [Zero α] :
Zero (Holor α ds)
Equations
• Holor.instZero = { zero := fun (x : ) => 0 }
Equations
• Holor.instAdd = { add := fun (x y : Holor α ds) (t : ) => x t + y t }
instance Holor.instNeg {α : Type} {ds : } [Neg α] :
Neg (Holor α ds)
Equations
• Holor.instNeg = { neg := fun (a : Holor α ds) (t : ) => -a t }
instance Holor.instAddSemigroup {α : Type} {ds : } [] :
Equations
instance Holor.instAddCommSemigroup {α : Type} {ds : } [] :
Equations
instance Holor.instAddMonoid {α : Type} {ds : } [] :
Equations
instance Holor.instAddCommMonoid {α : Type} {ds : } [] :
Equations
instance Holor.instAddGroup {α : Type} {ds : } [] :
Equations
instance Holor.instAddCommGroup {α : Type} {ds : } [] :
Equations
instance Holor.instSMulOfMul {α : Type} {ds : } [Mul α] :
SMul α (Holor α ds)
Equations
• Holor.instSMulOfMul = { smul := fun (a : α) (x : Holor α ds) (t : ) => a * x t }
instance Holor.instModule {α : Type} {ds : } [] :
Module α (Holor α ds)
Equations
• Holor.instModule = Pi.module () (fun (a : ) => α) α
def Holor.mul {α : Type} {ds₁ : } {ds₂ : } [Mul α] (x : Holor α ds₁) (y : Holor α ds₂) :
Holor α (ds₁ ++ ds₂)

The tensor product of two holors.

Equations
• x.mul y t = x t.take * y t.drop
Instances For
theorem Holor.cast_type {α : Type} {ds₁ : } {ds₂ : } (eq : ds₁ = ds₂) (a : Holor α ds₁) :
cast a = fun (t : HolorIndex ds₂) => a (cast t)
def Holor.assocRight {α : Type} {ds₁ : } {ds₂ : } {ds₃ : } :
Holor α (ds₁ ++ ds₂ ++ ds₃)Holor α (ds₁ ++ (ds₂ ++ ds₃))
Equations
• Holor.assocRight = cast
Instances For
def Holor.assocLeft {α : Type} {ds₁ : } {ds₂ : } {ds₃ : } :
Holor α (ds₁ ++ (ds₂ ++ ds₃))Holor α (ds₁ ++ ds₂ ++ ds₃)
Equations
• Holor.assocLeft = cast
Instances For
theorem Holor.mul_assoc0 {α : Type} {ds₁ : } {ds₂ : } {ds₃ : } [] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
(x.mul y).mul z = (x.mul (y.mul z)).assocLeft
theorem Holor.mul_assoc {α : Type} {ds₁ : } {ds₂ : } {ds₃ : } [] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
HEq ((x.mul y).mul z) (x.mul (y.mul z))
theorem Holor.mul_left_distrib {α : Type} {ds₁ : } {ds₂ : } [] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₂) :
x.mul (y + z) = x.mul y + x.mul z
theorem Holor.mul_right_distrib {α : Type} {ds₁ : } {ds₂ : } [] (x : Holor α ds₁) (y : Holor α ds₁) (z : Holor α ds₂) :
(x + y).mul z = x.mul z + y.mul z
@[simp]
theorem Holor.zero_mul {ds₁ : } {ds₂ : } {α : Type} [Ring α] (x : Holor α ds₂) :
= 0
@[simp]
theorem Holor.mul_zero {ds₁ : } {ds₂ : } {α : Type} [Ring α] (x : Holor α ds₁) :
x.mul 0 = 0
theorem Holor.mul_scalar_mul {α : Type} {ds : } [] (x : Holor α []) (y : Holor α ds) :
x.mul y = x [], y
def Holor.slice {α : Type} {d : } {ds : } (x : Holor α (d :: ds)) (i : ) (h : i < d) :
Holor α ds

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

Equations
• x.slice i h is = x i :: is,
Instances For
def Holor.unitVec {α : Type} [] [] (d : ) (j : ) :
Holor α [d]

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

Equations
Instances For
theorem Holor.holor_index_cons_decomp {d : } {ds : } (p : HolorIndex (d :: ds)Prop) (t : HolorIndex (d :: ds)) :
(∀ (i : ) (is : ) (h : t = i :: is), p i :: is, )p t
theorem Holor.slice_eq {α : Type} {d : } {ds : } (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) (h : x.slice = y.slice) :
x = y

Two holors are equal if all their slices are equal.

theorem Holor.slice_unitVec_mul {α : Type} {d : } {ds : } [Ring α] {i : } {j : } (hid : i < d) (x : Holor α ds) :
(().mul x).slice i hid = if i = j then x else 0
theorem Holor.slice_add {α : Type} {d : } {ds : } [Add α] (i : ) (hid : i < d) (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) :
x.slice i hid + y.slice i hid = (x + y).slice i hid
theorem Holor.slice_zero {α : Type} {d : } {ds : } [Zero α] (i : ) (hid : i < d) :
Holor.slice 0 i hid = 0
theorem Holor.slice_sum {α : Type} {d : } {ds : } [] {β : Type} (i : ) (hid : i < d) (s : ) (f : βHolor α (d :: ds)) :
xs, (f x).slice i hid = (xs, f x).slice i hid
@[simp]
theorem Holor.sum_unitVec_mul_slice {α : Type} {d : } {ds : } [Ring α] (x : Holor α (d :: ds)) :
i().attach, ().mul (x.slice 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 : } :
Holor α dsProp

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 α []), x.CPRankMax1
• cons: ∀ {α : Type} [inst : Mul α] {d : } {ds : } (x : Holor α [d]) (y : Holor α ds), y.CPRankMax1(x.mul y).CPRankMax1
Instances For
inductive Holor.CPRankMax {α : Type} [Mul α] [] :
{ds : } → Holor α dsProp

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 : ] {ds : },
• succ: ∀ {α : Type} [inst : Mul α] [inst_1 : ] (n : ) {ds : } (x y : Holor α ds), x.CPRankMax1Holor.CPRankMax (n + 1) (x + y)
Instances For
theorem Holor.cprankMax_nil {α : Type} [] [] (x : Holor α []) :
theorem Holor.cprankMax_1 {α : Type} {ds : } [] [] {x : Holor α ds} (h : x.CPRankMax1) :
@[irreducible]
theorem Holor.cprankMax_add {α : Type} {ds : } [] [] {m : } {n : } {x : Holor α ds} {y : Holor α ds} :
Holor.CPRankMax (m + n) (x + y)
@[irreducible]
theorem Holor.cprankMax_mul {α : Type} {d : } {ds : } [Ring α] (n : ) (x : Holor α [d]) (y : Holor α ds) :
Holor.CPRankMax n (x.mul y)
theorem Holor.cprankMax_sum {α : Type} {ds : } [Ring α] {β : Type u_1} {n : } (s : ) (f : βHolor α ds) :
(xs, Holor.CPRankMax n (f x))Holor.CPRankMax (s.card * n) (xs, f x)
theorem Holor.cprankMax_upper_bound {α : Type} [Ring α] {ds : } (x : Holor α ds) :
Holor.CPRankMax ds.prod x
noncomputable def Holor.cprank {α : Type} {ds : } [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
• x.cprank =
Instances For
theorem Holor.cprank_upper_bound {α : Type} [Ring α] {ds : } (x : Holor α ds) :
x.cprank ds.prod