小编VHa*_*sop的帖子

我正在尝试制作一个"自定义"卷积层Theano,而不是使用图像卷积的线性滤波器,我正在应用支气管或气流(基本上是膨胀和腐蚀).我怎样才能以有效的方式写出这样的卷积？

给定张量X旨在包含一组向量作为输入,其与滤波器的扩张W可以写为

dil, _ = theano.scan(fn = lambda x: T.max(W + x), sequences=[X])

问题是我不知道如何将这种操作适当地应用于图像的子区域,同时考虑到任意大小的滤波器的填充,张量切片等.我还在文档中读到,使用scan实现卷积效率非常低.有关如何做到这一点的任何想法？

我在Coq中使用MathComp库进行反射时遇到了一些非常简单的证明.

假设我想证明这个引理:

From mathcomp Require Import ssreflect ssrbool ssrnat.

Lemma example m n: n.+1 < m -> n < m.
Proof.
      have predn_ltn_k k: (0 < k.-1) -> (0 < k).
          by case: k.
      rewrite -subn_gt0 subnS => submn_pred_gt0.
      by rewrite -subn_gt0; apply predn_ltn_k.
Qed.

对于这样一个简单的任务,这种方法对我来说似乎有些"非正统".有更好/更简单的方法吗？