mathlib documentation

data.holor

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 holor_index  :
list → Type

holor_index ds is the type of valid index tuples to identify an entry of a holor of dimensions ds

Equations
def holor_index.take {ds₂ ds₁ : list } :
holor_index (ds₁ ++ ds₂)holor_index ds₁

Equations
def holor_index.drop {ds₂ ds₁ : list } :
holor_index (ds₁ ++ ds₂)holor_index ds₂

Equations
theorem holor_index.cast_type {ds₁ ds₂ : list } (is : list ) (eq : ds₁ = ds₂) (h : list.forall₂ has_lt.lt is ds₁) :
(cast _ is, h⟩).val = is

def holor_index.assoc_right {ds₁ ds₂ ds₃ : list } :
holor_index (ds₁ ++ ds₂ ++ ds₃)holor_index (ds₁ ++ (ds₂ ++ ds₃))

Equations
def holor_index.assoc_left {ds₁ ds₂ ds₃ : list } :
holor_index (ds₁ ++ (ds₂ ++ ds₃))holor_index (ds₁ ++ ds₂ ++ ds₃)

Equations
theorem holor_index.take_take {ds₁ ds₂ ds₃ : list } (t : holor_index (ds₁ ++ ds₂ ++ ds₃)) :

theorem holor_index.drop_take {ds₁ ds₂ ds₃ : list } (t : holor_index (ds₁ ++ ds₂ ++ ds₃)) :

theorem holor_index.drop_drop {ds₁ ds₂ ds₃ : list } (t : holor_index (ds₁ ++ ds₂ ++ ds₃)) :

def holor  :
Type ulist Type u

Holor (indexed collections of tensor coefficients)

Equations
@[instance]
def holor.inhabited {α : Type} {ds : list } [inhabited α] :

Equations
@[instance]
def holor.has_zero {α : Type} {ds : list } [has_zero α] :
has_zero (holor α ds)

Equations
@[instance]
def holor.has_add {α : Type} {ds : list } [has_add α] :
has_add (holor α ds)

Equations
@[instance]
def holor.has_neg {α : Type} {ds : list } [has_neg α] :
has_neg (holor α ds)

Equations
@[instance]
def holor.add_semigroup {α : Type} {ds : list } [add_semigroup α] :

Equations
@[instance]

Equations
@[instance]
def holor.add_monoid {α : Type} {ds : list } [add_monoid α] :

Equations
@[instance]
def holor.add_comm_monoid {α : Type} {ds : list } [add_comm_monoid α] :

Equations
@[instance]
def holor.add_group {α : Type} {ds : list } [add_group α] :

Equations
@[instance]
def holor.add_comm_group {α : Type} {ds : list } [add_comm_group α] :

Equations
@[instance]
def holor.has_scalar {α : Type} {ds : list } [has_mul α] :
has_scalar α (holor α ds)

Equations
@[instance]
def holor.semimodule {α : Type} {ds : list } [semiring α] :
semimodule α (holor α ds)

Equations
def holor.mul {α : Type} {ds₁ ds₂ : list } [s : has_mul α] :
holor α ds₁holor α ds₂holor α (ds₁ ++ ds₂)

The tensor product of two holors.

Equations
theorem holor.cast_type {α : Type} {ds₁ ds₂ : list } (eq : ds₁ = ds₂) (a : holor α ds₁) :
cast _ a = λ (t : holor_index ds₂), a (cast _ t)

def holor.assoc_right {α : Type} {ds₁ ds₂ ds₃ : list } :
holor α (ds₁ ++ ds₂ ++ ds₃)holor α (ds₁ ++ (ds₂ ++ ds₃))

Equations
def holor.assoc_left {α : Type} {ds₁ ds₂ ds₃ : list } :
holor α (ds₁ ++ (ds₂ ++ ds₃))holor α (ds₁ ++ ds₂ ++ ds₃)

Equations
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)).assoc_left

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} [ring α] (x : holor α ds₂) :
0.mul x = 0

@[simp]
theorem holor.mul_zero {ds₁ ds₂ : list } {α : Type} [ring α] (x : holor α ds₁) :
x.mul 0 = 0

theorem holor.mul_scalar_mul {α : Type} {ds : list } [monoid α] (x : holor α list.nil) (y : holor α ds) :
x.mul y = x list.nil , _⟩ y

def holor.slice {α : Type} {d : } {ds : list } (x : holor α (d :: ds)) (i : ) :
i < dholor α ds

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

Equations
def holor.unit_vec {α : Type} [monoid α] [add_monoid α] (d : ) :
holor α [d]

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

Equations
theorem holor.holor_index_cons_decomp {d : } {ds : list } (p : holor_index (d :: ds) → Prop) (t : holor_index (d :: ds)) :
(∀ (i : ) (is : list ) (h : t.val = i :: is), p i :: is, _⟩)p t

theorem holor.slice_eq {α : Type} {d : } {ds : list } (x y : holor α (d :: ds)) :
x.slice = y.slicex = y

Two holors are equal if all their slices are equal.

theorem holor.slice_unit_vec_mul {α : Type} {d : } {ds : list } [ring α] {i j : } (hid : i < d) (x : holor α ds) :
((holor.unit_vec d j).mul x).slice i hid = ite (i = j) x 0

theorem holor.slice_add {α : Type} {d : } {ds : list } [has_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 } [has_zero α] (i : ) (hid : i < d) :
0.slice i hid = 0

theorem holor.slice_sum {α : Type} {d : } {ds : list } [add_comm_monoid α] {β : Type} (i : ) (hid : i < d) (s : finset β) (f : β → holor α (d :: ds)) :
∑ (x : β) in s, (f x).slice i hid = (∑ (x : β) in s, f x).slice i hid

@[simp]
theorem holor.sum_unit_vec_mul_slice {α : Type} {d : } {ds : list } [ring α] (x : holor α (d :: ds)) :
∑ (i : {x // x finset.range d}) in (finset.range d).attach, (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.

inductive holor.cprank_max1 {α : Type} [has_mul α] {ds : list } :
holor α ds → Prop

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

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

theorem holor.cprank_max_1 {α : Type} {ds : list } [monoid α] [add_monoid α] {x : holor α ds} :

theorem holor.cprank_max_add {α : Type} {ds : list } [monoid α] [add_monoid α] {m n : } {x y : holor α ds} :

theorem holor.cprank_max_mul {α : Type} {d : } {ds : list } [ring α] (n : ) (x : holor α [d]) (y : holor α ds) :

theorem holor.cprank_max_sum {α : Type} {ds : list } [ring α] {β : Type u_1} {n : } (s : finset β) (f : β → holor α ds) :
(∀ (x : β), x sholor.cprank_max n (f x))holor.cprank_max ((s.card) * n) (∑ (x : β) in s, f x)

theorem holor.cprank_max_upper_bound {α : Type} [ring α] {ds : list } (x : holor α ds) :

def holor.cprank {α : Type} {ds : list } [ring α] :
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
theorem holor.cprank_upper_bound {α : Type} [ring α] {ds : list } (x : holor α ds) :