Chapter 4: CIFAR-10 2D CNN (no BatchNorm) — whole-network VJP

The Chapter-4 demo model cifarCnn (the no-BN spec of MainCifarCnnTrain):

conv 3→32 (relu) → conv 32→32 (relu) → maxPool 2×2 → conv 32→64 (relu) → conv 64→64 (relu) → maxPool 2×2 → flatten → dense 4096→512 (relu) → dense 512→512 (relu) → dense 512→10

i.e. two conv→conv→maxPool stages (channels 3→32→32, then 32→64→64) and a three-layer dense head, on 32×32 RGB input with two 2×2 pools (32→16→8).

This is the Chapter-3 mnistCnnNoBn machinery scaled up: the same convRelu/denseRelu/maxPoolFlat building blocks, chained through vjp_comp_at, just longer and with two maxpool steps. Spatial bookkeeping uses the final pooled size (h, w) as the unit: the second conv stage runs at (2h, 2w), the first at (2·(2h), 2·(2w)) — exactly the Chapter-3 (2h, 2w) convention nested one level deeper (so the two pools read maxPoolFlat _ (2h) (2w) and maxPoolFlat _ h w).

• cifarCnn_has_vjp_at — the structural whole-network VJP: the composed backward equals the pdiv-Jacobian VJP of the full forward pass, conditional on smoothness at the six ReLU kinks and the two MaxPools. The Chapter-4 sibling of mnistCnnNoBn_has_vjp_at.

• Tiny.cifarTinyCnn_has_vjp_correct — a concrete instance where every smoothness hypothesis is discharged (positivity + positional injectivity through both pools), so the statement is unconditional and closes under the three-axiom kernel. The non-vacuity witness for the conditional capstone.

noncomputable def Proofs.cifarCnnForward {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) : Vec (ic * (2 * (2 * h)) * (2 * (2 * w))) → Vec nClasses

The Chapter-4 cifarCnn forward, in flattened Vec space. The conv stack runs at spatial (2·(2h), 2·(2w)); the first maxPool halves it to (2h, 2w) (where the second conv stage runs), the second to (h, w); then three dense layers (two with ReLU). With the real CIFAR shapes ic=3, c1=32, c2=64, h=w=8, d1=512, nClasses=10, kH=kW=3 the input width is 3·32·32 = 3072 and the flattened pool output is 64·8·8 = 4096.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.cifarCnn_has_vjp_at {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) (h1 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₁ b₁ x k ≠ 0) (h2 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₂ b₂ ((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x) k ≠ 0) (h_mp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), flatConv W₃ b₃ (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x)) k ≠ 0) (h4 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), flatConv W₄ b₄ ((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))) k ≠ 0) (h_mp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))))) (h5 : ∀ (k : Fin d1), dense W₅ b₅ (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h6 : ∀ (k : Fin d1), dense W₆ b₆ ((relu d1 ∘ dense W₅ b₅) (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))))) k ≠ 0) : HasVJPAt (cifarCnnForward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇) x

CIFAR 2D CNN (no BN) whole-network VJP at a smooth point.

The composed backward of the full Chapter-4 forward equals the pdiv-contracted Jacobian, conditional on smoothness at the six ReLU kinks and the two MaxPools. Built by vjp_comp_at through convRelu → convRelu → maxPool → convRelu → convRelu → maxPool → denseRelu → denseRelu → dense. The Chapter-4 sibling of mnistCnnNoBn_has_vjp_at (two conv stages, two pools).

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.cifarCnn_has_vjp_at_correct {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) (h1 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₁ b₁ x k ≠ 0) (h2 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₂ b₂ ((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x) k ≠ 0) (h_mp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), flatConv W₃ b₃ (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x)) k ≠ 0) (h4 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), flatConv W₄ b₄ ((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))) k ≠ 0) (h_mp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))))) (h5 : ∀ (k : Fin d1), dense W₅ b₅ (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h6 : ∀ (k : Fin d1), dense W₆ b₆ ((relu d1 ∘ dense W₅ b₅) (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₁ b₁) x))))) k ≠ 0) (dy : Vec nClasses) (i : Fin (ic * (2 * (2 * h)) * (2 * (2 * w)))) : (cifarCnn_has_vjp_at W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ hc1 hc2 hh hw x h1 h2 h_mp1 h3 h4 h_mp2 h5 h6).backward dy i = ∑ j : Fin nClasses, pdiv (cifarCnnForward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇) x i j * dy j

Public correctness theorem for cifarCnn_has_vjp_at — the Chapter-4 CIFAR CNN's backward equals the pdiv-contracted Jacobian.

noncomputable def Proofs.Tiny.T0 : Tensor3 1 (2 * (2 * 1)) (2 * (2 * 1))

16 distinct positive values, 4×4 row-major ⇒ positionally injective. Typed at the 2·(2·1) spatial form so it lines up syntactically with the forward's stage-1 input shape (no 2*2 vs 2*(2*1) cast friction).

Equations

• Proofs.Tiny.T0 x✝ hi wi = ↑(4 * ↑hi + ↑wi + 1)

noncomputable def Proofs.Tiny.X : Vec (1 * (2 * (2 * 1)) * (2 * (2 * 1)))

Whole-network input, the flattened T0 (Vec 16).

Equations

• Proofs.Tiny.X = Proofs.Tiny.T0.flatten

noncomputable def Proofs.Tiny.K : Kernel4 1 1 1 1

Every conv: 1→1, 1×1 unit kernel ⇒ identity.

Equations

• Proofs.Tiny.K x✝³ x✝² x✝¹ x✝ = 1

noncomputable def Proofs.Tiny.Bz : Vec 1

Equations

• Proofs.Tiny.Bz x✝ = 0

noncomputable def Proofs.Tiny.Wd5 : Mat (1 * 1 * 1) 1

Dense heads: nonnegative weights + a strictly-positive bias keep every activation off the ReLU kink.

Equations

• Proofs.Tiny.Wd5 x✝¹ x✝ = 1

noncomputable def Proofs.Tiny.Wd6 : Mat 1 1

Equations

• Proofs.Tiny.Wd6 x✝¹ x✝ = 1

noncomputable def Proofs.Tiny.Bp : Vec 1

Equations

• Proofs.Tiny.Bp x✝ = 1

noncomputable def Proofs.Tiny.Wd7 : Mat 1 2

Equations

• Proofs.Tiny.Wd7 x✝¹ x✝ = 1

noncomputable def Proofs.Tiny.Bz2 : Vec 2

Equations

• Proofs.Tiny.Bz2 x✝ = 0

theorem Proofs.Tiny.T0_pos (ci : Fin 1) (hi wi : Fin (2 * (2 * 1))) : 0 < T0 ci hi wi

theorem Proofs.Tiny.T0_inj (ci : Fin 1) (r r' s s' : Fin (2 * (2 * 1))) (h : T0 ci r s = T0 ci r' s') : r = r' ∧ s = s'

T0 is positionally injective: 4·hi + wi + 1 pins down (hi, wi).

theorem Proofs.Tiny.X_pos (k : Fin (1 * (2 * (2 * 1)) * (2 * (2 * 1)))) : 0 < X k

theorem Proofs.Tiny.conv2dK_id {h w : ℕ} (t : Tensor3 1 h w) : conv2d K Bz t = t

1×1 unit conv is the identity (single channel).

theorem Proofs.Tiny.flatConvK_id {h w : ℕ} (v : Vec (1 * h * w)) : flatConv K Bz v = v

Hence flatConv K Bz is the identity at any spatial size.

theorem Proofs.Tiny.CRK_id {h w : ℕ} (v : Vec (1 * h * w)) (hv : ∀ (i : Fin (1 * h * w)), 0 < v i) : (relu (1 * h * w) ∘ flatConv K Bz) v = v

The conv→relu block returns its (positive) input unchanged.

theorem Proofs.Tiny.stage1_X : ((relu (1 * (2 * (2 * 1)) * (2 * (2 * 1))) ∘ flatConv K Bz) ∘ relu (1 * (2 * (2 * 1)) * (2 * (2 * 1))) ∘ flatConv K Bz) X = X

Both stage-1 conv→relu blocks fold (identity convs, positive ReLUs) to X.

theorem Proofs.Tiny.pool1_eq : maxPoolFlat 1 (2 * 1) (2 * 1) X = (maxPool2 T0).flatten

The first pool collapses (identity convs) to the maxpool of T0.

theorem Proofs.Tiny.pool1X_pos (k : Fin (1 * (2 * 1) * (2 * 1))) : 0 < maxPoolFlat 1 (2 * 1) (2 * 1) X k

The first pool's output is everywhere positive.

theorem Proofs.Tiny.unflatten_pos {c h w : ℕ} {v : Vec (c * h * w)} (hv : ∀ (k : Fin (c * h * w)), 0 < v k) (ci : Fin c) (hi : Fin h) (wi : Fin w) : 0 < Tensor3.unflatten v ci hi wi

A positive vector unflattens to a positive tensor.

theorem Proofs.Tiny.pool2X_pos (k : Fin (1 * 1 * 1)) : 0 < maxPoolFlat 1 1 1 (maxPoolFlat 1 (2 * 1) (2 * 1) X) k

The second pool's input (= the first pool's output, post identity stage-2) is everywhere positive.

theorem Proofs.Tiny.stage2_pool1 : ((relu (1 * (2 * 1) * (2 * 1)) ∘ flatConv K Bz) ∘ relu (1 * (2 * 1) * (2 * 1)) ∘ flatConv K Bz) (maxPoolFlat 1 (2 * 1) (2 * 1) X) = maxPoolFlat 1 (2 * 1) (2 * 1) X

Both stage-2 conv→relu blocks fold to the (positive) first-pool output.

theorem Proofs.Tiny.maxPool2T0_val (r s : Fin (2 * 1)) : maxPool2 T0 0 r s = ↑(8 * ↑r + 2 * ↑s + 6)

The four first-pool window maxima are 8·r + 2·s + 6 (i.e. 6,8,14,16): T0 is strictly increasing in row-major, so each 2×2 window's max is its bottom-right corner. Proved by folding the real maxes back through Nat.cast_max and discharging the resulting Nat identity with omega.

theorem Proofs.Tiny.pool1_inj (ci : Fin 1) (r r' s s' : Fin (2 * 1)) : maxPool2 T0 ci r s = maxPool2 T0 ci r' s' → r = r' ∧ s = s'

Hence the first pool's output is positionally injective (the four window maxima are pairwise distinct) — the second pool's no-tie condition.

noncomputable def Proofs.Tiny.cifarTinyCnn_has_vjp_at : HasVJPAt (cifarCnnForward K Bz K Bz K Bz K Bz Wd5 Bp Wd6 Bp Wd7 Bz2) X

Unconditional whole-network VJP for a concrete tiny CIFAR CNN. Every smoothness hypothesis of cifarCnn_has_vjp_at is discharged — the two no-tie conditions via positional injectivity (maxPool2Smooth_of_injective, the second through pool1_inj), the six ReLU conditions via positivity — so the statement carries no side conditions and stays in the three-axiom closure.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.Tiny.cifarTinyCnn_has_vjp_correct (dy : Vec 2) (i : Fin (1 * (2 * (2 * 1)) * (2 * (2 * 1)))) : cifarTinyCnn_has_vjp_at.backward dy i = ∑ j : Fin 2, pdiv (cifarCnnForward K Bz K Bz K Bz K Bz Wd5 Bp Wd6 Bp Wd7 Bz2) X i j * dy j

Public unconditional correctness theorem — the concrete tiny CIFAR CNN's backward equals the pdiv-Jacobian VJP, no hypotheses.

noncomputable def Proofs.cifarCnn8Forward {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) → Vec nClasses

The deeper (8-conv) CIFAR forward, flattened. Four conv→conv→pool stages (ic→c1→c1, c1→c2→c2, c2→c3→c3, c3→c4→c4) then dense 3-head.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.cifarCnn8_has_vjp_at {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hc3 : 0 < c3) (hc4 : 0 < c4) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) (hf1 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), flatConv W₁ b₁ x k ≠ 0) (hf2 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), flatConv W₂ b₂ ((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x) k ≠ 0) (hp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))) (hf3 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), flatConv W₃ b₃ (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)) k ≠ 0) (hf4 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), flatConv W₄ b₄ ((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))) k ≠ 0) (hp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))) (hf5 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₅ b₅ (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)))) k ≠ 0) (hf6 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₆ b₆ ((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))) k ≠ 0) (hp3 : MaxPool2Smooth (Tensor3.unflatten (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))) (hf7 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), flatConv W₇ b₇ (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)))))) k ≠ 0) (hf8 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), flatConv W₈ b₈ ((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))) k ≠ 0) (hp4 : MaxPool2Smooth (Tensor3.unflatten (((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))))) (hf9 : ∀ (k : Fin d1), dense W₉ b₉ (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)))))))) k ≠ 0) (hfa : ∀ (k : Fin d1), dense Wa ba ((relu d1 ∘ dense W₉ b₉) (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))))) k ≠ 0) : HasVJPAt (cifarCnn8Forward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ W₈ b₈ W₉ b₉ Wa ba Wb bb) x

Deeper (8-conv) CIFAR CNN (no BN) whole-network VJP at a smooth point. Conditional on the twelve ReLU smoothness kinks and the four MaxPools; built by vjp_comp_at through convRelu×8 / maxPool×4 / denseRelu×2 / dense. The 4-stage sibling of cifarCnn_has_vjp_at. The smoothness side conditions are supplied opaquely (hf1 … hf12, hp1 … hp4) — they discharge for a concrete instance the same way Tiny.cifarTinyCnn_has_vjp_at discharges the 2-stage ones.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.cifarCnn8_has_vjp_at_correct {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hc3 : 0 < c3) (hc4 : 0 < c4) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) (hf1 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), flatConv W₁ b₁ x k ≠ 0) (hf2 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), flatConv W₂ b₂ ((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x) k ≠ 0) (hp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))) (hf3 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), flatConv W₃ b₃ (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)) k ≠ 0) (hf4 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), flatConv W₄ b₄ ((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))) k ≠ 0) (hp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))) (hf5 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₅ b₅ (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)))) k ≠ 0) (hf6 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), flatConv W₆ b₆ ((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))) k ≠ 0) (hp3 : MaxPool2Smooth (Tensor3.unflatten (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))) (hf7 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), flatConv W₇ b₇ (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)))))) k ≠ 0) (hf8 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), flatConv W₈ b₈ ((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))) k ≠ 0) (hp4 : MaxPool2Smooth (Tensor3.unflatten (((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))))) (hf9 : ∀ (k : Fin d1), dense W₉ b₉ (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x)))))))) k ≠ 0) (hfa : ∀ (k : Fin d1), dense Wa ba ((relu d1 ∘ dense W₉ b₉) (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ flatConv W₁ b₁) x))))))))) k ≠ 0) (dy : Vec nClasses) (i : Fin (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) : (cifarCnn8_has_vjp_at W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ W₈ b₈ W₉ b₉ Wa ba Wb bb hc1 hc2 hc3 hc4 hh hw x hf1 hf2 hp1 hf3 hf4 hp2 hf5 hf6 hp3 hf7 hf8 hp4 hf9 hfa).backward dy i = ∑ j : Fin nClasses, pdiv (cifarCnn8Forward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ W₈ b₈ W₉ b₉ Wa ba Wb bb) x i j * dy j

Public correctness theorem for cifarCnn8_has_vjp_at — backward equals the pdiv-contracted Jacobian.

noncomputable def Proofs.convBnReluPC_has_vjp_at {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (v : Vec (ic * h * w)) (h_smooth : ∀ (k : Fin (oc * h * w)), bnPerChannelTensor3 oc h w ε γ β (flatConv W b v) k ≠ 0) : HasVJPAt (relu (oc * h * w) ∘ bnPerChannelTensor3 oc h w ε γ β ∘ flatConv W b) v

conv → per-channel-BN → relu block VJP at a smooth point. The per-channel (bnPerChannelTensor3, m=h·w) sibling of convBnRelu_has_vjp_at: the same two vjp_comp_at chain with bnPerChannelTensor3 (vector γ/β [oc], its own block-diagonal VJP) in place of the scalar-global bnForward.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.convBnReluPC_differentiableAt {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (v : Vec (ic * h * w)) (h_smooth : ∀ (k : Fin (oc * h * w)), bnPerChannelTensor3 oc h w ε γ β (flatConv W b v) k ≠ 0) : DifferentiableAt ℝ (relu (oc * h * w) ∘ bnPerChannelTensor3 oc h w ε γ β ∘ flatConv W b) v

conv → per-channel-BN → relu is differentiable at a smooth point.

noncomputable def Proofs.cifarCnnBnForward {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) : Vec (ic * (2 * (2 * h)) * (2 * (2 * w))) → Vec nClasses

The Chapter-4 BatchNorm CIFAR forward: cifarCnnForward with a per-example per-channel bnPerChannelTensor3 (m=h·w) inserted between each conv and its ReLU (four BN layers, scalar εᵢ, per-channel vector γᵢ, βᵢ : Vec cᵢ).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.cifarCnnBn_has_vjp_at {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (hε₁ : 0 < ε₁) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (hε₂ : 0 < ε₂) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (hε₃ : 0 < ε₃) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (hε₄ : 0 < ε₄) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) (h1 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ (flatConv W₁ b₁ x) k ≠ 0) (h2 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ (flatConv W₂ b₂ ((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)) k ≠ 0) (h_mp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ (flatConv W₃ b₃ (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) k ≠ 0) (h4 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ (flatConv W₄ b₄ ((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h_mp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) (h5 : ∀ (k : Fin d1), dense W₅ b₅ (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h6 : ∀ (k : Fin d1), dense W₆ b₆ ((relu d1 ∘ dense W₅ b₅) (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) k ≠ 0) : HasVJPAt (cifarCnnBnForward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ W₆ b₆ W₇ b₇) x

BN-CIFAR whole-network VJP at a (post-BN) smooth point. The composed backward equals the pdiv-contracted Jacobian, conditional on 0 < εᵢ and smoothness at the six ReLU kinks (now reading the post-BN pre-activations) and the two MaxPools. Chains convBnRelu → convBnRelu → maxPool → convBnRelu → convBnRelu → maxPool → denseRelu → denseRelu → dense through vjp_comp_at. The BatchNorm sibling of cifarCnn_has_vjp_at.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.cifarCnnBn_has_vjp_at_correct {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (hε₁ : 0 < ε₁) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (hε₂ : 0 < ε₂) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (hε₃ : 0 < ε₃) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (hε₄ : 0 < ε₄) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) (h1 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ (flatConv W₁ b₁ x) k ≠ 0) (h2 : ∀ (k : Fin (c1 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ (flatConv W₂ b₂ ((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)) k ≠ 0) (h_mp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ (flatConv W₃ b₃ (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) k ≠ 0) (h4 : ∀ (k : Fin (c2 * (2 * h) * (2 * w))), bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ (flatConv W₄ b₄ ((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h_mp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) (h5 : ∀ (k : Fin d1), dense W₅ b₅ (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h6 : ∀ (k : Fin d1), dense W₆ b₆ ((relu d1 ∘ dense W₅ b₅) (maxPoolFlat c2 h w (((relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c2 (2 * h) (2 * w) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * h) (2 * w) (((relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c1 (2 * (2 * h)) (2 * (2 * w)) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) k ≠ 0) (dy : Vec nClasses) (i : Fin (ic * (2 * (2 * h)) * (2 * (2 * w)))) : (cifarCnnBn_has_vjp_at W₁ b₁ ε₁ γ₁ β₁ hε₁ W₂ b₂ ε₂ γ₂ β₂ hε₂ W₃ b₃ ε₃ γ₃ β₃ hε₃ W₄ b₄ ε₄ γ₄ β₄ hε₄ W₅ b₅ W₆ b₆ W₇ b₇ hc1 hc2 hh hw x h1 h2 h_mp1 h3 h4 h_mp2 h5 h6).backward dy i = ∑ j : Fin nClasses, pdiv (cifarCnnBnForward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ W₆ b₆ W₇ b₇) x i j * dy j

Public correctness theorem for cifarCnnBn_has_vjp_at — the BN-CIFAR CNN's backward equals the pdiv-contracted Jacobian.

noncomputable def Proofs.cifarCnnBn8Forward {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (ε₅ : ℝ) (γ₅ β₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (ε₆ : ℝ) (γ₆ β₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (ε₇ : ℝ) (γ₇ β₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (ε₈ : ℝ) (γ₈ β₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) → Vec nClasses

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.cifarCnnBn8_has_vjp_at {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (hε₁ : 0 < ε₁) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (hε₂ : 0 < ε₂) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (hε₃ : 0 < ε₃) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (hε₄ : 0 < ε₄) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (ε₅ : ℝ) (γ₅ β₅ : Vec c3) (hε₅ : 0 < ε₅) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (ε₆ : ℝ) (γ₆ β₆ : Vec c3) (hε₆ : 0 < ε₆) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (ε₇ : ℝ) (γ₇ β₇ : Vec c4) (hε₇ : 0 < ε₇) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (ε₈ : ℝ) (γ₈ β₈ : Vec c4) (hε₈ : 0 < ε₈) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hc3 : 0 < c3) (hc4 : 0 < c4) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) (h1 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ (flatConv W₁ b₁ x) k ≠ 0) (h2 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ (flatConv W₂ b₂ ((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)) k ≠ 0) (h3 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ (flatConv W₃ b₃ (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) k ≠ 0) (h4 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ (flatConv W₄ b₄ ((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h5 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ (flatConv W₅ b₅ (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) k ≠ 0) (h6 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ (flatConv W₆ b₆ ((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))))) k ≠ 0) (h7 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ (flatConv W₇ b₇ (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))) k ≠ 0) (h8 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ (flatConv W₈ b₈ ((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))))))) k ≠ 0) (h_mp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) (h_mp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) (h_mp3 : MaxPool2Smooth (Tensor3.unflatten (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))) (h_mp4 : MaxPool2Smooth (Tensor3.unflatten (((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))))) (h9 : ∀ (k : Fin d1), dense W₉ b₉ (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))))))) k ≠ 0) (ha : ∀ (k : Fin d1), dense Wa ba ((relu d1 ∘ dense W₉ b₉) (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))))) k ≠ 0) : HasVJPAt (cifarCnnBn8Forward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ ε₅ γ₅ β₅ W₆ b₆ ε₆ γ₆ β₆ W₇ b₇ ε₇ γ₇ β₇ W₈ b₈ ε₈ γ₈ β₈ W₉ b₉ Wa ba Wb bb) x

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.cifarCnnBn8_has_vjp_at_correct {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (hε₁ : 0 < ε₁) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (hε₂ : 0 < ε₂) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (hε₃ : 0 < ε₃) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (hε₄ : 0 < ε₄) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (ε₅ : ℝ) (γ₅ β₅ : Vec c3) (hε₅ : 0 < ε₅) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (ε₆ : ℝ) (γ₆ β₆ : Vec c3) (hε₆ : 0 < ε₆) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (ε₇ : ℝ) (γ₇ β₇ : Vec c4) (hε₇ : 0 < ε₇) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (ε₈ : ℝ) (γ₈ β₈ : Vec c4) (hε₈ : 0 < ε₈) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (hc1 : 0 < c1) (hc2 : 0 < c2) (hc3 : 0 < c3) (hc4 : 0 < c4) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) (h1 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ (flatConv W₁ b₁ x) k ≠ 0) (h2 : ∀ (k : Fin (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))), bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ (flatConv W₂ b₂ ((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)) k ≠ 0) (h3 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ (flatConv W₃ b₃ (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) k ≠ 0) (h4 : ∀ (k : Fin (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w))))), bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ (flatConv W₄ b₄ ((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))) k ≠ 0) (h5 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ (flatConv W₅ b₅ (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) k ≠ 0) (h6 : ∀ (k : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))), bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ (flatConv W₆ b₆ ((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))))) k ≠ 0) (h7 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ (flatConv W₇ b₇ (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))) k ≠ 0) (h8 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ (flatConv W₈ b₈ ((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))))))) k ≠ 0) (h_mp1 : MaxPool2Smooth (Tensor3.unflatten (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))) (h_mp2 : MaxPool2Smooth (Tensor3.unflatten (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))) (h_mp3 : MaxPool2Smooth (Tensor3.unflatten (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))) (h_mp4 : MaxPool2Smooth (Tensor3.unflatten (((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))))) (h9 : ∀ (k : Fin d1), dense W₉ b₉ (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x)))))))) k ≠ 0) (ha : ∀ (k : Fin d1), dense Wa ba ((relu d1 ∘ dense W₉ b₉) (maxPoolFlat c4 h w (((relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ ∘ flatConv W₈ b₈) ∘ relu (c4 * (2 * h) * (2 * w)) ∘ bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ ∘ flatConv W₇ b₇) (maxPoolFlat c3 (2 * h) (2 * w) (((relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ ∘ flatConv W₆ b₆) ∘ relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) ∘ bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ ∘ flatConv W₅ b₅) (maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) (((relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ ∘ flatConv W₄ b₄) ∘ relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) ∘ bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ ∘ flatConv W₃ b₃) (maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) (((relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ ∘ flatConv W₂ b₂) ∘ relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) ∘ bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ ∘ flatConv W₁ b₁) x))))))))) k ≠ 0) (dy : Vec nClasses) (i : Fin (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) : (cifarCnnBn8_has_vjp_at W₁ b₁ ε₁ γ₁ β₁ hε₁ W₂ b₂ ε₂ γ₂ β₂ hε₂ W₃ b₃ ε₃ γ₃ β₃ hε₃ W₄ b₄ ε₄ γ₄ β₄ hε₄ W₅ b₅ ε₅ γ₅ β₅ hε₅ W₆ b₆ ε₆ γ₆ β₆ hε₆ W₇ b₇ ε₇ γ₇ β₇ hε₇ W₈ b₈ ε₈ γ₈ β₈ hε₈ W₉ b₉ Wa ba Wb bb hc1 hc2 hc3 hc4 hh hw x h1 h2 h3 h4 h5 h6 h7 h8 h_mp1 h_mp2 h_mp3 h_mp4 h9 ha).backward dy i = ∑ j : Fin nClasses, pdiv (cifarCnnBn8Forward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ ε₅ γ₅ β₅ W₆ b₆ ε₆ γ₆ β₆ W₇ b₇ ε₇ γ₇ β₇ W₈ b₈ ε₈ γ₈ β₈ W₉ b₉ Wa ba Wb bb) x i j * dy j