Documentation

Mathlib.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 HolorIndex (ds : List ) :

HolorIndex ds is the type of valid index tuples used to identify an entry of a holor of dimensions ds.

Equations
Instances For
    def HolorIndex.take {ds₂ : List } {ds₁ : List } :
    HolorIndex (ds₁ ++ ds₂)HolorIndex ds₁
    Equations
    Instances For
      def HolorIndex.drop {ds₂ : List } {ds₁ : List } :
      HolorIndex (ds₁ ++ ds₂)HolorIndex ds₂
      Equations
      Instances For
        theorem HolorIndex.cast_type {ds₁ : List } {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₁ : List } {ds₂ : List } {ds₃ : List } :
        HolorIndex (ds₁ ++ ds₂ ++ ds₃)HolorIndex (ds₁ ++ (ds₂ ++ ds₃))
        Equations
        • HolorIndex.assocRight = cast
        Instances For
          def HolorIndex.assocLeft {ds₁ : List } {ds₂ : List } {ds₃ : List } :
          HolorIndex (ds₁ ++ (ds₂ ++ ds₃))HolorIndex (ds₁ ++ ds₂ ++ ds₃)
          Equations
          • HolorIndex.assocLeft = cast
          Instances For
            theorem HolorIndex.take_take {ds₁ : List } {ds₂ : List } {ds₃ : List } (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) :
            t.assocRight.take = t.take.take
            theorem HolorIndex.drop_take {ds₁ : List } {ds₂ : List } {ds₃ : List } (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) :
            t.assocRight.drop.take = t.take.drop
            theorem HolorIndex.drop_drop {ds₁ : List } {ds₂ : List } {ds₃ : List } (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) :
            t.assocRight.drop.drop = t.drop
            def Holor (α : Type u) (ds : List ) :

            Holor (indexed collections of tensor coefficients)

            Equations
            Instances For
              instance Holor.instInhabited {α : Type} {ds : List } [Inhabited α] :
              Equations
              • Holor.instInhabited = { default := fun (x : HolorIndex ds) => default }
              instance Holor.instZero {α : Type} {ds : List } [Zero α] :
              Zero (Holor α ds)
              Equations
              • Holor.instZero = { zero := fun (x : HolorIndex ds) => 0 }
              instance Holor.instAdd {α : Type} {ds : List } [Add α] :
              Add (Holor α ds)
              Equations
              instance Holor.instNeg {α : Type} {ds : List } [Neg α] :
              Neg (Holor α ds)
              Equations
              instance Holor.instAddSemigroup {α : Type} {ds : List } [AddSemigroup α] :
              Equations
              • Holor.instAddSemigroup = Pi.addSemigroup
              Equations
              • Holor.instAddCommSemigroup = Pi.addCommSemigroup
              instance Holor.instAddMonoid {α : Type} {ds : List } [AddMonoid α] :
              Equations
              • Holor.instAddMonoid = Pi.addMonoid
              Equations
              • Holor.instAddCommMonoid = Pi.addCommMonoid
              instance Holor.instAddGroup {α : Type} {ds : List } [AddGroup α] :
              AddGroup (Holor α ds)
              Equations
              • Holor.instAddGroup = Pi.addGroup
              instance Holor.instAddCommGroup {α : Type} {ds : List } [AddCommGroup α] :
              Equations
              • Holor.instAddCommGroup = Pi.addCommGroup
              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 }
              instance Holor.instModule {α : Type} {ds : List } [Semiring α] :
              Module α (Holor α ds)
              Equations
              def Holor.mul {α : Type} {ds₁ : List } {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
              Instances For
                theorem Holor.cast_type {α : Type} {ds₁ : List } {ds₂ : List } (eq : ds₁ = ds₂) (a : Holor α ds₁) :
                cast a = fun (t : HolorIndex ds₂) => a (cast t)
                def Holor.assocRight {α : Type} {ds₁ : List } {ds₂ : List } {ds₃ : List } :
                Holor α (ds₁ ++ ds₂ ++ ds₃)Holor α (ds₁ ++ (ds₂ ++ ds₃))
                Equations
                • Holor.assocRight = cast
                Instances For
                  def Holor.assocLeft {α : Type} {ds₁ : List } {ds₂ : List } {ds₃ : List } :
                  Holor α (ds₁ ++ (ds₂ ++ ds₃))Holor α (ds₁ ++ ds₂ ++ ds₃)
                  Equations
                  • Holor.assocLeft = cast
                  Instances For
                    theorem Holor.mul_assoc0 {α : Type} {ds₁ : List } {ds₂ : List } {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₁ : List } {ds₂ : List } {ds₃ : List } [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
                    HEq ((x.mul y).mul z) (x.mul (y.mul z))
                    theorem Holor.mul_left_distrib {α : Type} {ds₁ : List } {ds₂ : List } [Distrib α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₂) :
                    x.mul (y + z) = x.mul y + x.mul z
                    theorem Holor.mul_right_distrib {α : Type} {ds₁ : List } {ds₂ : List } [Distrib α] (x : Holor α ds₁) (y : Holor α ds₁) (z : Holor α ds₂) :
                    (x + y).mul z = x.mul z + y.mul z
                    @[simp]
                    theorem Holor.zero_mul {ds₁ : List } {ds₂ : List } {α : Type} [Ring α] (x : Holor α ds₂) :
                    Holor.mul 0 x = 0
                    @[simp]
                    theorem Holor.mul_zero {ds₁ : List } {ds₂ : List } {α : Type} [Ring α] (x : Holor α ds₁) :
                    x.mul 0 = 0
                    theorem Holor.mul_scalar_mul {α : Type} {ds : List } [Monoid α] (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,
                    Instances For
                      def Holor.unitVec {α : Type} [Monoid α] [AddMonoid α] (d : ) (j : ) :
                      Holor α [d]

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

                      Equations
                      Instances For
                        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 : Holor α (d :: ds)) (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 } [Ring α] {i : } {j : } (hid : i < d) (x : Holor α ds) :
                        ((Holor.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 : Holor α (d :: ds)) (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) :
                        Holor.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)) :
                        xs, (f x).slice i hid = (∑ xs, f x).slice i hid
                        @[simp]
                        theorem Holor.sum_unitVec_mul_slice {α : Type} {d : } {ds : List } [Ring α] (x : Holor α (d :: ds)) :
                        i(Finset.range d).attach, (Holor.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 α dsProp

                        CPRankMax1 x means x has CP rank at most 1, that is, it is the tensor product of 1-dimensional holors.

                        • nil: ∀ {α : Type} [inst : Mul α] (x : Holor α []), x.CPRankMax1
                        • cons: ∀ {α : Type} [inst : Mul α] {d : } {ds : List } (x : Holor α [d]) (y : Holor α ds), y.CPRankMax1(x.mul y).CPRankMax1
                        Instances For
                          inductive Holor.CPRankMax {α : Type} [Mul α] [AddMonoid α] :
                          {ds : List } → Holor α dsProp

                          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.

                          Instances For
                            theorem Holor.cprankMax_nil {α : Type} [Monoid α] [AddMonoid α] (x : Holor α []) :
                            theorem Holor.cprankMax_1 {α : Type} {ds : List } [Monoid α] [AddMonoid α] {x : Holor α ds} (h : x.CPRankMax1) :
                            theorem Holor.cprankMax_add {α : Type} {ds : List } [Monoid α] [AddMonoid α] {m : } {n : } {x : Holor α ds} {y : Holor α ds} :
                            Holor.CPRankMax m xHolor.CPRankMax n yHolor.CPRankMax (m + n) (x + y)
                            theorem Holor.cprankMax_mul {α : Type} {d : } {ds : List } [Ring α] (n : ) (x : Holor α [d]) (y : Holor α ds) :
                            Holor.CPRankMax n yHolor.CPRankMax n (x.mul y)
                            theorem Holor.cprankMax_sum {α : Type} {ds : List } [Ring α] {β : Type u_1} {n : } (s : Finset β) (f : βHolor α ds) :
                            (∀ xs, Holor.CPRankMax n (f x))Holor.CPRankMax (s.card * n) (∑ xs, f x)
                            theorem Holor.cprankMax_upper_bound {α : Type} [Ring α] {ds : List } (x : Holor α ds) :
                            Holor.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
                            Instances For
                              theorem Holor.cprank_upper_bound {α : Type} [Ring α] {ds : List } (x : Holor α ds) :
                              x.cprank ds.prod