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.

Equations

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

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

Take the first elements of a HolorIndex.

Equations

• x✝.take = ⟨List.take x✝¹.length ↑x✝, ⋯⟩

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

Drop the first elements of a HolorIndex.

Equations

• x✝.drop = ⟨List.drop x✝¹.length ↑x✝, ⋯⟩

theorem HolorIndex.cast_type {ds₁ ds₂ : List ℕ} (is : List ℕ) (eq : ds₁ = ds₂) (h : List.Forall₂ (fun (x1 x2 : ℕ) => x1 < x2) is ds₁) : ↑(cast ⋯ ⟨is, h⟩) = is

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

Right associator for HolorIndex

Equations

• HolorIndex.assocRight = cast ⋯

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

Left associator for HolorIndex

Equations

• HolorIndex.assocLeft = cast ⋯

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

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

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

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

Holor (indexed collections of tensor coefficients)

Equations

• Holor α ds = (HolorIndex ds → α)

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Holor.instAddSemigroup = Pi.addSemigroup

@[implicit_reducible]

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

Equations

• Holor.instAddCommSemigroup = Pi.addCommSemigroup

@[implicit_reducible]

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

Equations

• Holor.instAddMonoid = Pi.addMonoid

@[implicit_reducible]

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

Equations

• Holor.instAddCommMonoid = Pi.addCommMonoid

@[implicit_reducible]

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

Equations

• Holor.instAddGroup = Pi.addGroup

@[implicit_reducible]

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

Equations

• Holor.instAddCommGroup = Pi.addCommGroup

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Holor.mul {α : Type} {ds₁ ds₂ : List ℕ} [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

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

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

Right associator for Holor

Equations

• Holor.assocRight = cast ⋯

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

Left associator for Holor

Equations

• Holor.assocLeft = cast ⋯

theorem Holor.mul_assoc0 {α : Type} {ds₁ ds₂ ds₃ : List ℕ} [Semigroup α] (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₃ : List ℕ} [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) : (x.mul y).mul z ≍ x.mul (y.mul z)

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

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

@[simp]

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

@[simp]

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

theorem Holor.mul_scalar_mul {α : Type} {ds : List ℕ} [Mul α] (x : Holor α []) (y : Holor α ds) : x.mul y = x ⟨[], ⋯⟩ • 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

• x.slice i h is = x ⟨i :: ↑is, ⋯⟩

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 ⟨i :: is, ⋯⟩) → p t

theorem Holor.slice_eq {α : Type} {d : ℕ} {ds : List ℕ} (x 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 : List ℕ} [Semiring α] {i j : ℕ} (hid : i < d) (x : Holor α ds) : ((unitVec d j).mul x).slice i hid = if i = j then x else 0

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

theorem Holor.slice_zero {α : Type} {d : ℕ} {ds : List ℕ} [Zero α] (i : ℕ) (hid : i < d) : 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)) : ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid

@[simp]

theorem Holor.sum_unitVec_mul_slice {α : Type} {d : ℕ} {ds : List ℕ} [Semiring α] (x : Holor α (d :: ds)) : ∑ i ∈ (Finset.range d).attach, (unitVec d ↑i).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 : 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} [Mul α] (x : Holor α []) : x.CPRankMax1
• cons {α : Type} [Mul α] {d : ℕ} {ds : List ℕ} (x : Holor α [d]) (y : Holor α ds) : y.CPRankMax1 → (x.mul y).CPRankMax1

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} [Mul α] [AddMonoid α] {ds : List ℕ} : CPRankMax 0 0
• succ {α : Type} [Mul α] [AddMonoid α] (n : ℕ) {ds : List ℕ} (x y : Holor α ds) : x.CPRankMax1 → CPRankMax n y → CPRankMax (n + 1) (x + y)

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

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

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

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

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

theorem Holor.cprankMax_upper_bound {α : Type} [Semiring α] {ds : List ℕ} (x : Holor α ds) : CPRankMax ds.prod 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

• x.cprank = Nat.find ⋯

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