Documentation

LeanMlir.Proofs.Float.ConvFloat

The conv forward in floating point — conv as a weight-shared dense layer, and its rounding budget #

The 2D conv read as a dense layer over the zero-padded window (convWindow, convKernelMat, over the convPad / k4Idx / t3Idx index vocabulary of ConvIndex), and the float conv: convF / flatConvF and their budgets convF_close (used by SgdDescent.CnnFloat) and flatConvF_close (used by floatClose_flatConv).

source
noncomputable def Proofs.convWindow {ic h w : ℕ} (kH kW : ℕ) (x : Tensor3 ic h w) (hi : Fin h) (wi : Fin w) :
Vec (ic * kH * kW)

The per-output-coordinate conv window as a flat Vec over the fan-in: the (padded) input reads that the kernel slab dots against.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Proofs.convKernelMat {oc ic kH kW : ℕ} (W : Kernel4 oc ic kH kW) :
    Mat (ic * kH * kW) oc

    The kernel as a Mat (ic·kH·kW) oc — column o is the flattened slab.

    Equations
    Instances For
      source
      @[simp]
      theorem Proofs.convWindow_w3 {ic h w : ℕ} (kH kW : ℕ) (x : Tensor3 ic h w) (hi : Fin h) (wi : Fin w) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) :
      convWindow kH kW x hi wi (t3Idx c kh kw) = convPad kH kW x c kh kw hi wi
      source
      @[simp]
      theorem Proofs.convKernelMat_w3 {oc ic kH kW : ℕ} (W : Kernel4 oc ic kH kW) (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) :
      convKernelMat W (t3Idx c kh kw) o = W o c kh kw
      source
      theorem Proofs.conv2d_eq_dense {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) :
      conv2d W b x o hi wi = dense (convKernelMat W) b (convWindow kH kW x hi wi) o

      conv2d is a dense layer at the conv fan-in — conv = dense-with-sharing made exact: each output coordinate is Proofs.dense of the kernel slab against the flattened window. The structural fact that lets the float conv budget reuse dense_close.

      source
      theorem Proofs.convPad_close {ic h w kH kW : ℕ} (xt xa : Tensor3 ic h w) {e : ℝ} (he : 0 ≤ e) (hx : ∀ (c : Fin ic) (i : Fin h) (j : Fin w), |xt c i j - xa c i j| ≤ e) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hi : Fin h) (wi : Fin w) :
      |convPad kH kW xt c kh kw hi wi - convPad kH kW xa c kh kw hi wi| ≤ e

      Padded reads of inputs within e stay within e (the read is either a coordinate, diff ≤ e, or 0, diff 0).

      source
      noncomputable def Proofs.FloatModel.convF {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) :
      Tensor3 oc h w

      The float conv layer — M.dense of the kernel slab against the flattened window, per output coordinate. The float peer of conv2d (every product/accumulate/bias-add rounded), in the dense form.

      Equations
      Instances For
        source
        theorem Proofs.FloatModel.convF_close {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) (xt xa : Tensor3 ic h w) {e : ℝ} (he : 0 ≤ e) (hx : ∀ (c : Fin ic) (i : Fin h) (j : Fin w), |xt c i j - xa c i j| ≤ e) (o : Fin oc) (hi : Fin h) (wi : Fin w) :
        |M.convF W b xt o hi wi - conv2d W b xa o hi wi| ≤ M.denseErr (convKernelMat W) b (convWindow kH kW xa hi wi) e o

        Conv forward rounding budget. The rounded conv at a float input within e of the real activation is within the conv-fan-in denseErr of the real conv — dense_close at the flattened window. The compounded Higham factor rides the fan-in ic·kH·kW (the dense column length here).

        source
        theorem Proofs.convKernelMat_abs_le {oc ic kH kW : ℕ} {W : Kernel4 oc ic kH kW} {w' : ℝ} (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), |W o c kh kw| ≤ w') (i : Fin (ic * kH * kW)) (j : Fin oc) :
        |convKernelMat W i j| ≤ w'

        Kernel-slab entries inherit the uniform kernel magnitude bound.

        source
        theorem Proofs.convWindow_abs_le {ic h w kH kW : ℕ} {x : Tensor3 ic h w} {a : ℝ} (ha : 0 ≤ a) (hx : ∀ (c : Fin ic) (i : Fin h) (j : Fin w), |x c i j| ≤ a) (hi : Fin h) (wi : Fin w) (idx : Fin (ic * kH * kW)) :
        |convWindow kH kW x hi wi idx| ≤ a

        Window reads inherit the uniform input magnitude bound (padding reads 0).

        source
        theorem Proofs.conv2d_abs_le {ic oc h w kH kW : ℕ} {W : Kernel4 oc ic kH kW} {b : Vec oc} {x : Tensor3 ic h w} {w' β a : ℝ} (ha : 0 ≤ a) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), |W o c kh kw| ≤ w') (hb : ∀ (o : Fin oc), |b o| ≤ β) (hx : ∀ (c : Fin ic) (i : Fin h) (j : Fin w), |x c i j| ≤ a) (o : Fin oc) (hi : Fin h) (wi : Fin w) :
        |conv2d W b x o hi wi| ≤ FloatModel.layerAct (ic * kH * kW) w' β a

        Conv output magnitude bound = dense_abs_le at the fan-in: conv is a dense layer, so |conv2dⱼ| ≤ layerAct (ic·kH·kW) w β a.

        source
        noncomputable def Proofs.FloatModel.flatConvF {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) :
        Vec (ic * h * w) → Vec (oc * h * w)

        Vec-space float conv — the float peer of flatConv (flatten ∘ conv2d ∘ unflatten), with the rounded convF inside.

        Equations
        Instances For
          source
          theorem Proofs.FloatModel.flatConvF_close {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) (vt va : Vec (ic * h * w)) {w' β a e : ℝ} (hw' : 0 ≤ w') (ha : 0 ≤ a) (he : 0 ≤ e) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), |W o c kh kw| ≤ w') (hb : ∀ (o : Fin oc), |b o| ≤ β) (hva : ∀ (k : Fin (ic * h * w)), |va k| ≤ a) (hvte : ∀ (k : Fin (ic * h * w)), |vt k - va k| ≤ e) (k : Fin (oc * h * w)) :
          |M.flatConvF W b vt k - flatConv W b va k| ≤ layerBudget M.u (ic * kH * kW) w' β a e

          Vec-space conv forward budget, uniform. The rounded flatConvF at a float input within e of the real activation is within the conv-fan-in layerBudget of the real flatConv — every output coordinate, one closed form. The conv layer threads exactly like a dense layer at fan-in ic·kH·kW.

          source
          theorem Proofs.flatConv_abs_le {ic oc h w kH kW : ℕ} {W : Kernel4 oc ic kH kW} {b : Vec oc} {v : Vec (ic * h * w)} {w' β a : ℝ} (ha : 0 ≤ a) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), |W o c kh kw| ≤ w') (hb : ∀ (o : Fin oc), |b o| ≤ β) (hv : ∀ (k : Fin (ic * h * w)), |v k| ≤ a) (k : Fin (oc * h * w)) :
          |flatConv W b v k| ≤ FloatModel.layerAct (ic * kH * kW) w' β a

          Vec-space conv magnitude bound (the activation-norm pass-through).