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 #

https://en.wikipedia.org/wiki/Tensor_rank_decomposition

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

holor_index ds = {is // list.forall₂ has_lt.lt is ds}

def holor_index.take {ds₂ ds₁ : list ℕ} :

holor_index (ds₁ ++ ds₂) → holor_index ds₁

Equations

is.take = ⟨list.take ds.length is.val, _⟩

def holor_index.drop {ds₂ ds₁ : list ℕ} :

holor_index (ds₁ ++ ds₂) → holor_index ds₂

Equations

is.drop = ⟨list.drop ds.length is.val, _⟩

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

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_take {ds₁ ds₂ ds₃ : list ℕ} (t : holor_index (ds₁ ++ ds₂ ++ ds₃)) :

t.assoc_right.drop.take = t.take.drop

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

t.assoc_right.drop.drop = t.drop

def holor (α : Type u) (ds : list ℕ) :

Holor (indexed collections of tensor coefficients)

Equations

holor α ds = (holor_index ds → α)

Instances for holor

@[protected, instance]

def holor.inhabited {α : Type} {ds : list ℕ} [inhabited α] :

inhabited (holor α ds)

Equations

holor.inhabited = {default := λ (t : holor_index ds), inhabited.default}

@[protected, instance]

def holor.has_zero {α : Type} {ds : list ℕ} [has_zero α] :

has_zero (holor α ds)

Equations

holor.has_zero = {zero := λ (t : holor_index ds), 0}

@[protected, instance]

def holor.has_add {α : Type} {ds : list ℕ} [has_add α] :

has_add (holor α ds)

Equations

holor.has_add = {add := λ (x y : holor α ds) (t : holor_index ds), x t + y t}

@[protected, instance]

def holor.has_neg {α : Type} {ds : list ℕ} [has_neg α] :

has_neg (holor α ds)

Equations

holor.has_neg = {neg := λ (a : holor α ds) (t : holor_index ds), -a t}

@[protected, instance]

def holor.add_semigroup {α : Type} {ds : list ℕ} [add_semigroup α] :

add_semigroup (holor α ds)

Equations

holor.add_semigroup = {add := has_add.add holor.has_add, add_assoc := _}

@[protected, instance]

def holor.add_comm_semigroup {α : Type} {ds : list ℕ} [add_comm_semigroup α] :

add_comm_semigroup (holor α ds)

Equations

holor.add_comm_semigroup = {add := has_add.add holor.has_add, add_assoc := _, add_comm := _}

@[protected, instance]

def holor.add_monoid {α : Type} {ds : list ℕ} [add_monoid α] :

add_monoid (holor α ds)

Equations

holor.add_monoid = {add := has_add.add holor.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (x : holor α ds) (i : holor_index ds), n • x i, nsmul_zero' := _, nsmul_succ' := _}

@[protected, instance]

def holor.add_comm_monoid {α : Type} {ds : list ℕ} [add_comm_monoid α] :

add_comm_monoid (holor α ds)

Equations

holor.add_comm_monoid = {add := has_add.add holor.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul holor.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

@[protected, instance]

def holor.add_group {α : Type} {ds : list ℕ} [add_group α] :

add_group (holor α ds)

Equations

holor.add_group = {add := has_add.add holor.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul holor.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (ᾰ : holor α ds), id (λ (ᾰ_1 : holor_index ds), add_group.neg (ᾰ ᾰ_1)), sub := λ (ᾰ ᾰ_1 : holor α ds), id (λ (ᾰ_2 : holor_index ds), add_group.sub (ᾰ ᾰ_2) (ᾰ_1 ᾰ_2)), sub_eq_add_neg := _, zsmul := λ (n : ℤ) (x : holor α ds) (i : holor_index ds), n • x i, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}

@[protected, instance]

def holor.add_comm_group {α : Type} {ds : list ℕ} [add_comm_group α] :

add_comm_group (holor α ds)

Equations

holor.add_comm_group = {add := has_add.add holor.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul holor.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (ᾰ : holor α ds), id (λ (ᾰ_1 : holor_index ds), add_comm_group.neg (ᾰ ᾰ_1)), sub := λ (ᾰ ᾰ_1 : holor α ds), id (λ (ᾰ_2 : holor_index ds), add_comm_group.sub (ᾰ ᾰ_2) (ᾰ_1 ᾰ_2)), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul (add_group.to_sub_neg_monoid (holor α ds)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

@[protected, instance]

def holor.has_smul {α : Type} {ds : list ℕ} [has_mul α] :

has_smul α (holor α ds)

Equations

holor.has_smul = {smul := λ (a : α) (x : holor α ds) (t : holor_index ds), a * x t}

@[protected, instance]

def holor.module {α : Type} {ds : list ℕ} [semiring α] :

module α (holor α ds)

Equations

holor.module = pi.module (holor_index ds) (λ (ᾰ : holor_index ds), α) α

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

x.mul y = λ (t : holor_index (ds₁ ++ ds₂)), x t.take * y t.drop

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

holor.assoc_right = cast holor.assoc_right._proof_1

def holor.assoc_left {α : Type} {ds₁ ds₂ ds₃ : list ℕ} :

holor α (ds₁ ++ (ds₂ ++ ds₃)) → holor α (ds₁ ++ ds₂ ++ ds₃)

Equations

holor.assoc_left = cast holor.assoc_left._proof_1

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

x.slice i h = λ (is : holor_index ds), x ⟨i :: is.val, _⟩

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

holor α [d]

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

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

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 α] :

ℕ → Π {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} (h : 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

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