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
holor_index ds is the type of valid index tuples to identify an entry of a holor of dimensions ds
Equations
- holor_index ds = {is // list.forall₂ has_lt.lt is ds}
def
holor_index.assoc_right
{ds₁ ds₂ ds₃ : list ℕ} :
holor_index (ds₁ ++ ds₂ ++ ds₃) → holor_index (ds₁ ++ (ds₂ ++ ds₃))
Equations
- holor_index.assoc_right = cast holor_index.assoc_right._proof_1
def
holor_index.assoc_left
{ds₁ ds₂ ds₃ : list ℕ} :
holor_index (ds₁ ++ (ds₂ ++ ds₃)) → holor_index (ds₁ ++ ds₂ ++ ds₃)
Equations
- holor_index.assoc_left = cast holor_index.assoc_left._proof_1
theorem
holor_index.take_take
{ds₁ ds₂ ds₃ : list ℕ}
(t : holor_index (ds₁ ++ ds₂ ++ ds₃)) :
t.assoc_right.take = t.take.take
theorem
holor_index.drop_drop
{ds₁ ds₂ ds₃ : list ℕ}
(t : holor_index (ds₁ ++ ds₂ ++ ds₃)) :
t.assoc_right.drop.drop = t.drop
@[instance]
Equations
- holor.inhabited = {default := λ (t : holor_index ds), inhabited.default α}
@[instance]
Equations
- holor.has_zero = {zero := λ (t : holor_index ds), 0}
@[instance]
Equations
- holor.has_add = {add := λ (x y : holor α ds) (t : holor_index ds), x t + y t}
@[instance]
Equations
- holor.has_neg = {neg := λ (a : holor α ds) (t : holor_index ds), -a t}
@[instance]
Equations
- holor.add_semigroup = {add := λ (a a_1 : holor α ds), id (λ (a_2 : holor_index ds), add_semigroup.add (a a_2) (a_1 a_2)), add_assoc := _}
@[instance]
def
holor.add_comm_semigroup
{α : Type}
{ds : list ℕ}
[add_comm_semigroup α] :
add_comm_semigroup (holor α ds)
Equations
- holor.add_comm_semigroup = {add := λ (a a_1 : holor α ds), id (λ (a_2 : holor_index ds), add_comm_semigroup.add (a a_2) (a_1 a_2)), add_assoc := _, add_comm := _}
@[instance]
Equations
- holor.add_monoid = {add := λ (a a_1 : holor α ds), id (λ (a_2 : holor_index ds), add_monoid.add (a a_2) (a_1 a_2)), add_assoc := _, zero := id (λ (a : holor_index ds), add_monoid.zero), zero_add := _, add_zero := _}
@[instance]
def
holor.add_comm_monoid
{α : Type}
{ds : list ℕ}
[add_comm_monoid α] :
add_comm_monoid (holor α ds)
Equations
- holor.add_comm_monoid = {add := λ (a a_1 : holor α ds), id (λ (a_2 : holor_index ds), add_comm_monoid.add (a a_2) (a_1 a_2)), add_assoc := _, zero := id (λ (a : holor_index ds), add_comm_monoid.zero), zero_add := _, add_zero := _, add_comm := _}
@[instance]
Equations
- holor.add_group = {add := λ (a a_1 : holor α ds), id (λ (a_2 : holor_index ds), add_group.add (a a_2) (a_1 a_2)), add_assoc := _, zero := id (λ (a : holor_index ds), add_group.zero), zero_add := _, add_zero := _, neg := λ (a : holor α ds), id (λ (a_1 : holor_index ds), add_group.neg (a a_1)), add_left_neg := _}
@[instance]
Equations
- holor.add_comm_group = {add := λ (a a_1 : holor α ds), id (λ (a_2 : holor_index ds), add_comm_group.add (a a_2) (a_1 a_2)), add_assoc := _, zero := id (λ (a : holor_index ds), add_comm_group.zero), zero_add := _, add_zero := _, neg := λ (a : holor α ds), id (λ (a_1 : holor_index ds), add_comm_group.neg (a a_1)), add_left_neg := _, add_comm := _}
@[instance]
Equations
- holor.has_scalar = {smul := λ (a : α) (x : holor α ds) (t : holor_index ds), a * x t}
@[instance]
Equations
- holor.semimodule = pi.semimodule (holor_index ds) (λ (a : holor_index ds), α) α
theorem
holor.cast_type
{α : Type}
{ds₁ ds₂ : list ℕ}
(eq : ds₁ = ds₂)
(a : holor α ds₁) :
cast _ a = λ (t : holor_index ds₂), a (cast _ t)
The 1-dimensional "unit" holor with 1 in the jth position.
Equations
- holor.unit_vec d j = λ (ti : holor_index [d]), ite (ti.val = [j]) 1 0
@[simp]
theorem
holor.sum_unit_vec_mul_slice
{α : Type}
{d : ℕ}
{ds : list ℕ}
[ring α]
(x : holor α (d :: ds)) :
(finset.range d).attach.sum (λ (i : {x // x ∈ finset.range d}), (holor.unit_vec d ↑i).mul (x.slice ↑i _)) = x
The original holor can be recovered from its slices by multiplying with unit vectors and summing up.
- nil : ∀ {α : Type} [_inst_1 : has_mul α] (x : holor α list.nil), x.cprank_max1
- cons : ∀ {α : Type} [_inst_1 : has_mul α] {d : ℕ} {ds : list ℕ} (x : holor α [d]) (y : holor α ds), y.cprank_max1 → (x.mul y).cprank_max1
cprank_max1 x means x has CP rank at most 1, that is,
it is the tensor product of 1-dimensional holors.
inductive
holor.cprank_max
{α : Type}
[has_mul α]
[add_monoid α]
(a : ℕ)
{ds : list ℕ} :
holor α ds → Prop
- zero : ∀ {α : Type} [_inst_1 : has_mul α] [_inst_2 : add_monoid α] {ds : list ℕ}, holor.cprank_max 0 0
- succ : ∀ {α : Type} [_inst_1 : has_mul α] [_inst_2 : add_monoid α] (n : ℕ) {ds : list ℕ} (x y : holor α ds), x.cprank_max1 → holor.cprank_max n y → holor.cprank_max (n + 1) (x + y)
cprank_max 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.cprank_max_nil
{α : Type}
[monoid α]
[add_monoid α]
(x : holor α list.nil) :
holor.cprank_max 1 x
theorem
holor.cprank_max_1
{α : Type}
{ds : list ℕ}
[monoid α]
[add_monoid α]
{x : holor α ds} :
x.cprank_max1 → holor.cprank_max 1 x
theorem
holor.cprank_max_add
{α : Type}
{ds : list ℕ}
[monoid α]
[add_monoid α]
{m n : ℕ}
{x y : holor α ds} :
holor.cprank_max m x → holor.cprank_max n y → holor.cprank_max (m + n) (x + y)
theorem
holor.cprank_max_mul
{α : Type}
{d : ℕ}
{ds : list ℕ}
[ring α]
(n : ℕ)
(x : holor α [d])
(y : holor α ds) :
holor.cprank_max n y → holor.cprank_max n (x.mul y)
theorem
holor.cprank_max_sum
{α : Type}
{ds : list ℕ}
[ring α]
{β : Type u_1}
{n : ℕ}
(s : finset β)
(f : β → holor α ds) :
(∀ (x : β), x ∈ s → holor.cprank_max n (f x)) → holor.cprank_max (s.card * n) (s.sum (λ (x : β), f x))
theorem
holor.cprank_max_upper_bound
{α : Type}
[ring α]
{ds : list ℕ}
(x : holor α ds) :
holor.cprank_max ds.prod x