mathlib3 documentation

data.holor

Basic properties of holors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (ds : list ) :

holor_index ds is the type of valid index tuples used 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₃)) :
@[protected, instance]
def holor.inhabited {α : Type} {ds : list } [inhabited α] :
Equations
@[protected, instance]
def holor.has_zero {α : Type} {ds : list } [has_zero α] :
has_zero (holor α ds)
Equations
@[protected, instance]
def holor.has_add {α : Type} {ds : list } [has_add α] :
has_add (holor α ds)
Equations
@[protected, instance]
def holor.has_neg {α : Type} {ds : list } [has_neg α] :
has_neg (holor α ds)
Equations
@[protected, instance]
def holor.add_semigroup {α : Type} {ds : list } [add_semigroup α] :
Equations
@[protected, instance]
def holor.add_monoid {α : Type} {ds : list } [add_monoid α] :
Equations
@[protected, instance]
def holor.add_group {α : Type} {ds : list } [add_group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def holor.has_smul {α : Type} {ds : list } [has_mul α] :
has_smul α (holor α ds)
Equations
@[protected, instance]
def holor.module {α : Type} {ds : list } [semiring α] :
module α (holor α ds)
Equations
def holor.mul {α : Type} {ds₁ ds₂ : list } [s : has_mul α] (x : holor α ds₁) (y : 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 : ) (h : i < d) :
holor α ds

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

Equations
def holor.unit_vec {α : Type} [monoid α] [add_monoid α] (d j : ) :
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)) (h : x.slice = y.slice) :
x = 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)) :
s.sum (λ (x : β), (f x).slice i hid) = (s.sum (λ (x : β), f x)).slice i hid
@[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.

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