ℝ→Float32 bridge: depthwise convolution (the one new conv lemma for EfficientNet)

EfficientNet's MBConv depthwise stage is the only forward op in the enet line whose float bound isn't already a wrap of an existing closeness. Structurally it is easier than a full conv: per output (ch, hi, wi) it is

depthwiseConv2d W b x ch hi wi = b ch + Σ_{kh,kw} W ch kh kw · pad(x ch …)

— a dot over the kH·kW window with no channel sum (fan-in kH·kW, not ic·kH·kW). That is the depthwise efficiency advantage, and it carries to the bound: the Higham γ-factor rides kH·kW.

We get it for free from the existing conv scaffolding. The padded read in the depthwise forward is definitionally convPad kH kW x ch kh kw hi wi (same SAME-padding dite), so each output channel is a single-output Proofs.dense over the kH·kW-flattened window (depthwiseConv2d_eq_dense), and dense_close / denseErr_le_uniform deliver the budget exactly as they do for the regular conv (flatConvF_close). Then floatClose_depthwise is the FloatClose wrap, the depthwise peer of floatClose_flatConv.

noncomputable def Proofs.dwWindow {c h w : ℕ} (kH kW : ℕ) (x : Tensor3 c h w) (ch : Fin c) (hi : Fin h) (wi : Fin w) : Vec (kH * kW)

The per-output-coordinate depthwise window as a flat Vec over the kH·kW fan-in: channel ch's padded reads that its filter dots against. The depthwise analogue of convWindow, one channel only (no ic axis).

Equations

• Proofs.dwWindow kH kW x ch hi wi idx = Proofs.convPad kH kW x ch (finProdFinEquiv.symm idx).1 (finProdFinEquiv.symm idx).2 hi wi

noncomputable def Proofs.dwKernelMat {c kH kW : ℕ} (W : DepthwiseKernel c kH kW) (ch : Fin c) : Mat (kH * kW) 1

Channel ch's depthwise filter as a single-column Mat (kH·kW) 1.

Equations

• Proofs.dwKernelMat W ch idx x✝ = W ch (finProdFinEquiv.symm idx).1 (finProdFinEquiv.symm idx).2

@[simp]

theorem Proofs.dwWindow_k {c h w : ℕ} (kH kW : ℕ) (x : Tensor3 c h w) (ch : Fin c) (hi : Fin h) (wi : Fin w) (kh : Fin kH) (kw : Fin kW) : dwWindow kH kW x ch hi wi (finProdFinEquiv (kh, kw)) = convPad kH kW x ch kh kw hi wi

@[simp]

theorem Proofs.dwKernelMat_k {c kH kW : ℕ} (W : DepthwiseKernel c kH kW) (ch : Fin c) (kh : Fin kH) (kw : Fin kW) (j : Fin 1) : dwKernelMat W ch (finProdFinEquiv (kh, kw)) j = W ch kh kw

theorem Proofs.depthwiseConv2d_eq_dense {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (x : Tensor3 c h w) (ch : Fin c) (hi : Fin h) (wi : Fin w) : depthwiseConv2d W b x ch hi wi = dense (dwKernelMat W ch) (fun (x : Fin 1) => b ch) (dwWindow kH kW x ch hi wi) 0

Depthwise conv2d is a single-output dense at fan-in kH·kW — each output channel ch is Proofs.dense of its flattened filter against its window. The structural fact that lets the float depthwise budget reuse dense_close.

theorem Proofs.dwKernelMat_abs_le {c kH kW : ℕ} {W : DepthwiseKernel c kH kW} {w' : ℝ} (hW : ∀ (ch : Fin c) (kh : Fin kH) (kw : Fin kW), |W ch kh kw| ≤ w') (ch : Fin c) (i : Fin (kH * kW)) (j : Fin 1) : |dwKernelMat W ch i j| ≤ w'

Depthwise filter entries inherit the uniform kernel magnitude bound.

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

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

theorem Proofs.depthwiseConv2d_abs_le {c h w kH kW : ℕ} {W : DepthwiseKernel c kH kW} {b : Vec c} {x : Tensor3 c h w} {w' β a : ℝ} (ha : 0 ≤ a) (hW : ∀ (ch : Fin c) (kh : Fin kH) (kw : Fin kW), |W ch kh kw| ≤ w') (hb : ∀ (ch : Fin c), |b ch| ≤ β) (hx : ∀ (ch : Fin c) (i : Fin h) (j : Fin w), |x ch i j| ≤ a) (ch : Fin c) (hi : Fin h) (wi : Fin w) : |depthwiseConv2d W b x ch hi wi| ≤ FloatModel.layerAct (kH * kW) w' β a

Depthwise output magnitude bound = dense_abs_le at fan-in kH·kW.

noncomputable def Proofs.FloatModel.depthwiseConv2dF {c h w kH kW : ℕ} (M : FloatModel) (W : DepthwiseKernel c kH kW) (b : Vec c) (x : Tensor3 c h w) : Tensor3 c h w

The float depthwise conv — M.dense of the single-column filter against the flattened window, per output coordinate. The float peer of depthwiseConv2d.

Equations

• M.depthwiseConv2dF W b x ch hi wi = M.dense (Proofs.dwKernelMat W ch) (fun (x : Fin 1) => b ch) (Proofs.dwWindow kH kW x ch hi wi) 0

theorem Proofs.FloatModel.depthwiseConv2dF_close {c h w kH kW : ℕ} (M : FloatModel) (W : DepthwiseKernel c kH kW) (b : Vec c) (xt xa : Tensor3 c h w) {e : ℝ} (he : 0 ≤ e) (hx : ∀ (ch : Fin c) (i : Fin h) (j : Fin w), |xt ch i j - xa ch i j| ≤ e) (ch : Fin c) (hi : Fin h) (wi : Fin w) : |M.depthwiseConv2dF W b xt ch hi wi - depthwiseConv2d W b xa ch hi wi| ≤ M.denseErr (dwKernelMat W ch) (fun (x : Fin 1) => b ch) (dwWindow kH kW xa ch hi wi) e 0

Depthwise conv forward rounding budget. The rounded depthwise conv at a float input within e of the real activation is within the kH·kW-fan-in denseErr of the real depthwise conv — dense_close at the flattened window.

noncomputable def Proofs.FloatModel.depthwiseFlatF {c h w kH kW : ℕ} (M : FloatModel) (W : DepthwiseKernel c kH kW) (b : Vec c) : Vec (c * h * w) → Vec (c * h * w)

Vec-space float depthwise conv — the float peer of depthwiseFlat (flatten ∘ depthwiseConv2d ∘ unflatten), with the rounded depthwiseConv2dF.

Equations

• M.depthwiseFlatF W b v = (M.depthwiseConv2dF W b (Proofs.Tensor3.unflatten v)).flatten

theorem Proofs.FloatModel.depthwiseFlatF_close {c h w kH kW : ℕ} (M : FloatModel) (W : DepthwiseKernel c kH kW) (b : Vec c) (vt va : Vec (c * h * w)) {w' β a e : ℝ} (hw' : 0 ≤ w') (ha : 0 ≤ a) (he : 0 ≤ e) (hW : ∀ (ch : Fin c) (kh : Fin kH) (kw : Fin kW), |W ch kh kw| ≤ w') (hb : ∀ (ch : Fin c), |b ch| ≤ β) (hva : ∀ (k : Fin (c * h * w)), |va k| ≤ a) (hvte : ∀ (k : Fin (c * h * w)), |vt k - va k| ≤ e) (k : Fin (c * h * w)) : |M.depthwiseFlatF W b vt k - depthwiseFlat W b va k| ≤ layerBudget M.u (kH * kW) w' β a e

Vec-space depthwise forward budget, uniform. The rounded depthwiseFlatF at a float input within e of the real activation is within the kH·kW-fan-in layerBudget of the real depthwiseFlat, every output coordinate.

theorem Proofs.depthwiseFlat_abs_le {c h w kH kW : ℕ} {W : DepthwiseKernel c kH kW} {b : Vec c} {v : Vec (c * h * w)} {w' β a : ℝ} (ha : 0 ≤ a) (hW : ∀ (ch : Fin c) (kh : Fin kH) (kw : Fin kW), |W ch kh kw| ≤ w') (hb : ∀ (ch : Fin c), |b ch| ≤ β) (hv : ∀ (k : Fin (c * h * w)), |v k| ≤ a) (k : Fin (c * h * w)) : |depthwiseFlat W b v k| ≤ FloatModel.layerAct (kH * kW) w' β a

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

theorem Proofs.floatClose_depthwise {c h w kH kW : ℕ} (M : FloatModel) (W : DepthwiseKernel c kH kW) (b : Vec c) {w' β A : ℝ} (hw' : 0 ≤ w') (hβ : 0 ≤ β) (hA : 0 ≤ A) (hn : 0 < c * h * w) (hW : ∀ (ch : Fin c) (kh : Fin kH) (kw : Fin kW), |W ch kh kw| ≤ w') (hb : ∀ (ch : Fin c), |b ch| ≤ β) : FloatClose A (FloatModel.layerAct (kH * kW) w' β A + FloatModel.layerBudget M.u (kH * kW) w' β A 0) (depthwiseFlat W b) (M.depthwiseFlatF W b) fun (e : ℝ) => FloatModel.layerBudget M.u (kH * kW) w' β A e

Depthwise convolution is FloatClose with modulus the depthwise-fan-in layerBudget (fan-in kH·kW, no channel sum — the depthwise efficiency carries into the budget). Real output ≤ layerAct; float output ≤ that + the fresh-input rounding layerBudget(e=0). The depthwise peer of floatClose_flatConv; the MBConv depthwise stage folds through .comp like any other conv.