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 (convPad, k4Idx, w3Idx, convWindow), the kernel drift that makes it Lipschitz in the weights, and the float conv: convF / flatConvF and the flatConvF_close budget every float conv-net bridge composes (ResNet-34's strided convs through ResNet34FloatBridge). The whole MNIST-CNN forward budget built from them is in SgdDescentCnn.

theorem Proofs.conv2d_eq_convPad {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 = b o + ∑ c : Fin ic, ∑ kh : Fin kH, ∑ kw : Fin kW, W o c kh kw * convPad kH kW x c kh kw hi wi

conv2d through convPad: bias plus the kernel-linear form.

theorem Proofs.abs_convPad_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) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hi : Fin h) (wi : Fin w) :

|convPad kH kW x c kh kw hi wi| ≤ a

Padded reads are bounded by the input bound (out-of-bounds reads are zero).

def Proofs.k4Idx {oc ic kH kW : ℕ} (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) :

Fin (oc * ic * kH * kW)

Flat index of a Kernel4 entry (the suite's row-major layout).

Equations

Proofs.k4Idx o c kh kw = finProdFinEquiv (finProdFinEquiv (finProdFinEquiv (o, c), kh), kw)

Instances For

theorem Proofs.unflatten_k4Idx {oc ic kH kW : ℕ} (v : Vec (oc * ic * kH * kW)) (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) :

Kernel4.unflatten v o c kh kw = v (k4Idx o c kh kw)

k4Idx reads back through Kernel4.unflatten.

theorem Proofs.flatten_k4Idx {oc ic kH kW : ℕ} (W : Kernel4 oc ic kH kW) (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) :

W.flatten (k4Idx o c kh kw) = W o c kh kw

Kernel4.flatten reads off at a k4Idx — the forward peer of unflatten_k4Idx, lifting a per-entry kernel bound to the flattened vector.

theorem Proofs.k4Idx_surj {oc ic kH kW : ℕ} (idx : Fin (oc * ic * kH * kW)) :

∃ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), idx = k4Idx o c kh kw

Every flat kernel index is a k4Idx — lets the abstract ∀ idx gradient accuracy be discharged per (o,cc,kh,kw) by cnn_conv2_grad_close.

theorem Proofs.sum_abs_k4 {oc ic kH kW : ℕ} (e : Vec (oc * ic * kH * kW)) :

∑ idx : Fin (oc * ic * kH * kW), |e idx| = ∑ o : Fin oc, ∑ c : Fin ic, ∑ kh : Fin kH, ∑ kw : Fin kW, |e (k4Idx o c kh kw)|

The output-channel slabs tile the kernel: summing the slab masses over the output channels recovers the total ℓ1 mass.

theorem Proofs.sum_abs_kernel_slab_le {oc ic kH kW : ℕ} (e : Vec (oc * ic * kH * kW)) (o : Fin oc) :

∑ c : Fin ic, ∑ kh : Fin kH, ∑ kw : Fin kW, |e (k4Idx o c kh kw)| ≤ ∑ idx : Fin (oc * ic * kH * kW), |e idx|

The ℓ1 mass of one output-channel slab is at most the total ℓ1 mass — the conv analogue of a dense column being part of the flat parameter vector.

def Proofs.w3Idx {ic kH kW : ℕ} (c : Fin ic) (kh : Fin kH) (kw : Fin kW) :

Fin (ic * kH * kW)

Flat index of a conv window slot (c, kh, kw) — k4Idx without the output channel (row-major, fan-in ic·kH·kW).

Equations

Proofs.w3Idx c kh kw = finProdFinEquiv (finProdFinEquiv (c, kh), kw)

Instances For

theorem Proofs.sum_w3 {ic kH kW : ℕ} (g : Fin (ic * kH * kW) → ℝ) :

∑ idx : Fin (ic * kH * kW), g idx = ∑ c : Fin ic, ∑ kh : Fin kH, ∑ kw : Fin kW, g (w3Idx c kh kw)

The triple conv-window sum collapses to one flat sum over the fan-in — the conv analogue of dot being a single-index sum (mirrors sum_abs_k4, one fewer axis).

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

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

Proofs.convKernelMat W idx o = W o (finProdFinEquiv.symm (finProdFinEquiv.symm idx).1).1 (finProdFinEquiv.symm (finProdFinEquiv.symm idx).1).2 (finProdFinEquiv.symm idx).2

Instances For

@[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 (w3Idx c kh kw) = convPad kH kW x c kh kw hi wi

@[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 (w3Idx c kh kw) o = W o c kh kw

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.

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).

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

M.convF W b x o hi wi = M.dense (Proofs.convKernelMat W) b (Proofs.convWindow kH kW x hi wi) o

Instances For

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 (Item A). 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), exactly as the planning doc calls for.

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.

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).

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.

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

M.flatConvF W b v = (M.convF W b (Proofs.Tensor3.unflatten v)).flatten

Instances For

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.

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).