Layer

Difficulty: hard — 6 definitions, 2 abbreviations, 1 lemmas, 7 theorems, 0 examples.

definition abbreviation lemma theorem

legend

NoteLayer

layers

Layer (I J : InterfaceOld) : Type

Show details

fun I J => Specification (I.tensor J)

Complexity: 11 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: InterfaceOld.tensor, Specification

Used by: DataLinkLayer.network, DataLinkLayer.physical, Layer.Realizable, Layer.Univalent, Layer.eq_toFun_of_univalent, Layer.id, Layer.id_sequential, Layer.loop, Layer.parallel, Layer.parallel_rel, Layer.rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.symmetry, Layer.toFun, Layer.toFun_spec, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, NetworkArchitecture.stack, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, TransportLayer.application

NoteLayer.sequential

Layer.sequential {I J K : InterfaceOld} (f : Layer I J) (g : Layer J K) : Layer I K

Show details

fun {I J K} f g v => ∃ w, f (v.left.join w) ∧ g (w.join v.right)

Complexity: 73 (size of the value term)

Outer dependencies: InterfaceOld, Layer

Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

Lean core dependencies: And, Exists

Used by: Layer.id_sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, NetworkArchitecture.stack

NoteLayer.parallel

Layer.parallel {I1 J1 I2 J2 : InterfaceOld} (f : Layer I1 J1) (g : Layer I2 J2) :
  Layer (I1.tensor I2) (J1.tensor J2)

Show details

fun {I1 J1 I2 J2} f g v => f (v.left.left.join v.right.left) ∧ g (v.left.right.join v.right.right)

Complexity: 141 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.tensor, Layer

Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right

Lean core dependencies: And

Used by: Layer.parallel_rel, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_vanishing

NoteLayer.id

Layer.id (I : InterfaceOld) : Layer I I

Show details

fun I v => v.left = v.right

Complexity: 31 (size of the value term)

Outer dependencies: InterfaceOld, Layer

Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

Lean core dependencies: Eq

Used by: Layer.id_rel, Layer.id_sequential, Layer.sequential_id, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_vanishing, Layer.trace_yanking

NoteLayer.rel

Layer.rel {I J : InterfaceOld} (f : Layer I J) (a : I.Value) (b : J.Value) : Prop

Show details

fun {I J} f a b => f (a.join b)

Complexity: 29 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value, Layer

Inner dependencies: InterfaceOld.Value.join

Used by: Layer.id_rel, Layer.loop, Layer.parallel_rel, Layer.sequential_rel, Layer.trace_yanking

ImportantLayer.sequential_rel

Layer.sequential_rel {I J K : InterfaceOld} (f : Layer I J) (g : Layer J K) (i : I.Value)
  (k : K.Value) : (f.sequential g).rel i k ↔ ∃ w, f.rel i w ∧ g.rel w k

Show details

fun {I J K} f g i k =>
  id
    (id
      (of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Iff
              (congrArg Exists
                (funext fun w =>
                  congr
                    (congrArg And
                      (congrArg f
                        (congrFun'
                          (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join i k)) w)))
                    (congrArg g (congrArg w.join (InterfaceOld.Value.right_join i k))))))
            (∃ w, f (i.join w) ∧ g (w.join k)))
          (iff_self (∃ w, f (i.join w) ∧ g (w.join k))))))

Complexity: 1315 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, Layer, Layer.rel, Layer.sequential

Proof dependencies: InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.tensor

Lean core dependencies: And, Eq.trans, Exists, Iff, True, congr, congrArg, congrFun', funext, id, iff_self, of_eq_true

Used by: (none)

ImportantLayer.parallel_rel

Layer.parallel_rel {I1 J1 I2 J2 : InterfaceOld} (f : Layer I1 J1) (g : Layer I2 J2)
  (a : (I1.tensor I2).Value) (b : (J1.tensor J2).Value) :
  (f.parallel g).rel a b ↔ f.rel a.left b.left ∧ g.rel a.right b.right

Show details

fun {I1 J1 I2 J2} f g a b =>
  id
    (id
      (of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Iff
              (congr
                (congrArg And
                  (congrArg f
                    (congr
                      (congrArg InterfaceOld.Value.join
                        (congrArg InterfaceOld.Value.left (InterfaceOld.Value.left_join a b)))
                      (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join a b)))))
                (congrArg g
                  (congr
                    (congrArg InterfaceOld.Value.join
                      (congrArg InterfaceOld.Value.right (InterfaceOld.Value.left_join a b)))
                    (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join a b))))))
            (f (a.left.join b.left) ∧ g (a.right.join b.right)))
          (iff_self (f (a.left.join b.left) ∧ g (a.right.join b.right))))))

Complexity: 2567 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor, Layer, Layer.parallel, Layer.rel

Proof dependencies: InterfaceOld.Value.join, InterfaceOld.Value.left_join, InterfaceOld.Value.right_join

Lean core dependencies: And, Eq.trans, Iff, True, congr, congrArg, congrFun', id, iff_self, of_eq_true

Used by: (none)

ImportantLayer.id_rel

Layer.id_rel {I : InterfaceOld} (a b : I.Value) : (Layer.id I).rel a b ↔ a = b

Show details

fun {I} a b =>
  id
    (id
      (of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Iff
              (congr (congrArg Eq (InterfaceOld.Value.left_join a b))
                (InterfaceOld.Value.right_join a b)))
            (a = b))
          (iff_self (a = b)))))

Complexity: 445 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, Layer.id, Layer.rel

Proof dependencies: InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join

Lean core dependencies: Eq, Eq.trans, Iff, True, congr, congrArg, congrFun', id, iff_self, of_eq_true

Used by: (none)

ImportantLayer.sequential_assoc

Layer.sequential_assoc {I J K L : InterfaceOld} (f : Layer I J) (g : Layer J K) (h : Layer K L) :
  (f.sequential g).sequential h = f.sequential (g.sequential h)

Show details

fun {I J K L} f g h =>
  funext fun v =>
    Eq.mpr
      (id
        (congr
          (congrArg Eq
            (congrArg Exists
              (funext fun w =>
                congrFun'
                  (congrArg And
                    (congrArg Exists
                      (funext fun w_1 =>
                        congr
                          (congrArg And
                            (congrArg f
                              (congrFun'
                                (congrArg InterfaceOld.Value.join
                                  (InterfaceOld.Value.left_join v.left w))
                                w_1)))
                          (congrArg g
                            (congrArg w_1.join (InterfaceOld.Value.right_join v.left w))))))
                  (h (w.join v.right)))))
          (congrArg Exists
            (funext fun w =>
              congrArg (And (f (v.left.join w)))
                (congrArg Exists
                  (funext fun w_1 =>
                    congr
                      (congrArg And
                        (congrArg g
                          (congrFun'
                            (congrArg InterfaceOld.Value.join
                              (InterfaceOld.Value.left_join w v.right))
                            w_1)))
                      (congrArg h
                        (congrArg w_1.join (InterfaceOld.Value.right_join w v.right)))))))))
      (propext
        {
          mp := fun a =>
            Exists.casesOn a fun k h_1 =>
              And.casesOn h_1 fun left hh =>
                Exists.casesOn left fun j h_2 =>
                  And.casesOn h_2 fun hf hg => Exists.intro j ⟨hf, Exists.intro k ⟨hg, hh⟩⟩,
          mpr := fun a =>
            Exists.casesOn a fun j h_1 =>
              And.casesOn h_1 fun hf right =>
                Exists.casesOn right fun k h_2 =>
                  And.casesOn h_2 fun hg hh => Exists.intro k ⟨Exists.intro j ⟨hf, hg⟩, hh⟩ })

Complexity: 5721 (size of the value term)

Dependencies: InterfaceOld, Layer, Layer.sequential

Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.tensor

Lean core dependencies: And, Eq, Eq.mpr, Exists, congr, congrArg, congrFun', funext, id

Used by: (none)

ImportantLayer.id_sequential

Layer.id_sequential {I J : InterfaceOld} (f : Layer I J) : (Layer.id I).sequential f = f

Show details

fun {I J} f =>
  funext fun v =>
    propext
      {
        mp := fun a =>
          Exists.casesOn a fun w h =>
            And.casesOn h fun hw hf =>
              Eq.mp (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v))
                (Eq.mp
                  (congrArg (fun _a => f (_a.join v.right))
                    (Eq.symm
                      (Eq.mp
                        (congr (congrArg Eq (InterfaceOld.Value.left_join v.left w))
                          (InterfaceOld.Value.right_join v.left w))
                        hw)))
                  hf),
        mpr := fun hf =>
          Exists.intro v.left
            ⟨of_eq_true
                (Eq.trans
                  (congr (congrArg Eq (InterfaceOld.Value.left_join v.left v.left))
                    (InterfaceOld.Value.right_join v.left v.left))
                  (eq_self v.left)),
              Eq.mpr (id (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v))) hf⟩ }

Complexity: 1329 (size of the value term)

Dependencies: InterfaceOld, Layer, Layer.id, Layer.sequential

Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.tensor

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, True, congr, congrArg, eq_self, funext, id, of_eq_true

Used by: (none)

ImportantLayer.sequential_id

Layer.sequential_id {I J : InterfaceOld} (f : Layer I J) : f.sequential (Layer.id J) = f

Show details

fun {I J} f =>
  funext fun v =>
    propext
      {
        mp := fun a =>
          Exists.casesOn a fun w h =>
            And.casesOn h fun hf hw =>
              Eq.mp (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v))
                (Eq.mp
                  (congrArg (fun _a => f (v.left.join _a))
                    (Eq.mp
                      (congr (congrArg Eq (InterfaceOld.Value.left_join w v.right))
                        (InterfaceOld.Value.right_join w v.right))
                      hw))
                  hf),
        mpr := fun hf =>
          Exists.intro v.right
            ⟨Eq.mpr (id (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v))) hf,
              of_eq_true
                (Eq.trans
                  (congr (congrArg Eq (InterfaceOld.Value.left_join v.right v.right))
                    (InterfaceOld.Value.right_join v.right v.right))
                  (eq_self v.right))⟩ }

Complexity: 1307 (size of the value term)

Dependencies: InterfaceOld, Layer, Layer.id, Layer.sequential

Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.tensor

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.trans, True, congr, congrArg, eq_self, funext, id, of_eq_true

Used by: (none)

NoteLayer.Univalent

Layer.Univalent {I J : InterfaceOld} (f : Layer I J) : Prop

Show details

fun {I J} f => ∀ (i : I.Value) (j1 j2 : J.Value), f (i.join j1) → f (i.join j2) → j1 = j2

Complexity: 55 (size of the value term)

Outer dependencies: InterfaceOld, Layer

Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.join

Lean core dependencies: Eq

Used by: Layer.eq_toFun_of_univalent

NoteLayer.Realizable

Layer.Realizable {I J : InterfaceOld} (f : Layer I J) : Prop

Show details

fun {I J} f => ∀ (i : I.Value), ∃ j, f (i.join j)

Complexity: 35 (size of the value term)

Outer dependencies: InterfaceOld, Layer

Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.join

Lean core dependencies: Exists

Used by: Layer.eq_toFun_of_univalent, Layer.toFun, Layer.toFun_spec

NoteLayer.toFun

Layer.toFun {I J : InterfaceOld} (f : Layer I J) (h : f.Realizable) : I.Value → J.Value

Show details

fun {I J} f h i => ⋯.choose

Complexity: 47 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value, Layer, Layer.Realizable

Inner dependencies: InterfaceOld.Value.join

Lean core dependencies: Exists.choose

Used by: Layer.eq_toFun_of_univalent, Layer.toFun_spec

TipLayer.toFun_spec

Layer.toFun_spec {I J : InterfaceOld} (f : Layer I J) (h : f.Realizable) (i : I.Value) :
  f (i.join (f.toFun h i))

Show details

fun {I J} f h i => Exists.choose_spec (h i)

Complexity: 47 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.join, Layer, Layer.Realizable, Layer.toFun

Lean core dependencies: Exists.choose_spec

Used by: Layer.eq_toFun_of_univalent

ImportantLayer.eq_toFun_of_univalent

Layer.eq_toFun_of_univalent {I J : InterfaceOld} (f : Layer I J) (hr : f.Realizable)
  (hu : f.Univalent) : f = fun v => v.right = f.toFun hr v.left

Show details

fun {I J} f hr hu =>
  funext fun v =>
    propext
      {
        mp := fun hf =>
          hu v.left v.right (f.toFun hr v.left)
            (Eq.mp (congrArg (fun _a => f _a) (Eq.symm (InterfaceOld.Value.join_left_right v))) hf)
            (Layer.toFun_spec f hr v.left),
        mpr := fun hv =>
          have this := Layer.toFun_spec f hr v.left;
          Eq.mp (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v))
            (Eq.mp (congrArg (fun _a => f (v.left.join _a)) (Eq.symm hv)) this) }

Complexity: 672 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor, Layer, Layer.Realizable, Layer.Univalent, Layer.toFun

Proof dependencies: InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, Layer.toFun_spec

Lean core dependencies: Eq, Eq.mp, Eq.symm, congrArg, funext

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend