Documentation

LeanMlir.Proofs.Nets.EfficientNet.EfficientNetParamGrad

EfficientNet-B0 — every parameter gradient node IS the loss's derivative in that parameter #

efficientnet_net_tiedG says each of the 262 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 and each block's cotangent its certified VJP's backward. enet_net_lossGrad composes them: for any loss L of the logits whose gradient at the net's output is g, every node is ∂L/∂θ of the WHOLE net efficientnetForwardBFull with that one parameter varied. enet_net_lossGrad_smoothedCE discharges hL for the label-smoothed loss the artifacts ship.

How. MobileNetV2ParamGrad's shape:

The tail every MBConv block shares (depthwise BN → swish → squeeze-excite → 1×1 project → project BN, over EnTail): the loss read at each of its activations and its gradient, the tie's own cotangent (enetTail_hasGradAt). Every stage VJP is global (swish has no kink), and the tie's cotangents are spelled as the certified backwards (bnBackB, swBackB, seInB), so each step is one HasGradAt.comp.
The SE gate (enet_se_lossTiedB): with the block input dr held fixed, the SE output is the gated product dr ⊙ broadcast(σ(e2)) (seB_eq_gateMul), whose VJP in the gate is the emitted gateCotB (seGateMulBHasVJP). The loss read at the excite and reduce pre-activations then has the tie's cotE2 and cotE1 as its gradients, and the four SE dense nodes are its derivatives.
Per block kind (at variable widths): the expand stage (stride 1 or at the input grid 2h × 2w) or none, the depthwise, then the tail. The stride-1 bundle serves both the skip blocks and the two widenings (b9, b16): a skip block's body sees the loss u ↦ Gn (u + v), whose gradient at the body output is still dyOut (enet_resid_lossTiedG).
Bias nodes. B0 emits every conv and depthwise bias gradient with the BatchNorm β op (ConvBBetaTiedB); GradNodeB.biasBeta_eq_pdiv makes it the bias derivative.
Per net: the loss read after each block (enetSuf*), pulled back through the sixteen certified block VJPs and the head's, and each Φ identified with the whole net at updated weights by a standalone enet_factor_* theorem.

Hypotheses. B0Weights.EpsPos (every BN ε > 0), as in the tie; there is no smoothness hypothesis. For the smoothed loss, every example's target sums to one and 0 < nCls. Drop-path, classifier dropout and the bf16 nodes are outside this statement, as they are outside the tie.

noncomputable def Proofs.EnetTiePoCG.seGateMulB (N c h w : ℕ) (x : Vec (N * (c * h * w))) :

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

The SE block's gated product with the gate read at its pre-broadcast [N, c] value: x ⊙ broadcast(s), per example.

Equations

Proofs.EnetTiePoCG.seGateMulB N c h w x s J = x J * s (finProdFinEquiv ((finProdFinEquiv.symm J).1, Proofs.flatChannel c h w (finProdFinEquiv.symm J).2))

Instances For

noncomputable def Proofs.EnetTiePoCG.seGateMulBHasVJP (N c h w : ℕ) (x : Vec (N * (c * h * w))) :

HasVJP (seGateMulB N c h w x)

The gated product is linear in the gate; its backward is gateCotB, the emitted seReduceB.

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.seGateMulB_differentiable (N c h w : ℕ) (x : Vec (N * (c * h * w))) :

Differentiable ℝ (seGateMulB N c h w x)

theorem Proofs.EnetTiePoCG.seB_eq_gateMul (N : ℕ) {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x : Vec (N * (c * h * w))) :

seB N W₁ b₁ W₂ b₂ x = seGateMulB N c h w x (sigmoid (N * c) (StableHLO.batchMap N (dense W₂ b₂) (swish (N * r) (StableHLO.batchMap N (dense W₁ b₁) (StableHLO.batchMap N (globalAvgPoolFlat c h w) x)))))

The batched SE block, split at the gate. seB is the gated product of the block input with the sigmoid of the excite dense's output, the squeeze path computed on the whole batch — the spelling of the tie's SE activations s e1 z e2.

noncomputable def Proofs.EnetTiePoCG.enetSeGE2 (N : ℕ) {c h w : ℕ} (Gse : Vec (N * (c * h * w)) → Vec 1) (dr : Vec (N * (c * h * w))) :

Vec (N * c) → Vec 1

The loss at the excite dense's output (the sigmoid's input), the SE input dr held fixed. Gse is the loss at the SE output.

Equations

Proofs.EnetTiePoCG.enetSeGE2 N Gse dr e = Gse (Proofs.EnetTiePoCG.seGateMulB N c h w dr (Proofs.sigmoid (N * c) e))

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSeGE1 (N : ℕ) {c h w r : ℕ} (Gse : Vec (N * (c * h * w)) → Vec 1) (dr : Vec (N * (c * h * w))) (W₂ : Mat r c) (b₂ : Vec c) :

Vec (N * r) → Vec 1

The loss at the reduce dense's output (the swish's input), dr held fixed.

Equations

Proofs.EnetTiePoCG.enetSeGE1 N Gse dr W₂ b₂ e = Proofs.EnetTiePoCG.enetSeGE2 N Gse dr (Proofs.StableHLO.batchMap N (Proofs.dense W₂ b₂) (Proofs.swish (N * r) e))

Instances For

theorem Proofs.EnetTiePoCG.enetSe_hasGradAt {N c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (dr : Vec (N * (c * h * w))) {Gse : Vec (N * (c * h * w)) → Vec 1} {cot : Vec (N * (c * h * w))} (hG : HasGradAt Gse (seB N W₁ b₁ W₂ b₂ dr) cot) :

have e1 := StableHLO.batchMap N (dense W₁ b₁) (StableHLO.batchMap N (globalAvgPoolFlat c h w) dr); have e2 := StableHLO.batchMap N (dense W₂ b₂) (swish (N * r) e1); have cotE2 := BackLinks.sigBackB (N * c) e2 (BackLinks.gateCotB N c h w dr cot); HasGradAt (enetSeGE2 N Gse dr) e2 cotE2 ∧ HasGradAt (enetSeGE1 N Gse dr W₂ b₂) e1 (BackLinks.swBackB (N * r) e1 (StableHLO.rowDenseBackFlat N r c W₂ cotE2))

The SE gate's two cotangents are loss gradients: from the gradient cot at the SE output, the loss at the excite pre-activation has gradient σ'(e2) · gateCotB dr cot (the tie's cotE2), and at the reduce pre-activation the tie's cotE1.

def Proofs.EnetTiePoCG.enetSeLossTiedB {N c h w r : ℕ} (xN cotN : String) (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (dr : Vec (N * (c * h * w))) (Ψ : Mat c r → Vec r → Mat r c → Vec c → Vec 1) (cot : Vec (N * (c * h * w))) :

SE, every parameter node a loss derivative — the reduce and excite dense W/b nodes the tie states, Ψ the loss as a function of (W₁, b₁, W₂, b₂) with the SE input dr fixed.

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.enet_se_lossTiedB {N c h w r : ℕ} (xN cotN : String) (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (dr : Vec (N * (c * h * w))) {Gse : Vec (N * (c * h * w)) → Vec 1} {cot : Vec (N * (c * h * w))} (hG : HasGradAt Gse (seB N W₁ b₁ W₂ b₂ dr) cot) {Ψ : Mat c r → Vec r → Mat r c → Vec c → Vec 1} (hΨ : ∀ (a : Mat c r) (b : Vec r) (a' : Mat r c) (b' : Vec c), Ψ a b a' b' = Gse (seB N a b a' b' dr)) :

enetSeLossTiedB xN cotN W₁ b₁ W₂ b₂ dr Ψ cot

noncomputable def Proofs.EnetTiePoCG.enetTailDn (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (dc : Vec (N * (mid * h * w))) :

Vec (N * (mid * h * w))

The depthwise BN's output.

Equations

Proofs.EnetTiePoCG.enetTailDn N h w t dc = Proofs.StableHLO.bnBatchLA N mid h w t.dε t.dγ t.dβ dc

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailDr (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (dc : Vec (N * (mid * h * w))) :

Vec (N * (mid * h * w))

The depthwise swish's output (the SE input).

Equations

Proofs.EnetTiePoCG.enetTailDr N h w t dc = Proofs.swish (N * (mid * h * w)) (Proofs.EnetTiePoCG.enetTailDn N h w t dc)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailSe (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (dc : Vec (N * (mid * h * w))) :

Vec (N * (mid * h * w))

The SE output.

Equations

Proofs.EnetTiePoCG.enetTailSe N h w t dc = Proofs.seB N t.z1 t.zb1 t.z2 t.zb2 (Proofs.EnetTiePoCG.enetTailDr N h w t dc)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailPc (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (dc : Vec (N * (mid * h * w))) :

Vec (N * (oc * h * w))

The project conv's output.

Equations

Proofs.EnetTiePoCG.enetTailPc N h w t dc = Proofs.StableHLO.batchMap N (Proofs.flatConv t.pW t.pb) (Proofs.EnetTiePoCG.enetTailSe N h w t dc)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailB (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (dc : Vec (N * (mid * h * w))) :

Vec (N * (oc * h * w))

The tail's output, the project BN's.

Equations

Proofs.EnetTiePoCG.enetTailB N h w t dc = Proofs.StableHLO.bnBatchLA N oc h w t.pε t.pγ t.pβ (Proofs.EnetTiePoCG.enetTailPc N h w t dc)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailGPc (N h w : ℕ) {mid oc r : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (t : EnTail mid oc r) :

Vec (N * (oc * h * w)) → Vec 1

The loss at the project conv's output.

Equations

Proofs.EnetTiePoCG.enetTailGPc N h w Gb t z = Gb (Proofs.StableHLO.bnBatchLA N oc h w t.pε t.pγ t.pβ z)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailGSe (N h w : ℕ) {mid oc r : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (t : EnTail mid oc r) :

Vec (N * (mid * h * w)) → Vec 1

The loss at the SE output.

Equations

Proofs.EnetTiePoCG.enetTailGSe N h w Gb t u = Proofs.EnetTiePoCG.enetTailGPc N h w Gb t (Proofs.StableHLO.batchMap N (Proofs.flatConv t.pW t.pb) u)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailGDn (N h w : ℕ) {mid oc r : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (t : EnTail mid oc r) :

Vec (N * (mid * h * w)) → Vec 1

The loss at the depthwise BN's output.

Equations

Proofs.EnetTiePoCG.enetTailGDn N h w Gb t u = Proofs.EnetTiePoCG.enetTailGSe N h w Gb t (Proofs.seB N t.z1 t.zb1 t.z2 t.zb2 (Proofs.swish (N * (mid * h * w)) u))

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailGDc (N h w : ℕ) {mid oc r : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (t : EnTail mid oc r) :

Vec (N * (mid * h * w)) → Vec 1

The loss at the depthwise conv's output.

Equations

Proofs.EnetTiePoCG.enetTailGDc N h w Gb t z = Proofs.EnetTiePoCG.enetTailGDn N h w Gb t (Proofs.StableHLO.bnBatchLA N mid h w t.dε t.dγ t.dβ z)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailCotPbn (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (hp : 0 < t.pε) (dc : Vec (N * (mid * h * w))) (dy : Vec (N * (oc * h * w))) :

Vec (N * (oc * h * w))

The tie's cotPbn: the cotangent at the project conv's output.

Equations

Proofs.EnetTiePoCG.enetTailCotPbn N h w t hp dc dy = Proofs.BackLinks.bnBackB N oc h w t.pε hp t.pγ t.pβ (Proofs.EnetTiePoCG.enetTailPc N h w t dc) dy

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailCotSeOut (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (hp : 0 < t.pε) (dc : Vec (N * (mid * h * w))) (dy : Vec (N * (oc * h * w))) :

Vec (N * (mid * h * w))

The tie's cotSeOut: the cotangent at the SE output.

Equations

Proofs.EnetTiePoCG.enetTailCotSeOut N h w t hp dc dy = Proofs.BackLinks.cInB N t.pW t.pb (Proofs.EnetTiePoCG.enetTailCotPbn N h w t hp dc dy)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailCotDn (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (hp : 0 < t.pε) (dc : Vec (N * (mid * h * w))) (dy : Vec (N * (oc * h * w))) :

Vec (N * (mid * h * w))

The tie's cotDn: the cotangent at the depthwise BN's output.

Equations

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

Instances For

noncomputable def Proofs.EnetTiePoCG.enetTailCotDc (N h w : ℕ) {mid oc r : ℕ} (t : EnTail mid oc r) (hd : 0 < t.dε) (hp : 0 < t.pε) (dc : Vec (N * (mid * h * w))) (dy : Vec (N * (oc * h * w))) :

Vec (N * (mid * h * w))

The tie's cotDc: the cotangent at the depthwise conv's output.

Equations

Proofs.EnetTiePoCG.enetTailCotDc N h w t hd hp dc dy = Proofs.BackLinks.bnBackB N mid h w t.dε hd t.dγ t.dβ dc (Proofs.EnetTiePoCG.enetTailCotDn N h w t hp dc dy)

Instances For

theorem Proofs.EnetTiePoCG.enetTail_hasGradAt {N h w mid oc r : ℕ} (t : EnTail mid oc r) (hd : 0 < t.dε) (hp : 0 < t.pε) (dc : Vec (N * (mid * h * w))) {Gb : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGb : HasGradAt Gb (enetTailB N h w t dc) dy) :

HasGradAt (enetTailGPc N h w Gb t) (enetTailPc N h w t dc) (enetTailCotPbn N h w t hp dc dy) ∧ HasGradAt (enetTailGSe N h w Gb t) (enetTailSe N h w t dc) (enetTailCotSeOut N h w t hp dc dy) ∧ HasGradAt (enetTailGDn N h w Gb t) (enetTailDn N h w t dc) (enetTailCotDn N h w t hp dc dy) ∧ HasGradAt (enetTailGDc N h w Gb t) dc (enetTailCotDc N h w t hd hp dc dy)

The tail's cotangents are loss gradients, each stage one HasGradAt.comp through its certified VJP.

noncomputable def Proofs.EnetTiePoCG.enetExpEc (N h w : ℕ) {ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (xin : Vec (N * (ic * h * w))) :

Vec (N * (mid * h * w))

The expand conv's output.

Equations

Proofs.EnetTiePoCG.enetExpEc N h w p xin = Proofs.StableHLO.batchMap N (Proofs.flatConv p.eW p.eb) xin

Instances For

noncomputable def Proofs.EnetTiePoCG.enetExpEr (N h w : ℕ) {ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (xin : Vec (N * (ic * h * w))) :

Vec (N * (mid * h * w))

The expand swish's output (the depthwise input).

Equations

Proofs.EnetTiePoCG.enetExpEr N h w p xin = Proofs.swish (N * (mid * h * w)) (Proofs.StableHLO.bnBatchLA N mid h w p.eε p.eγ p.eβ (Proofs.EnetTiePoCG.enetExpEc N h w p xin))

Instances For

noncomputable def Proofs.EnetTiePoCG.enetExpDc (N h w : ℕ) {ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (xin : Vec (N * (ic * h * w))) :

Vec (N * (mid * h * w))

The depthwise conv's output.

Equations

Proofs.EnetTiePoCG.enetExpDc N h w p xin = Proofs.StableHLO.batchMap N (Proofs.depthwiseFlat p.dW p.db) (Proofs.EnetTiePoCG.enetExpEr N h w p xin)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetExpGEn (N h w : ℕ) {ic mid oc r kh kw : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (p : MBW ic mid oc r kh kw) :

Vec (N * (mid * h * w)) → Vec 1

The loss at the expand BN's output.

Equations

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

Instances For

noncomputable def Proofs.EnetTiePoCG.enetExpGEc (N h w : ℕ) {ic mid oc r kh kw : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (p : MBW ic mid oc r kh kw) :

Vec (N * (mid * h * w)) → Vec 1

The loss at the expand conv's output.

Equations

Proofs.EnetTiePoCG.enetExpGEc N h w Gb p z = Proofs.EnetTiePoCG.enetExpGEn N h w Gb p (Proofs.StableHLO.bnBatchLA N mid h w p.eε p.eγ p.eβ z)

Instances For

theorem Proofs.EnetTiePoCG.enetExp_hasGradAt {N h w ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * h * w))) {Gb : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGb : HasGradAt Gb (mbExpW N h w p xin) dy) :

have cotDc := enetTailCotDc N h w p.toEnTail ⋯ ⋯ (enetExpDc N h w p xin) dy; have cotEn := BackLinks.swBackB (N * (mid * h * w)) (StableHLO.bnBatchLA N mid h w p.eε p.eγ p.eβ (enetExpEc N h w p xin)) (BackLinks.dInB N p.dW p.db cotDc); HasGradAt (enetExpGEn N h w Gb p) (StableHLO.bnBatchLA N mid h w p.eε p.eγ p.eβ (enetExpEc N h w p xin)) cotEn ∧ HasGradAt (enetExpGEc N h w Gb p) (enetExpEc N h w p xin) (BackLinks.bnBackB N mid h w p.eε ⋯ p.eγ p.eβ (enetExpEc N h w p xin) cotEn)

def Proofs.EnetTiePoCG.enetExpLossTiedG {N h w ic mid oc r kh kw : ℕ} (xN vN epsStr cotN : String) (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * h * w))) (Φ : MBW ic mid oc r kh kw → Vec 1) (dyOut : Vec (N * (oc * h * w))) :

Stride-1 expand body, every parameter node a loss derivative — the thirteen nodes enetExpTiedG ties (its BN pairs split into γ and β), at the tie's forward activations and cotangents, Φ the loss at the body 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.EnetTiePoCG.enet_exp_lossTiedG {N h w ic mid oc r kh kw : ℕ} (xN vN epsStr cotN : String) (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * h * w))) {Gb : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGb : HasGradAt Gb (mbExpW N h w p xin) dy) {Φ : MBW ic mid oc r kh kw → Vec 1} (hΦ : ∀ (p' : MBW ic mid oc r kh kw), Φ p' = Gb (mbExpW N h w p' xin)) :

enetExpLossTiedG xN vN epsStr cotN p hq xin Φ dy

The stride-1 expand bundle, from the loss Gb at the body output. A widening block (b9, b16) is this at Gb := Gn.

theorem Proofs.EnetTiePoCG.enet_resid_lossTiedG {N h w mid r kh kw c : ℕ} (xN vN epsStr cotN : String) (p : MBW c mid c r kh kw) (hq : p.EpsPos) (v : Vec (N * (c * h * w))) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (mbResidW N h w p v) dy) {Φ : MBW c mid c r kh kw → Vec 1} (hΦ : ∀ (p' : MBW c mid c r kh kw), Φ p' = Gn (mbResidW N h w p' v)) :

enetExpLossTiedG xN vN epsStr cotN p hq v Φ dy

A skip block's thirteen nodes. The identity skip is a constant once a body parameter varies, so the loss at the body output has gradient dyOut there and the body bundle applies.

noncomputable def Proofs.EnetTiePoCG.enetStrEc (N h w : ℕ) {ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (mid * (2 * h) * (2 * w)))

The expand conv's output, at the input grid 2h × 2w.

Equations

Proofs.EnetTiePoCG.enetStrEc N h w p xin = Proofs.StableHLO.batchMap N (Proofs.flatConv p.eW p.eb) xin

Instances For

noncomputable def Proofs.EnetTiePoCG.enetStrEr (N h w : ℕ) {ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (mid * (2 * h) * (2 * w)))

The expand swish's output (the strided depthwise's input).

Equations

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

Instances For

noncomputable def Proofs.EnetTiePoCG.enetStrDc (N h w : ℕ) {ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (mid * h * w))

The strided depthwise conv's output.

Equations

Proofs.EnetTiePoCG.enetStrDc N h w p xin = Proofs.StableHLO.batchMap N (Proofs.depthwiseStride2Flat p.dW p.db) (Proofs.EnetTiePoCG.enetStrEr N h w p xin)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetStrGEn (N h w : ℕ) {ic mid oc r kh kw : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (p : MBW ic mid oc r kh kw) :

Vec (N * (mid * (2 * h) * (2 * w))) → Vec 1

The loss at the expand BN's output.

Equations

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

Instances For

noncomputable def Proofs.EnetTiePoCG.enetStrGEc (N h w : ℕ) {ic mid oc r kh kw : ℕ} (Gb : Vec (N * (oc * h * w)) → Vec 1) (p : MBW ic mid oc r kh kw) :

Vec (N * (mid * (2 * h) * (2 * w))) → Vec 1

The loss at the expand conv's output.

Equations

Proofs.EnetTiePoCG.enetStrGEc N h w Gb p z = Proofs.EnetTiePoCG.enetStrGEn N h w Gb p (Proofs.StableHLO.bnBatchLA N mid (2 * h) (2 * w) p.eε p.eγ p.eβ z)

Instances For

theorem Proofs.EnetTiePoCG.enetStr_hasGradAt {N h w ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) {Gb : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGb : HasGradAt Gb (mbStridedW N h w p xin) dy) :

have cotDc := enetTailCotDc N h w p.toEnTail ⋯ ⋯ (enetStrDc N h w p xin) dy; have cotEn := BackLinks.swBackB (N * (mid * (2 * h) * (2 * w))) (StableHLO.bnBatchLA N mid (2 * h) (2 * w) p.eε p.eγ p.eβ (enetStrEc N h w p xin)) (BackLinks.dStridedInB N p.dW p.db cotDc); HasGradAt (enetStrGEn N h w Gb p) (StableHLO.bnBatchLA N mid (2 * h) (2 * w) p.eε p.eγ p.eβ (enetStrEc N h w p xin)) cotEn ∧ HasGradAt (enetStrGEc N h w Gb p) (enetStrEc N h w p xin) (BackLinks.bnBackB N mid (2 * h) (2 * w) p.eε ⋯ p.eγ p.eβ (enetStrEc N h w p xin) cotEn)

def Proofs.EnetTiePoCG.enetStridedLossTiedG {N h w ic mid oc r kh kw : ℕ} (xN vN epsStr cotN : String) (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) (Φ : MBW ic mid oc r kh kw → Vec 1) (dyOut : Vec (N * (oc * h * w))) :

Stride-2 block, every parameter node a loss derivative — the thirteen nodes enetStridedTiedG ties; the depthwise nodes are the symmetric strided ones.

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.enet_strided_lossTiedG {N h w ic mid oc r kh kw : ℕ} (xN vN epsStr cotN : String) (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (mbStridedW N h w p xin) dy) {Φ : MBW ic mid oc r kh kw → Vec 1} (hΦ : ∀ (p' : MBW ic mid oc r kh kw), Φ p' = Gn (mbStridedW N h w p' xin)) :

enetStridedLossTiedG xN vN epsStr cotN p hq xin Φ dy

def Proofs.EnetTiePoCG.enetNoExpLossTiedG {N h w ic oc r kh kw : ℕ} (xN vN epsStr cotN : String) (p : MBWNoExp ic oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * h * w))) (Φ : MBWNoExp ic oc r kh kw → Vec 1) (dyOut : Vec (N * (oc * h * w))) :

No-expand block, every parameter node a loss derivative — the ten nodes enetNoExpTiedG ties.

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.enet_noexp_lossTiedG {N h w ic oc r kh kw : ℕ} (xN vN epsStr cotN : String) (p : MBWNoExp ic oc r kh kw) (hq : p.EpsPos) (xin : Vec (N * (ic * h * w))) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (mbNoExpW N h w p xin) dy) {Φ : MBWNoExp ic oc r kh kw → Vec 1} (hΦ : ∀ (p' : MBWNoExp ic oc r kh kw), Φ p' = Gn (mbNoExpW N h w p' xin)) :

enetNoExpLossTiedG xN vN epsStr cotN p hq xin Φ dy

def Proofs.EnetTiePoCG.enetStemLossTiedG {N h w ic oc kHs kWs : ℕ} (xN vN epsStr cotN : String) (εs : ℝ) (hεs : 0 < εs) (Ws : Kernel4 oc ic kHs kWs) (bs γs βs : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (Φ : Kernel4 oc ic kHs kWs → Vec oc → Vec oc → Vec oc → Vec 1) (dyStem : Vec (N * (oc * h * w))) :

Stem, every parameter node a loss derivative — the four nodes enetStemTiedG ties, Φ the loss as a function of the stem's (W, b, γ, β).

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.enet_stem_lossTiedG {N h w ic oc kHs kWs : ℕ} (xN vN epsStr cotN : String) (εs : ℝ) (hεs : 0 < εs) (Ws : Kernel4 oc ic kHs kWs) (bs γs βs : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (stemB N Ws bs εs γs βs x) dy) {Φ : Kernel4 oc ic kHs kWs → Vec oc → Vec oc → Vec oc → Vec 1} (hΦ : ∀ (W : Kernel4 oc ic kHs kWs) (b γ β : Vec oc), Φ W b γ β = Gn (stemB N W b εs γ β x)) :

enetStemLossTiedG xN vN epsStr cotN εs hεs Ws bs γs βs x Φ dy

def Proofs.EnetTiePoCG.enetHeadLossTiedG {N h w c oc nC : ℕ} (xN vN epsStr cotN dN : String) (εh : ℝ) (hεh : 0 < εh) (Wh : Kernel4 oc c 1 1) (bh γh βh : Vec oc) (Wfc : Mat oc nC) (bfc : Vec nC) (xhead : Vec (N * (c * h * w))) (Φ : Kernel4 oc c 1 1 → Vec oc → Vec oc → Vec oc → Mat oc nC → Vec nC → Vec 1) (g : Vec (N * nC)) :

Head, every parameter node a loss derivative — the six nodes enetHeadTiedG ties, at the loss cotangent g, Φ the loss as a function of (hW, hb, hγ, hβ, Wfc, bfc).

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.enet_head_lossTiedG {N h w c oc nC : ℕ} (xN vN epsStr cotN dN : String) (εh : ℝ) (hεh : 0 < εh) (Wh : Kernel4 oc c 1 1) (bh γh βh : Vec oc) (Wfc : Mat oc nC) (bfc : Vec nC) (xhead : Vec (N * (c * h * w))) {L : Vec (N * nC) → Vec 1} {g : Vec (N * nC)} (hL : HasGradAt L (headFwdB N Wh bh εh γh βh Wfc bfc xhead) g) {Φ : Kernel4 oc c 1 1 → Vec oc → Vec oc → Vec oc → Mat oc nC → Vec nC → Vec 1} (hΦ : ∀ (W : Kernel4 oc c 1 1) (b γ β : Vec oc) (Wd : Mat oc nC) (bd : Vec nC), Φ W b γ β Wd bd = L (headFwdB N W b εh γ β Wd bd xhead)) :

enetHeadLossTiedG xN vN epsStr cotN dN εh hεh Wh bh γh βh Wfc bfc xhead Φ g

theorem Proofs.EnetTiePoCG.enetNoExpW_hasGradAt_comp {N h w ic oc r kh kw : ℕ} (p : MBWNoExp ic oc r kh kw) (hq : p.EpsPos) (v : Vec (N * (ic * h * w))) {G : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hG : HasGradAt G (mbNoExpW N h w p v) dy) :

HasGradAt (fun (y : Vec (N * (ic * h * w))) => G (mbNoExpW N h w p y)) v ((mbNoExpWHasVJP N h w p ⋯ ⋯).backward v dy)

Pull the loss gradient back through the t = 1 block's certified VJP.

theorem Proofs.EnetTiePoCG.enetStridedW_hasGradAt_comp {N h w ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (v : Vec (N * (ic * (2 * h) * (2 * w)))) {G : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hG : HasGradAt G (mbStridedW N h w p v) dy) :

HasGradAt (fun (y : Vec (N * (ic * (2 * h) * (2 * w)))) => G (mbStridedW N h w p y)) v ((mbStridedWHasVJP N h w p ⋯ ⋯ ⋯).backward v dy)

…through a stride-2 block.

theorem Proofs.EnetTiePoCG.enetResidW_hasGradAt_comp {N h w c mid r kh kw : ℕ} (p : MBW c mid c r kh kw) (hq : p.EpsPos) (v : Vec (N * (c * h * w))) {G : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hG : HasGradAt G (mbResidW N h w p v) dy) :

HasGradAt (fun (y : Vec (N * (c * h * w))) => G (mbResidW N h w p y)) v ((mbResidWHasVJP N h w p ⋯ ⋯ ⋯).backward v dy)

…through a skip block.

theorem Proofs.EnetTiePoCG.enetExpW_hasGradAt_comp {N h w ic mid oc r kh kw : ℕ} (p : MBW ic mid oc r kh kw) (hq : p.EpsPos) (v : Vec (N * (ic * h * w))) {G : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hG : HasGradAt G (mbExpW N h w p v) dy) :

HasGradAt (fun (y : Vec (N * (ic * h * w))) => G (mbExpW N h w p y)) v ((mbExpWHasVJP N h w p ⋯ ⋯ ⋯).backward v dy)

…and through a widening block.

noncomputable def Proofs.EnetTiePoCG.enetPreB0 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (3 * 224 * 224)) → Vec (N * (32 * 112 * 112))

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

Equations

Proofs.EnetTiePoCG.enetPreB0 N w = Proofs.stemB N w.sW w.sb w.sε w.sγ w.sβ

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB1 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (3 * 224 * 224)) → Vec (N * (16 * 112 * 112))

Block b1's output (the tie's a1).

Equations

Proofs.EnetTiePoCG.enetPreB1 N w = Proofs.mbNoExpW N 112 112 w.b1 ∘ Proofs.EnetTiePoCG.enetPreB0 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB2 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b2's output (the tie's a2).

Equations

Proofs.EnetTiePoCG.enetPreB2 N w = Proofs.mbStridedW N 56 56 w.b2 ∘ Proofs.EnetTiePoCG.enetPreB1 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB3 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b3's output (the tie's a3).

Equations

Proofs.EnetTiePoCG.enetPreB3 N w = Proofs.mbResidW N 56 56 w.b3 ∘ Proofs.EnetTiePoCG.enetPreB2 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB4 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b4's output (the tie's a4).

Equations

Proofs.EnetTiePoCG.enetPreB4 N w = Proofs.mbStridedW N 28 28 w.b4 ∘ Proofs.EnetTiePoCG.enetPreB3 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB5 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b5's output (the tie's a5).

Equations

Proofs.EnetTiePoCG.enetPreB5 N w = Proofs.mbResidW N 28 28 w.b5 ∘ Proofs.EnetTiePoCG.enetPreB4 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB6 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b6's output (the tie's a6).

Equations

Proofs.EnetTiePoCG.enetPreB6 N w = Proofs.mbStridedW N 14 14 w.b6 ∘ Proofs.EnetTiePoCG.enetPreB5 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB7 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b7's output (the tie's a7).

Equations

Proofs.EnetTiePoCG.enetPreB7 N w = Proofs.mbResidW N 14 14 w.b7 ∘ Proofs.EnetTiePoCG.enetPreB6 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB8 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b8's output (the tie's a8).

Equations

Proofs.EnetTiePoCG.enetPreB8 N w = Proofs.mbResidW N 14 14 w.b8 ∘ Proofs.EnetTiePoCG.enetPreB7 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB9 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b9's output (the tie's a9).

Equations

Proofs.EnetTiePoCG.enetPreB9 N w = Proofs.mbExpW N 14 14 w.b9 ∘ Proofs.EnetTiePoCG.enetPreB8 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB10 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b10's output (the tie's a10).

Equations

Proofs.EnetTiePoCG.enetPreB10 N w = Proofs.mbResidW N 14 14 w.b10 ∘ Proofs.EnetTiePoCG.enetPreB9 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB11 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b11's output (the tie's a11).

Equations

Proofs.EnetTiePoCG.enetPreB11 N w = Proofs.mbResidW N 14 14 w.b11 ∘ Proofs.EnetTiePoCG.enetPreB10 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB12 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b12's output (the tie's a12).

Equations

Proofs.EnetTiePoCG.enetPreB12 N w = Proofs.mbStridedW N 7 7 w.b12 ∘ Proofs.EnetTiePoCG.enetPreB11 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB13 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b13's output (the tie's a13).

Equations

Proofs.EnetTiePoCG.enetPreB13 N w = Proofs.mbResidW N 7 7 w.b13 ∘ Proofs.EnetTiePoCG.enetPreB12 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB14 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b14's output (the tie's a14).

Equations

Proofs.EnetTiePoCG.enetPreB14 N w = Proofs.mbResidW N 7 7 w.b14 ∘ Proofs.EnetTiePoCG.enetPreB13 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB15 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b15's output (the tie's a15).

Equations

Proofs.EnetTiePoCG.enetPreB15 N w = Proofs.mbResidW N 7 7 w.b15 ∘ Proofs.EnetTiePoCG.enetPreB14 N w

Instances For

noncomputable def Proofs.EnetTiePoCG.enetPreB16 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

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

Block b16's output (the tie's a16).

Equations

Proofs.EnetTiePoCG.enetPreB16 N w = Proofs.mbExpW N 7 7 w.b16 ∘ Proofs.EnetTiePoCG.enetPreB15 N w

Instances For

theorem Proofs.EnetTiePoCG.enetPreB0_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB0 N w x = stemB N w.sW w.sb w.sε w.sγ w.sβ x

theorem Proofs.EnetTiePoCG.enetPreB1_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB1 N w x = mbNoExpW N 112 112 w.b1 (enetPreB0 N w x)

theorem Proofs.EnetTiePoCG.enetPreB2_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB2 N w x = mbStridedW N 56 56 w.b2 (enetPreB1 N w x)

theorem Proofs.EnetTiePoCG.enetPreB3_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB3 N w x = mbResidW N 56 56 w.b3 (enetPreB2 N w x)

theorem Proofs.EnetTiePoCG.enetPreB4_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB4 N w x = mbStridedW N 28 28 w.b4 (enetPreB3 N w x)

theorem Proofs.EnetTiePoCG.enetPreB5_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB5 N w x = mbResidW N 28 28 w.b5 (enetPreB4 N w x)

theorem Proofs.EnetTiePoCG.enetPreB6_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB6 N w x = mbStridedW N 14 14 w.b6 (enetPreB5 N w x)

theorem Proofs.EnetTiePoCG.enetPreB7_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB7 N w x = mbResidW N 14 14 w.b7 (enetPreB6 N w x)

theorem Proofs.EnetTiePoCG.enetPreB8_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB8 N w x = mbResidW N 14 14 w.b8 (enetPreB7 N w x)

theorem Proofs.EnetTiePoCG.enetPreB9_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB9 N w x = mbExpW N 14 14 w.b9 (enetPreB8 N w x)

theorem Proofs.EnetTiePoCG.enetPreB10_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB10 N w x = mbResidW N 14 14 w.b10 (enetPreB9 N w x)

theorem Proofs.EnetTiePoCG.enetPreB11_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB11 N w x = mbResidW N 14 14 w.b11 (enetPreB10 N w x)

theorem Proofs.EnetTiePoCG.enetPreB12_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB12 N w x = mbStridedW N 7 7 w.b12 (enetPreB11 N w x)

theorem Proofs.EnetTiePoCG.enetPreB13_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB13 N w x = mbResidW N 7 7 w.b13 (enetPreB12 N w x)

theorem Proofs.EnetTiePoCG.enetPreB14_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB14 N w x = mbResidW N 7 7 w.b14 (enetPreB13 N w x)

theorem Proofs.EnetTiePoCG.enetPreB15_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB15 N w x = mbResidW N 7 7 w.b15 (enetPreB14 N w x)

theorem Proofs.EnetTiePoCG.enetPreB16_apply (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

enetPreB16 N w x = mbExpW N 7 7 w.b16 (enetPreB15 N w x)

noncomputable def Proofs.EnetTiePoCG.enetSufB16 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (320 * 7 * 7)) → Vec (N * nCls)

The net after block b16 — the head.

Equations

Proofs.EnetTiePoCG.enetSufB16 N w = Proofs.headFwdB N w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB15 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (192 * 7 * 7)) → Vec (N * nCls)

The net after block b15: block b16, then the rest.

Equations

Proofs.EnetTiePoCG.enetSufB15 N w y = Proofs.EnetTiePoCG.enetSufB16 N w (Proofs.mbExpW N 7 7 w.b16 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB14 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (192 * 7 * 7)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB14 N w y = Proofs.EnetTiePoCG.enetSufB15 N w (Proofs.mbResidW N 7 7 w.b15 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB13 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (192 * 7 * 7)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB13 N w y = Proofs.EnetTiePoCG.enetSufB14 N w (Proofs.mbResidW N 7 7 w.b14 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB12 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (192 * 7 * 7)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB12 N w y = Proofs.EnetTiePoCG.enetSufB13 N w (Proofs.mbResidW N 7 7 w.b13 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB11 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (112 * 14 * 14)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB11 N w y = Proofs.EnetTiePoCG.enetSufB12 N w (Proofs.mbStridedW N 7 7 w.b12 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB10 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (112 * 14 * 14)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB10 N w y = Proofs.EnetTiePoCG.enetSufB11 N w (Proofs.mbResidW N 14 14 w.b11 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB9 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (112 * 14 * 14)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB9 N w y = Proofs.EnetTiePoCG.enetSufB10 N w (Proofs.mbResidW N 14 14 w.b10 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB8 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (80 * 14 * 14)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB8 N w y = Proofs.EnetTiePoCG.enetSufB9 N w (Proofs.mbExpW N 14 14 w.b9 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB7 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (80 * 14 * 14)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB7 N w y = Proofs.EnetTiePoCG.enetSufB8 N w (Proofs.mbResidW N 14 14 w.b8 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB6 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (80 * 14 * 14)) → Vec (N * nCls)

The net after block b6: block b7, then the rest.

Equations

Proofs.EnetTiePoCG.enetSufB6 N w y = Proofs.EnetTiePoCG.enetSufB7 N w (Proofs.mbResidW N 14 14 w.b7 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB5 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (40 * 28 * 28)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB5 N w y = Proofs.EnetTiePoCG.enetSufB6 N w (Proofs.mbStridedW N 14 14 w.b6 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB4 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (40 * 28 * 28)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB4 N w y = Proofs.EnetTiePoCG.enetSufB5 N w (Proofs.mbResidW N 28 28 w.b5 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB3 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (24 * 56 * 56)) → Vec (N * nCls)

The net after block b3: block b4, then the rest.

Equations

Proofs.EnetTiePoCG.enetSufB3 N w y = Proofs.EnetTiePoCG.enetSufB4 N w (Proofs.mbStridedW N 28 28 w.b4 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB2 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (24 * 56 * 56)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB2 N w y = Proofs.EnetTiePoCG.enetSufB3 N w (Proofs.mbResidW N 56 56 w.b3 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufB1 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (16 * 112 * 112)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufB1 N w y = Proofs.EnetTiePoCG.enetSufB2 N w (Proofs.mbStridedW N 56 56 w.b2 y)

Instances For

noncomputable def Proofs.EnetTiePoCG.enetSufStem (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) :

Vec (N * (32 * 112 * 112)) → Vec (N * nCls)

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

Equations

Proofs.EnetTiePoCG.enetSufStem N w y = Proofs.EnetTiePoCG.enetSufB1 N w (Proofs.mbNoExpW N 112 112 w.b1 y)

Instances For

theorem Proofs.EnetTiePoCG.enet_factor_stem (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (W : Kernel4 32 3 3 3) (b γ β : Vec 32) :

efficientnetForwardBFull N { sW := W, sb := b, sε := w.sε, sγ := γ, sβ := β, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufStem N w (stemB N W b w.sε γ β x)

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

theorem Proofs.EnetTiePoCG.enet_factor_b1 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBWNoExp 32 16 8 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := p, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB1 N w (mbNoExpW N 112 112 p (enetPreB0 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b2 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 16 96 24 4 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := p, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB2 N w (mbStridedW N 56 56 p (enetPreB1 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b3 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 24 144 24 6 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := p, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB3 N w (mbResidW N 56 56 p (enetPreB2 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b4 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 24 144 40 6 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := p, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB4 N w (mbStridedW N 28 28 p (enetPreB3 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b5 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 40 240 40 10 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := p, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB5 N w (mbResidW N 28 28 p (enetPreB4 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b6 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 40 240 80 10 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB6 N w (mbStridedW N 14 14 p (enetPreB5 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b7 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 80 480 80 20 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB7 N w (mbResidW N 14 14 p (enetPreB6 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b8 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 80 480 80 20 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB8 N w (mbResidW N 14 14 p (enetPreB7 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b9 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 80 480 112 20 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB9 N w (mbExpW N 14 14 p (enetPreB8 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b10 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 112 672 112 28 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB10 N w (mbResidW N 14 14 p (enetPreB9 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b11 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 112 672 112 28 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB11 N w (mbResidW N 14 14 p (enetPreB10 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b12 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 112 672 192 28 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB12 N w (mbStridedW N 7 7 p (enetPreB11 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b13 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 192 1152 192 48 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB13 N w (mbResidW N 7 7 p (enetPreB12 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b14 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 192 1152 192 48 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB14 N w (mbResidW N 7 7 p (enetPreB13 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b15 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 192 1152 192 48 5 5) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB15 N w (mbResidW N 7 7 p (enetPreB14 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_b16 (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (p : MBW 192 1152 320 48 3 3) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := p, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb } x = enetSufB16 N w (mbExpW N 7 7 p (enetPreB15 N w x))

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

theorem Proofs.EnetTiePoCG.enet_factor_head (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) (W : Kernel4 1280 320 1 1) (b γ β : Vec 1280) (Wd : Mat 1280 nCls) (bd : Vec nCls) :

efficientnetForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, 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, b16 := w.b16, hW := W, hb := b, hε := w.hε, hγ := γ, hβ := β, fcW := Wd, fcb := bd } x = headFwdB N W b w.hε γ β Wd bd (enetPreB16 N w x)

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

theorem Proofs.EnetTiePoCG.enet_forward_eq_head (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (x : Vec (N * (3 * 224 * 224))) :

efficientnetForwardBFull N w x = headFwdB N w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb (enetPreB16 N w x)

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

def Proofs.EnetTiePoCG.EnetNetLossTiedG (xN vN epsStr cotN dN : String) (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (hεw : w.EpsPos) (x : Vec (N * (3 * 224 * 224))) (L : Vec (N * nCls) → Vec 1) (g : Vec (N * nCls)) :

Every EfficientNet-B0 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 262 nodes efficientnet_net_tiedG ties, each at the cotangent the certified block VJPs thread to it from g, stated against L of efficientnetForwardBFull with that one parameter varied.

Equations

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

Instances For

theorem Proofs.EnetTiePoCG.enet_net_lossGrad (xN vN epsStr cotN dN : String) (N : ℕ) {nCls : ℕ} (w : B0Weights nCls) (hεw : w.EpsPos) (x : Vec (N * (3 * 224 * 224))) {L : Vec (N * nCls) → Vec 1} {g : Vec (N * nCls)} (hL : HasGradAt L (efficientnetForwardBFull N w x) g) :

EnetNetLossTiedG xN vN epsStr cotN dN N w hεw x L g

Every EfficientNet-B0 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 262 nodes efficientnet_net_tiedG ties — at the same cotangent — is ∂L/∂θ of the WHOLE net, efficientnetForwardBFull with that one parameter varied (a stem field, a block's weight record w.bk := p with one slot changed, or a head field).

Hypothesis: every BN ε positive (B0Weights.EpsPos), as in the tie. The loss enters only through hL; enet_net_lossGrad_smoothedCE discharges it for the loss the artifacts ship.

theorem Proofs.EnetTiePoCG.enet_net_lossGrad_smoothedCE (xN vN epsStr cotN dN aStr negAK bStr logN ohN : String) (N : ℕ) {nCls : ℕ} (hK : 0 < nCls) (α B : ℝ) (w : B0Weights nCls) (hεw : w.EpsPos) (x : Vec (N * (3 * 224 * 224))) (t : Vec (N * (1 * nCls))) (ht : ∀ (n : Fin N), ∑ k : Fin nCls, targetRow N nCls t n k = 1) :

EnetNetLossTiedG xN vN epsStr cotN dN N w hεw x (smoothedBatchLoss N nCls α B t) (BackLinks.unrowB N nCls (StableHLO.den (smoothedLossCotGraph N nCls α B aStr negAK bStr logN ohN (BackLinks.rowB N nCls (efficientnetForwardBFull N w x)) t)))

The loss the artifacts ship: every node is the derivative of the batched label-smoothed cross-entropy smoothedBatchLoss, g the six-op cotangent the render emits — the tie's own g, whose logits headFwdB … a16 are efficientnetForwardBFull N w x.