Documentation

LeanMlir.Proofs.Nets.ConvNeXt.ConvNeXtParamGrad

ConvNeXt-T — every parameter gradient node IS the loss's derivative in that parameter #

cnx_net_tiedGB says each of the 182 parameter gradient nodes denotes its layer's parameter Jacobian contracted with the cotangent the emitted backward chain threads to it, the chain's top being the smoothed-loss cotangent. cnx_net_lossGrad composes that with the chain: for any loss L of the logits whose gradient at the net's output is g, every node is ∂L/∂θ of the WHOLE net cnxNetB with that one parameter varied. cnx_net_lossGrad_smoothedCE discharges hL for the label-smoothed loss the artifacts ship (smoothedBatchLossDiv, whose gradient is the softmaxDiv cotangent the render emits).

How. No ConvNeXt op couples examples, so the work is per example and lifted once:

Per example (at variable widths): the loss read at each activation inside a block, a downsample, the stem and the head has the tie's own per-example cotangent as its gradient (cnxBlk_hasGradAt, cnxDown_hasGradAt, …). Every stage VJP is global — GELU has no kink and LayerNorm needs only 0 < ε — so each step is one HasGradAt.comp_global, and the channel-LN step is chanLNTensor3Back_eq_chanLN_vjp.
Lifted (HasGradAt.pdiv_param_batchMap_through, ParamGrad): read against the linear loss ⟨·, dyₙ⟩ per example, those gradients turn each tied node's Σ_n Σ_j ∂per/∂θ · cotₙ into ∂G/∂θ of the batched block, G the loss at the block's output.
Per net: the loss read after each stage (cnxSuf*), pulled back through the certified batched block, downsample and head VJPs (cnxBlockCotInB_eq_vjp, cnxDownCotInB_eq_vjp, cnxHeadDyB_eq_vjp), and each Φ identified with the whole net at updated weights by a standalone cnx_factor_* theorem.

Two nodes are stated differently from the tie. The stem's bias node is emitted as a stride-1 convBiasGradB over a free xstem; its Jacobian in the bias is the channel indicator whatever the conv, so it equals the patchify conv's (GradNodeB.pdiv_bias_of_split). The classifier bias node biasGradB is the identity on its operand and the batch reduce is emitted text, so the statement is the sum over the batch of the node's per-example slices.

Hypotheses. 0 < ε (the LayerNorms' VJPs); no smoothness hypothesis. For the smoothed loss, every example's target sums to one and 0 < nC. Drop-path and the bf16 nodes are outside this statement, as they are outside the tie.

theorem Proofs.CnxTiePoCGB.rowLNVecFlat_gamma_differentiable (s c : ℕ) (ε : ℝ) (β : Vec c) (x : Vec (s * c)) :

Differentiable ℝ fun (γ : Vec c) => rowLNVecFlat s c ε γ β x

theorem Proofs.CnxTiePoCGB.rowLNVecFlat_beta_differentiable (s c : ℕ) (ε : ℝ) (γ : Vec c) (x : Vec (s * c)) :

Differentiable ℝ fun (β : Vec c) => rowLNVecFlat s c ε γ β x

theorem Proofs.CnxTiePoCGB.chanLNTensor3_gamma_differentiable (c h w : ℕ) (ε : ℝ) (β : Vec c) (x : Vec (c * h * w)) :

Differentiable ℝ fun (γ : Vec c) => chanLNTensor3 c h w ε γ β x

theorem Proofs.CnxTiePoCGB.chanLNTensor3_beta_differentiable (c h w : ℕ) (ε : ℝ) (γ : Vec c) (x : Vec (c * h * w)) :

Differentiable ℝ fun (β : Vec c) => chanLNTensor3 c h w ε γ β x

theorem Proofs.CnxTiePoCGB.layerScaleCh_gamma_differentiable (c h w : ℕ) (x : Vec (c * h * w)) :

Differentiable ℝ fun (γ : Vec c) => layerScale (fun (k : Fin (c * h * w)) => γ (StableHLO.chanIdx c h w k)) x

theorem Proofs.CnxTiePoCGB.flatConvStride4_weight_differentiable {ic oc h w kH kW : ℕ} (b : Vec oc) (y : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :

Differentiable ℝ fun (θ : Vec (oc * ic * kH * kW)) => flatConvStride4 (Kernel4.unflatten θ) b y

theorem Proofs.CnxTiePoCGB.flatConvStride4_bias_differentiable {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (y : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :

Differentiable ℝ fun (θ : Vec oc) => flatConvStride4 W θ y

noncomputable def Proofs.CnxTiePoCGB.cnxPostP {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (c * h * w) → Vec (c * h * w)

The block after the project conv: layer scale, then the identity skip.

Equations

Proofs.CnxTiePoCGB.cnxPostP h w p y u i = Proofs.layerScale (fun (k : Fin (c * h * w)) => p.sL (Proofs.StableHLO.chanIdx c h w k)) u i + y i

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPostE {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (cExp * h * w) → Vec (c * h * w)

The block after the expand conv (pre-GELU).

Equations

Proofs.CnxTiePoCGB.cnxPostE h w p y u = Proofs.CnxTiePoCGB.cnxPostP h w p y (Proofs.flatConv p.pW p.pB (Proofs.gelu (cExp * h * w) u))

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPostN {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (c * h * w) → Vec (c * h * w)

The block after the channel LN.

Equations

Proofs.CnxTiePoCGB.cnxPostN h w p y u = Proofs.CnxTiePoCGB.cnxPostE h w p y (Proofs.flatConv p.eW p.eB u)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPostD {c cExp : ℕ} (h w : ℕ) (ε : ℝ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (c * h * w) → Vec (c * h * w)

The block after the depthwise conv.

Equations

Proofs.CnxTiePoCGB.cnxPostD h w ε p y u = Proofs.CnxTiePoCGB.cnxPostN h w p y (Proofs.chanLNTensor3 c h w ε p.nG p.nB u)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxActD {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (c * h * w)

The depthwise conv's output.

Equations

Proofs.CnxTiePoCGB.cnxActD h w p y = Proofs.depthwiseFlat p.aW p.aB y

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxActNl {c cExp : ℕ} (h w : ℕ) (ε : ℝ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (c * h * w)

The channel LN's output.

Equations

Proofs.CnxTiePoCGB.cnxActNl h w ε p y = Proofs.chanLNTensor3 c h w ε p.nG p.nB (Proofs.CnxTiePoCGB.cnxActD h w p y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxActG {c cExp : ℕ} (h w : ℕ) (ε : ℝ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (cExp * h * w)

The GELU's output (the project conv's input).

Equations

Proofs.CnxTiePoCGB.cnxActG h w ε p y = Proofs.gelu (cExp * h * w) (Proofs.flatConv p.eW p.eB (Proofs.CnxTiePoCGB.cnxActNl h w ε p y))

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxActP {c cExp : ℕ} (h w : ℕ) (ε : ℝ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Vec (c * h * w)

The project conv's output (the layer scale's input).

Equations

Proofs.CnxTiePoCGB.cnxActP h w ε p y = Proofs.flatConv p.pW p.pB (Proofs.CnxTiePoCGB.cnxActG h w ε p y)

Instances For

theorem Proofs.CnxTiePoCGB.cnxPostP_differentiable {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Differentiable ℝ (cnxPostP h w p y)

theorem Proofs.CnxTiePoCGB.cnxPostE_differentiable {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Differentiable ℝ (cnxPostE h w p y)

theorem Proofs.CnxTiePoCGB.cnxPostN_differentiable {c cExp : ℕ} (h w : ℕ) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Differentiable ℝ (cnxPostN h w p y)

theorem Proofs.CnxTiePoCGB.cnxPostD_differentiable {c cExp : ℕ} (h w : ℕ) (ε : ℝ) (hε : 0 < ε) (p : CnxTiePoC.CnxTieBlk c cExp) (y : Vec (c * h * w)) :

Differentiable ℝ (cnxPostD h w ε p y)

theorem Proofs.CnxTiePoCGB.cnxBlk_hasGradAt {c cExp h w : ℕ} (ε : ℝ) (hε : 0 < ε) (p : CnxTiePoC.CnxTieBlk c cExp) (y dy : Vec (c * h * w)) {G : Vec (c * h * w) → Vec 1} (hG : HasGradAt G (p.fwdO ε y) dy) :

HasGradAt (fun (u : Vec (c * h * w)) => G fun (i : Fin (c * h * w)) => u i + y i) (layerScale (fun (k : Fin (c * h * w)) => p.sL (StableHLO.chanIdx c h w k)) (cnxActP h w ε p y)) dy ∧ HasGradAt (fun (u : Vec (c * h * w)) => G (cnxPostP h w p y u)) (cnxActP h w ε p y) (cnxCotP (fun (k : Fin (c * h * w)) => p.sL (StableHLO.chanIdx c h w k)) dy) ∧ HasGradAt (fun (u : Vec (cExp * h * w)) => G (cnxPostE h w p y u)) (flatConv p.eW p.eB (cnxActNl h w ε p y)) (blkCotE ε p.aW p.aB p.nG p.nB p.eW p.eB p.pW p.pB p.sL y dy) ∧ HasGradAt (fun (u : Vec (c * h * w)) => G (cnxPostN h w p y u)) (cnxActNl h w ε p y) (blkCotN ε p.aW p.aB p.nG p.nB p.eW p.eB p.pW p.pB p.sL y dy) ∧ HasGradAt (fun (u : Vec (c * h * w)) => G (cnxPostD h w ε p y u)) (cnxActD h w p y) (blkCotD ε p.aW p.aB p.nG p.nB p.eW p.eB p.pW p.pB p.sL y dy)

A block's cotangents are loss gradients, per example: from the gradient dy at the block output, the loss read after each activation has the tie's cotangent there — dy at the layer scale's output, cnxCotP at the project conv's, then blkCotE, blkCotN, blkCotD.

def Proofs.CnxTiePoCGB.cnxBlockLossTiedGB {c cExp : ℕ} (N : ℕ) {h w : ℕ} (xN epsStr cotN : String) (ε : ℝ) (p : CnxTiePoC.CnxTieBlk c cExp) (xin : Vec (N * (c * h * w))) (Φ : CnxTiePoC.CnxTieBlk c cExp → Vec 1) (dyOut : Vec (N * (c * h * w))) :

ConvNeXt block, every parameter node a loss derivative — the nine nodes cnxBlockChTiedGB ties, at the tie's batched activations and cotangents, Φ the loss at the block's output as a function of the block's weight record.

Equations

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

Instances For

theorem Proofs.CnxTiePoCGB.cnx_block_lossTiedGB {c cExp : ℕ} (N : ℕ) {h w : ℕ} (xN epsStr cotN : String) (ε : ℝ) (hε : 0 < ε) (p : CnxTiePoC.CnxTieBlk c cExp) (xin : Vec (N * (c * h * w))) {Lb : Vec (N * (c * h * w)) → Vec 1} {dyOut : Vec (N * (c * h * w))} (hLb : HasGradAt Lb (StableHLO.batchMap N (p.fwdO ε) xin) dyOut) {Φ : CnxTiePoC.CnxTieBlk c cExp → Vec 1} (hΦ : ∀ (p' : CnxTiePoC.CnxTieBlk c cExp), Φ p' = Lb (StableHLO.batchMap N (p'.fwdO ε) xin)) :

cnxBlockLossTiedGB N xN epsStr cotN ε p xin Φ dyOut

def Proofs.CnxTiePoCGB.cnxDownLossTiedGB {ci co : ℕ} (N : ℕ) {h w : ℕ} (xN epsStr cotN : String) (ε : ℝ) (p : CnxTiePoC.CnxTieDown ci co) (xin : Vec (N * (ci * (2 * h) * (2 * w)))) (Φ : CnxTiePoC.CnxTieDown ci co → Vec 1) (dyOut : Vec (N * (co * h * w))) :

Downsample, every parameter node a loss derivative — the four nodes cnxDownChTiedGB ties.

Equations

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

Instances For

theorem Proofs.CnxTiePoCGB.cnx_down_lossTiedGB {ci co : ℕ} (N : ℕ) {h w : ℕ} (xN epsStr cotN : String) (ε : ℝ) (p : CnxTiePoC.CnxTieDown ci co) (xin : Vec (N * (ci * (2 * h) * (2 * w)))) {Lb : Vec (N * (co * h * w)) → Vec 1} {dyOut : Vec (N * (co * h * w))} (hLb : HasGradAt Lb (StableHLO.batchMap N (p.fwdO ε) xin) dyOut) {Φ : CnxTiePoC.CnxTieDown ci co → Vec 1} (hΦ : ∀ (p' : CnxTiePoC.CnxTieDown ci co), Φ p' = Lb (StableHLO.batchMap N (p'.fwdO ε) xin)) :

cnxDownLossTiedGB N xN epsStr cotN ε p xin Φ dyOut

def Proofs.CnxTiePoCGB.cnxStemLossTiedGB {c : ℕ} (N : ℕ) {h w : ℕ} (xN epsStr cotN : String) (ε : ℝ) (Wst : Kernel4 c 3 4 4) (psb psng psnbt : Vec c) (x : Vec (N * (3 * (2 * (2 * h)) * (2 * (2 * w))))) (xstem : Vec (N * (3 * h * w))) (Φ : Kernel4 c 3 4 4 → Vec c → Vec c → Vec c → Vec 1) (dyStem : Vec (N * (c * h * w))) :

Stem, every parameter node a loss derivative — the four nodes cnxStemChTiedGB ties. The bias node is the emitted stride-1 convBiasGradB over a free xstem, as in the tie.

Equations

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

Instances For

theorem Proofs.CnxTiePoCGB.cnx_stem_lossTiedGB {c : ℕ} (N : ℕ) {h w : ℕ} (xN epsStr cotN : String) (ε : ℝ) (hε : 0 < ε) (Wst : Kernel4 c 3 4 4) (psb psng psnbt : Vec c) (x : Vec (N * (3 * (2 * (2 * h)) * (2 * (2 * w))))) (xstem : Vec (N * (3 * h * w))) {Lb : Vec (N * (c * h * w)) → Vec 1} {dyStem : Vec (N * (c * h * w))} (hLb : HasGradAt Lb (StableHLO.batchMap N (CnxTiePoC.cnxStemFwdO ε Wst psb psng psnbt) x) dyStem) {Φ : Kernel4 c 3 4 4 → Vec c → Vec c → Vec c → Vec 1} (hΦ : ∀ (W : Kernel4 c 3 4 4) (b γ β : Vec c), Φ W b γ β = Lb (StableHLO.batchMap N (CnxTiePoC.cnxStemFwdO ε W b γ β) x)) :

cnxStemLossTiedGB N xN epsStr cotN ε Wst psb psng psnbt x xstem Φ dyStem

noncomputable def Proofs.CnxTiePoCGB.cnxHeadO (h w : ℕ) {nC : ℕ} (ε : ℝ) (hng hnbt : Vec 768) (Wfc : Mat 768 nC) (bfc : Vec nC) :

Vec (768 * h * w) → Vec nC

The head per example: GAP, then LayerNorm at one row, then the dense classifier.

Equations

Proofs.CnxTiePoCGB.cnxHeadO h w ε hng hnbt Wfc bfc = Proofs.dense Wfc bfc ∘ Proofs.rowLNVecFlat 1 768 ε hng hnbt ∘ Proofs.globalAvgPoolFlat 768 h w

Instances For

def Proofs.CnxTiePoCGB.cnxHeadLossTiedGB (N : ℕ) {h w nC : ℕ} (xN epsStr cotN dN : String) (ε : ℝ) (hng hnbt : Vec 768) (Wfc : Mat 768 nC) (bfc : Vec nC) (xhead : Vec (N * (768 * h * w))) (Φ : Vec 768 → Vec 768 → Mat 768 nC → Vec nC → Vec 1) (g : Vec (N * nC)) :

Head, every parameter node a loss derivative — the four nodes cnxHeadChTiedGB ties. The classifier bias node is the identity on its operand (the batch reduce is emitted text), so its statement is the batch sum of the node's slices.

Equations

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

Instances For

theorem Proofs.CnxTiePoCGB.cnx_head_lossTiedGB (N : ℕ) {h w nC : ℕ} (xN epsStr cotN dN : String) (ε : ℝ) (hng hnbt : Vec 768) (Wfc : Mat 768 nC) (bfc : Vec nC) (xhead : Vec (N * (768 * h * w))) {L : Vec (N * nC) → Vec 1} {g : Vec (N * nC)} (hL : HasGradAt L (StableHLO.batchMap N (cnxHeadO h w ε hng hnbt Wfc bfc) xhead) g) {Φ : Vec 768 → Vec 768 → Mat 768 nC → Vec nC → Vec 1} (hΦ : ∀ (a b : Vec 768) (W : Mat 768 nC) (bb : Vec nC), Φ a b W bb = L (StableHLO.batchMap N (cnxHeadO h w ε a b W bb) xhead)) :

cnxHeadLossTiedGB N xN epsStr cotN dN ε hng hnbt Wfc bfc xhead Φ g

theorem Proofs.CnxTiePoCGB.cnxBlkB_hasGradAt_comp (N : ℕ) {c cExp h w : ℕ} (ε : ℝ) (hε : 0 < ε) (p : CnxTiePoC.CnxTieBlk c cExp) (X : Vec (N * (c * h * w))) {G : Vec (N * (c * h * w)) → Vec 1} {dY : Vec (N * (c * h * w))} (hG : HasGradAt G (StableHLO.batchMap N (p.fwdO ε) X) dY) :

HasGradAt (fun (y : Vec (N * (c * h * w))) => G (StableHLO.batchMap N (p.fwdO ε) y)) X (StableHLO.batchMapAux N (p.cotIn ε) X dY)

Pull the loss gradient back through a batched block's certified VJP: the cotangent is the tie's batchMapAux N (p.cotIn ε) (cnxBlockCotInB_eq_vjp).

theorem Proofs.CnxTiePoCGB.cnxDownB_hasGradAt_comp (N : ℕ) {ci co h w : ℕ} (ε : ℝ) (hε : 0 < ε) (p : CnxTiePoC.CnxTieDown ci co) (X : Vec (N * (ci * (2 * h) * (2 * w)))) {G : Vec (N * (co * h * w)) → Vec 1} {dY : Vec (N * (co * h * w))} (hG : HasGradAt G (StableHLO.batchMap N (p.fwdO ε) X) dY) :

HasGradAt (fun (y : Vec (N * (ci * (2 * h) * (2 * w)))) => G (StableHLO.batchMap N (p.fwdO ε) y)) X (StableHLO.batchMapAux N (p.cotIn ε) X dY)

…through a batched downsample (cnxDownCotInB_eq_vjp).

theorem Proofs.CnxTiePoCGB.cnxHeadB_hasGradAt_comp (N : ℕ) {h w nC : ℕ} (ε : ℝ) (hε : 0 < ε) (hng hnbt : Vec 768) (Wfc : Mat 768 nC) (bfc : Vec nC) (X : Vec (N * (768 * h * w))) {L : Vec (N * nC) → Vec 1} {g : Vec (N * nC)} (hL : HasGradAt L (StableHLO.batchMap N (cnxHeadO h w ε hng hnbt Wfc bfc) X) g) :

HasGradAt (fun (y : Vec (N * (768 * h * w))) => L (StableHLO.batchMap N (cnxHeadO h w ε hng hnbt Wfc bfc) y)) X (StableHLO.batchMapAux N (cnxHeadDyXheadChN ε hng hnbt Wfc bfc) X g)

…and through the batched head (cnxHeadDyB_eq_vjp).

noncomputable def Proofs.CnxTiePoCGB.cnxNetB (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

Vec (N * nC)

ConvNeXt-T, batched: the tie's forward, stage by stage — batchMap N of the stem, each block and downsample, then of the head.

Equations

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

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreS (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (96 * 56 * 56))

The stem's output — block b1's input (the tie's ib1).

Equations

Proofs.CnxTiePoCGB.cnxPreS N ε w = Proofs.StableHLO.batchMap N (Proofs.CnxTiePoC.cnxStemFwdO ε w.sW w.sb w.sγ w.sβ)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB1 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (96 * 56 * 56))

Stage b1's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB1 N ε w = Proofs.StableHLO.batchMap N (w.b1.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreS N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB2 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (96 * 56 * 56))

Stage b2's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB2 N ε w = Proofs.StableHLO.batchMap N (w.b2.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB1 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB3 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (96 * 56 * 56))

Stage b3's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB3 N ε w = Proofs.StableHLO.batchMap N (w.b3.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB2 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreD0 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (192 * 28 * 28))

Stage d0's output.

Equations

Proofs.CnxTiePoCGB.cnxPreD0 N ε w = Proofs.StableHLO.batchMap N (w.d0.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB3 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB4 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (192 * 28 * 28))

Stage b4's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB4 N ε w = Proofs.StableHLO.batchMap N (w.b4.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreD0 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB5 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (192 * 28 * 28))

Stage b5's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB5 N ε w = Proofs.StableHLO.batchMap N (w.b5.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB4 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB6 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (192 * 28 * 28))

Stage b6's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB6 N ε w = Proofs.StableHLO.batchMap N (w.b6.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB5 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreD1 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage d1's output.

Equations

Proofs.CnxTiePoCGB.cnxPreD1 N ε w = Proofs.StableHLO.batchMap N (w.d1.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB6 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB7 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b7's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB7 N ε w = Proofs.StableHLO.batchMap N (w.b7.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreD1 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB8 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b8's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB8 N ε w = Proofs.StableHLO.batchMap N (w.b8.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB7 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB9 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b9's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB9 N ε w = Proofs.StableHLO.batchMap N (w.b9.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB8 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB10 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b10's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB10 N ε w = Proofs.StableHLO.batchMap N (w.b10.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB9 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB11 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b11's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB11 N ε w = Proofs.StableHLO.batchMap N (w.b11.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB10 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB12 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b12's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB12 N ε w = Proofs.StableHLO.batchMap N (w.b12.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB11 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB13 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b13's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB13 N ε w = Proofs.StableHLO.batchMap N (w.b13.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB12 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB14 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b14's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB14 N ε w = Proofs.StableHLO.batchMap N (w.b14.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB13 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB15 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (384 * 14 * 14))

Stage b15's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB15 N ε w = Proofs.StableHLO.batchMap N (w.b15.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB14 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreD2 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (768 * 7 * 7))

Stage d2's output.

Equations

Proofs.CnxTiePoCGB.cnxPreD2 N ε w = Proofs.StableHLO.batchMap N (w.d2.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB15 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB16 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (768 * 7 * 7))

Stage b16's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB16 N ε w = Proofs.StableHLO.batchMap N (w.b16.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreD2 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB17 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (768 * 7 * 7))

Stage b17's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB17 N ε w = Proofs.StableHLO.batchMap N (w.b17.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB16 N ε w

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxPreB18 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (3 * 224 * 224)) → Vec (N * (768 * 7 * 7))

Stage b18's output.

Equations

Proofs.CnxTiePoCGB.cnxPreB18 N ε w = Proofs.StableHLO.batchMap N (w.b18.fwdO ε) ∘ Proofs.CnxTiePoCGB.cnxPreB17 N ε w

Instances For

theorem Proofs.CnxTiePoCGB.cnxPreS_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreS N ε w x = StableHLO.batchMap N (CnxTiePoC.cnxStemFwdO ε w.sW w.sb w.sγ w.sβ) x

theorem Proofs.CnxTiePoCGB.cnxPreB1_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB1 N ε w x = StableHLO.batchMap N (w.b1.fwdO ε) (cnxPreS N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB2_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB2 N ε w x = StableHLO.batchMap N (w.b2.fwdO ε) (cnxPreB1 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB3_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB3 N ε w x = StableHLO.batchMap N (w.b3.fwdO ε) (cnxPreB2 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreD0_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreD0 N ε w x = StableHLO.batchMap N (w.d0.fwdO ε) (cnxPreB3 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB4_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB4 N ε w x = StableHLO.batchMap N (w.b4.fwdO ε) (cnxPreD0 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB5_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB5 N ε w x = StableHLO.batchMap N (w.b5.fwdO ε) (cnxPreB4 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB6_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB6 N ε w x = StableHLO.batchMap N (w.b6.fwdO ε) (cnxPreB5 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreD1_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreD1 N ε w x = StableHLO.batchMap N (w.d1.fwdO ε) (cnxPreB6 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB7_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB7 N ε w x = StableHLO.batchMap N (w.b7.fwdO ε) (cnxPreD1 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB8_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB8 N ε w x = StableHLO.batchMap N (w.b8.fwdO ε) (cnxPreB7 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB9_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB9 N ε w x = StableHLO.batchMap N (w.b9.fwdO ε) (cnxPreB8 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB10_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB10 N ε w x = StableHLO.batchMap N (w.b10.fwdO ε) (cnxPreB9 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB11_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB11 N ε w x = StableHLO.batchMap N (w.b11.fwdO ε) (cnxPreB10 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB12_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB12 N ε w x = StableHLO.batchMap N (w.b12.fwdO ε) (cnxPreB11 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB13_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB13 N ε w x = StableHLO.batchMap N (w.b13.fwdO ε) (cnxPreB12 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB14_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB14 N ε w x = StableHLO.batchMap N (w.b14.fwdO ε) (cnxPreB13 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB15_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB15 N ε w x = StableHLO.batchMap N (w.b15.fwdO ε) (cnxPreB14 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreD2_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreD2 N ε w x = StableHLO.batchMap N (w.d2.fwdO ε) (cnxPreB15 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB16_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB16 N ε w x = StableHLO.batchMap N (w.b16.fwdO ε) (cnxPreD2 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB17_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB17 N ε w x = StableHLO.batchMap N (w.b17.fwdO ε) (cnxPreB16 N ε w x)

theorem Proofs.CnxTiePoCGB.cnxPreB18_apply (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxPreB18 N ε w x = StableHLO.batchMap N (w.b18.fwdO ε) (cnxPreB17 N ε w x)

noncomputable def Proofs.CnxTiePoCGB.cnxSufB18 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (768 * 7 * 7)) → Vec (N * nC)

The net after block b18 — the head.

Equations

Proofs.CnxTiePoCGB.cnxSufB18 N ε w = Proofs.StableHLO.batchMap N (Proofs.CnxTiePoCGB.cnxHeadO 7 7 ε w.hG w.hT w.Wfc w.bfc)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB17 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (768 * 7 * 7)) → Vec (N * nC)

The net after stage b17: stage b18, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB17 N ε w y = Proofs.CnxTiePoCGB.cnxSufB18 N ε w (Proofs.StableHLO.batchMap N (w.b18.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB16 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (768 * 7 * 7)) → Vec (N * nC)

The net after stage b16: stage b17, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB16 N ε w y = Proofs.CnxTiePoCGB.cnxSufB17 N ε w (Proofs.StableHLO.batchMap N (w.b17.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufD2 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (768 * 7 * 7)) → Vec (N * nC)

The net after stage d2: stage b16, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufD2 N ε w y = Proofs.CnxTiePoCGB.cnxSufB16 N ε w (Proofs.StableHLO.batchMap N (w.b16.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB15 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b15: stage d2, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB15 N ε w y = Proofs.CnxTiePoCGB.cnxSufD2 N ε w (Proofs.StableHLO.batchMap N (w.d2.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB14 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b14: stage b15, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB14 N ε w y = Proofs.CnxTiePoCGB.cnxSufB15 N ε w (Proofs.StableHLO.batchMap N (w.b15.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB13 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b13: stage b14, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB13 N ε w y = Proofs.CnxTiePoCGB.cnxSufB14 N ε w (Proofs.StableHLO.batchMap N (w.b14.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB12 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b12: stage b13, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB12 N ε w y = Proofs.CnxTiePoCGB.cnxSufB13 N ε w (Proofs.StableHLO.batchMap N (w.b13.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB11 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b11: stage b12, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB11 N ε w y = Proofs.CnxTiePoCGB.cnxSufB12 N ε w (Proofs.StableHLO.batchMap N (w.b12.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB10 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b10: stage b11, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB10 N ε w y = Proofs.CnxTiePoCGB.cnxSufB11 N ε w (Proofs.StableHLO.batchMap N (w.b11.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB9 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b9: stage b10, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB9 N ε w y = Proofs.CnxTiePoCGB.cnxSufB10 N ε w (Proofs.StableHLO.batchMap N (w.b10.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB8 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b8: stage b9, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB8 N ε w y = Proofs.CnxTiePoCGB.cnxSufB9 N ε w (Proofs.StableHLO.batchMap N (w.b9.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB7 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage b7: stage b8, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB7 N ε w y = Proofs.CnxTiePoCGB.cnxSufB8 N ε w (Proofs.StableHLO.batchMap N (w.b8.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufD1 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (384 * 14 * 14)) → Vec (N * nC)

The net after stage d1: stage b7, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufD1 N ε w y = Proofs.CnxTiePoCGB.cnxSufB7 N ε w (Proofs.StableHLO.batchMap N (w.b7.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB6 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (192 * 28 * 28)) → Vec (N * nC)

The net after stage b6: stage d1, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB6 N ε w y = Proofs.CnxTiePoCGB.cnxSufD1 N ε w (Proofs.StableHLO.batchMap N (w.d1.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB5 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (192 * 28 * 28)) → Vec (N * nC)

The net after stage b5: stage b6, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB5 N ε w y = Proofs.CnxTiePoCGB.cnxSufB6 N ε w (Proofs.StableHLO.batchMap N (w.b6.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB4 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (192 * 28 * 28)) → Vec (N * nC)

The net after stage b4: stage b5, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB4 N ε w y = Proofs.CnxTiePoCGB.cnxSufB5 N ε w (Proofs.StableHLO.batchMap N (w.b5.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufD0 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (192 * 28 * 28)) → Vec (N * nC)

The net after stage d0: stage b4, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufD0 N ε w y = Proofs.CnxTiePoCGB.cnxSufB4 N ε w (Proofs.StableHLO.batchMap N (w.b4.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB3 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (96 * 56 * 56)) → Vec (N * nC)

The net after stage b3: stage d0, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB3 N ε w y = Proofs.CnxTiePoCGB.cnxSufD0 N ε w (Proofs.StableHLO.batchMap N (w.d0.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB2 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (96 * 56 * 56)) → Vec (N * nC)

The net after stage b2: stage b3, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB2 N ε w y = Proofs.CnxTiePoCGB.cnxSufB3 N ε w (Proofs.StableHLO.batchMap N (w.b3.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufB1 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (96 * 56 * 56)) → Vec (N * nC)

The net after stage b1: stage b2, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufB1 N ε w y = Proofs.CnxTiePoCGB.cnxSufB2 N ε w (Proofs.StableHLO.batchMap N (w.b2.fwdO ε) y)

Instances For

noncomputable def Proofs.CnxTiePoCGB.cnxSufS (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) :

Vec (N * (96 * 56 * 56)) → Vec (N * nC)

The net after the stem: stage b1, then the rest.

Equations

Proofs.CnxTiePoCGB.cnxSufS N ε w y = Proofs.CnxTiePoCGB.cnxSufB1 N ε w (Proofs.StableHLO.batchMap N (w.b1.fwdO ε) y)

Instances For

theorem Proofs.CnxTiePoCGB.cnx_factor_stem (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (W : Kernel4 96 3 4 4) (b γ β : Vec 96) :

cnxNetB N ε { sW := W, sb := b, sγ := γ, sβ := β, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufS N ε w (StableHLO.batchMap N (CnxTiePoC.cnxStemFwdO ε W b γ β) x)

The net with the stem's parameters varied is the suffix after the stem at the varied stem.

theorem Proofs.CnxTiePoCGB.cnx_factor_b1 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 96 384) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := p, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB1 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreS N ε w x))

The net with stage b1's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b2 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 96 384) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := p, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB2 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB1 N ε w x))

The net with stage b2's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b3 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 96 384) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := p, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB3 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB2 N ε w x))

The net with stage b3's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_d0 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieDown 96 192) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := p, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufD0 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB3 N ε w x))

The net with stage d0's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b4 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 192 768) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := p, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB4 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreD0 N ε w x))

The net with stage b4's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b5 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 192 768) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := p, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB5 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB4 N ε w x))

The net with stage b5's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b6 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 192 768) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := p, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB6 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB5 N ε w x))

The net with stage b6's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_d1 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieDown 192 384) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := p, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufD1 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB6 N ε w x))

The net with stage d1's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b7 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := p, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB7 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreD1 N ε w x))

The net with stage b7's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b8 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := p, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB8 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB7 N ε w x))

The net with stage b8's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b9 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := p, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB9 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB8 N ε w x))

The net with stage b9's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b10 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := p, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB10 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB9 N ε w x))

The net with stage b10's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b11 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := p, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB11 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB10 N ε w x))

The net with stage b11's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b12 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := p, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB12 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB11 N ε w x))

The net with stage b12's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b13 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := p, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB13 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB12 N ε w x))

The net with stage b13's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b14 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := p, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB14 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB13 N ε w x))

The net with stage b14's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b15 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 384 1536) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := p, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB15 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB14 N ε w x))

The net with stage b15's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_d2 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieDown 384 768) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := p, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufD2 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB15 N ε w x))

The net with stage d2's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b16 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 768 3072) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := p, b17 := w.b17, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB16 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreD2 N ε w x))

The net with stage b16's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b17 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 768 3072) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := p, b18 := w.b18, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB17 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB16 N ε w x))

The net with stage b17's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_b18 (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (p : CnxTiePoC.CnxTieBlk 768 3072) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := p, hG := w.hG, hT := w.hT, Wfc := w.Wfc, bfc := w.bfc } x = cnxSufB18 N ε w (StableHLO.batchMap N (p.fwdO ε) (cnxPreB17 N ε w x))

The net with stage b18's weights varied is the suffix after it at the varied stage.

theorem Proofs.CnxTiePoCGB.cnx_factor_head (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) (a b : Vec 768) (W : Mat 768 nC) (bb : Vec nC) :

cnxNetB N ε { sW := w.sW, sb := w.sb, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, d0 := w.d0, b4 := w.b4, b5 := w.b5, b6 := w.b6, d1 := w.d1, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, d2 := w.d2, b16 := w.b16, b17 := w.b17, b18 := w.b18, hG := a, hT := b, Wfc := W, bfc := bb } x = StableHLO.batchMap N (cnxHeadO 7 7 ε a b W bb) (cnxPreB18 N ε w x)

The net with the head varied is the head at the varied parameters.

theorem Proofs.CnxTiePoCGB.cnx_forward_eq_head (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

cnxNetB N ε w x = StableHLO.batchMap N (cnxHeadO 7 7 ε w.hG w.hT w.Wfc w.bfc) (cnxPreB18 N ε w x)

The net's output is the head at block b18's output.

theorem Proofs.CnxTiePoCGB.cnx_logitsB_eq (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.batchMap N (dense w.Wfc w.bfc) (StableHLO.batchMap N (rowLNVecFlat 1 768 ε w.hG w.hT) (StableHLO.batchMap N (globalAvgPoolFlat 768 7 7) (cnxPreB18 N ε w x))) = cnxNetB N ε w x

The logits the tie's loss cotangent reads are cnxNetB's. The tie spells the head as three batched ops (batchMap_comp).

def Proofs.CnxTiePoCGB.CnxNetLossTiedGB (xN epsStr cotN dN : String) (N : ℕ) {nC : ℕ} (ε : ℝ) (w : CnxTiePoC.CnxTieWeights nC) (xstem : Vec (N * (3 * 56 * 56))) (x : Vec (N * (3 * 224 * 224))) (L : Vec (N * nC) → Vec 1) (g : Vec (N * nC)) :

Every ConvNeXt-T parameter gradient node is the derivative of L in that parameter, for a loss L of the logits and g the cotangent the chain starts from: the 182 nodes cnx_net_tiedGB ties, each at the cotangent the tie threads to it from g, stated against L of cnxNetB with that one parameter varied.

Equations

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

Instances For

theorem Proofs.CnxTiePoCGB.cnx_net_lossGrad (xN epsStr cotN dN : String) (N : ℕ) {nC : ℕ} (ε : ℝ) (hε : 0 < ε) (w : CnxTiePoC.CnxTieWeights nC) (xstem : Vec (N * (3 * 56 * 56))) (x : Vec (N * (3 * 224 * 224))) {L : Vec (N * nC) → Vec 1} {g : Vec (N * nC)} (hL : HasGradAt L (cnxNetB N ε w x) g) :

CnxNetLossTiedGB xN epsStr cotN dN N ε w xstem x L g

Every ConvNeXt-T parameter gradient node is the derivative of the loss in that parameter. For any loss L of the logits with gradient g at the net's output, each of the 182 nodes cnx_net_tiedGB ties — at the same cotangent — is ∂L/∂θ of the WHOLE net, cnxNetB with that one parameter varied (a stem field, a block's or downsample's record w.bk := p with one slot changed, or a head field).

Hypothesis: 0 < ε, the LayerNorms' (the tie itself needs none). The loss enters only through hL; cnx_net_lossGrad_smoothedCE discharges it for the loss the artifacts ship.

theorem Proofs.CnxTiePoCGB.cnx_net_lossGrad_smoothedCE (xN epsStr cotN dN aStr negAK bStr logN ohN : String) (N : ℕ) {nC : ℕ} (hK : 0 < nC) (ε α B : ℝ) (hε : 0 < ε) (w : CnxTiePoC.CnxTieWeights nC) (xstem : Vec (N * (3 * 56 * 56))) (x : Vec (N * (3 * 224 * 224))) (t : Vec (N * nC)) (ht : ∀ (n : Fin N), ∑ k : Fin nC, StableHLO.batchSlice N nC t n k = 1) :

CnxNetLossTiedGB xN epsStr cotN dN N ε w xstem x (smoothedBatchLossDiv N nC α B t) (StableHLO.den (smoothedLossCotGraphDiv N nC α B aStr negAK bStr logN ohN (cnxNetB N ε w x) t))

The loss the artifacts ship: every node is the derivative of the batched label-smoothed cross-entropy smoothedBatchLossDiv, g the softmaxDiv cotangent the render emits — the tie's own g, whose logits are cnxNetB N ε w x (cnx_logitsB_eq).