MobileNetV2 — every parameter gradient node IS the loss's derivative in that parameter #
mnv2_net_tiedB says each of the 210 parameter gradient nodes (158 emitted at the default
convBias := false) denotes its layer's parameter Jacobian contracted with the cotangent the
emitted backward chain threads to it, from a loss cotangent g; the *_eq_vjp lemmas say the
chain's segments are certified VJP backwards. mnv2_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 with
that one parameter varied. mnv2_net_lossGrad_smoothedCE discharges hL for the label-smoothed
loss the artifacts ship.
Scope. One replica, at either precision: every conv and depthwise weight node is stated on
the renderers' switch (convWeightGradBAt bf16 id …, depthwiseWeightGradBAt bf16 id …, …;
Foundation.GradNodesBAt), so bf16 := true is the bf16 kind the mobilenetv2*bf16 artifacts
emit — mobilenetv2in_rmsdp64wxdols0eps0001bf16, the book's ImageNet run, among them — read over ℝ
at the identity rounding (Bf16Erasure), and bf16 := false the f32 artifacts'. Classifier
dropout is an optional site on the statement, as in MobileNetV2StepTieB: cd : Option (Vec (N * 1280)), none the drop-free artifacts and some m the *do* ones, the loss read at
mobilenetv2ForwardBFullDoOpt (the net with the site), the dense weight node reading the dropped
activation and the chain above the site pulled back through the mask (dropoutOptHasVJP).
Sync-BN data parallelism is reached by composition: mnv2_net_syncTiedB says each all-reduced
gradient is this net's tied node at N := R·N, which this file's capstone makes the loss's
gradient at the global batch.
How. ResNet50ParamGrad's shape:
- Per stage (at variable widths): the loss read at the output of the stem, the
t = 1block, the stride-1 body, the stride-2 body and the head, pulled back one stage at a time byParamGradNodes' pull-backs (relu6'shasGradAt_relu6, batch BN, the conv and depthwise input-VJPs, the XLA-SAMEstrided depthwise'shasGradAt_depthwiseStridedXlaamong them), so each internal activation's gradient is the chain's own cotangent. The stride-1 body bundle covers both the skip blocks and the two widenings: a skip block's body sees the lossu ↦ Gn (u + v), whose gradient at the body output is stilldyOut(mnv2_resid_lossTiedB). - Per net: the loss read after each block (
mnv2Suf*), pulled back through the seventeen certified block VJPs and the head's, and eachΦidentified with the whole net at updated weights by a standalonemnv2_factor_*theorem.
Hypotheses. MNV2PosB (every BN ε > 0), MNV2SmoothAtB (all 35 relu6 sites off both kinks
at the real activations); for the smoothed loss every example's target summing to one and
0 < nCls.
def
Proofs.MobileNetV2TieB.mnv2StemLossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(Ws : Kernel4 oc ic 3 3)
(bs : Vec oc)
(εs : ℝ)
(γs βs : Vec oc)
(bf16 : Bool)
(x : Vec (N * (ic * (2 * h) * (2 * w))))
(Φ : Kernel4 oc ic 3 3 → Vec oc → Vec oc → Vec oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
Stem, every parameter node a loss derivative — the four nodes mnv2StemTiedB 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.MobileNetV2TieB.mnv2_stem_lossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(Ws : Kernel4 oc ic 3 3)
(bs : Vec oc)
(εs : ℝ)
(hεs : 0 < εs)
(γs βs : Vec oc)
(bf16 : Bool)
(x : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : MNV2StemSmoothAtB N h w Ws bs εs γs βs x)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StemB N h w Ws bs εs γs βs x) dy)
{Φ : Kernel4 oc ic 3 3 → Vec oc → Vec oc → Vec oc → Vec 1}
(hΦ : ∀ (W : Kernel4 oc ic 3 3) (b γ β : Vec oc), Φ W b γ β = Gn (mnv2StemB N h w W b εs γ β x))
:
mnv2StemLossTiedB xN cotN vN epsStr Ws bs εs γs βs bf16 x Φ dy
def
Proofs.MobileNetV2TieB.mnv2NoExpLossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVWNoExp ic oc)
(bf16 : Bool)
(v : Vec (N * (ic * h * w)))
(Φ : IVWNoExp ic oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
t = 1 block, every parameter node a loss derivative — the eight nodes mnv2NoExpTiedB
ties. The project BN's γ/β read dyOut itself: nothing follows the linear bottleneck.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_noexp_lossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVWNoExp ic oc)
(bf16 : Bool)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVNoExpSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2NoExpB N h w p v) dy)
{Φ : IVWNoExp ic oc → Vec 1}
(hΦ : ∀ (p' : IVWNoExp ic oc), Φ p' = Gn (mnv2NoExpB N h w p' v))
:
mnv2NoExpLossTiedB xN cotN vN epsStr p bf16 v Φ dy
def
Proofs.MobileNetV2TieB.mnv2Stride1LossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(bf16 : Bool)
(v : Vec (N * (ic * h * w)))
(Φ : IVW ic mid oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
Stride-1 body, every parameter node a loss derivative — the twelve nodes
mnv2Stride1TiedB ties, Φ the loss at the body output as a function of the weight record.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_stride1_lossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(bf16 : Bool)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
{Φ : IVW ic mid oc → Vec 1}
(hΦ : ∀ (p' : IVW ic mid oc), Φ p' = Gb (mnv2ExpOnlyB N h w p' v))
:
mnv2Stride1LossTiedB xN cotN vN epsStr p bf16 v Φ dy
The stride-1 body bundle, from the loss Gb at the body output. A widening block (b11,
b17) is this at Gb := Gn.
theorem
Proofs.MobileNetV2TieB.mnv2_resid_lossTiedB
{N h w mid c : ℕ}
(xN cotN vN epsStr : String)
(p : IVW c mid c)
(bf16 : Bool)
(hq : IVPos p)
(v : Vec (N * (c * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gn : Vec (N * (c * h * w)) → Vec 1}
{dy : Vec (N * (c * h * w))}
(hGn : HasGradAt Gn (mnv2ResidB N h w p v) dy)
{Φ : IVW c mid c → Vec 1}
(hΦ : ∀ (p' : IVW c mid c), Φ p' = Gn (mnv2ResidB N h w p' v))
:
mnv2Stride1LossTiedB xN cotN vN epsStr p bf16 v Φ dy
A skip block's twelve 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.
def
Proofs.MobileNetV2TieB.mnv2Stride2LossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(bf16 : Bool)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(Φ : IVW ic mid oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
Stride-2 block, every parameter node a loss derivative — the twelve nodes
mnv2Stride2TiedB ties; the depthwise nodes are the XLA-SAME strided ones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_stride2_lossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(bf16 : Bool)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
{Φ : IVW ic mid oc → Vec 1}
(hΦ : ∀ (p' : IVW ic mid oc), Φ p' = Gn (mnv2StridedB N h w p' v))
:
mnv2Stride2LossTiedB xN cotN vN epsStr p bf16 v Φ dy
def
Proofs.MobileNetV2TieB.mnv2HeadLossTiedB
{N h w ic oc nCls : ℕ}
(xN cotN vN epsStr : String)
(Wh : Kernel4 oc ic 1 1)
(bh : Vec oc)
(εh : ℝ)
(γh βh : Vec oc)
(Wd : Mat oc nCls)
(bd : Vec nCls)
(bf16 : Bool)
(cd : Option (Vec (N * oc)))
(v : Vec (N * (ic * h * w)))
(Φ : Kernel4 oc ic 1 1 → Vec oc → Vec oc → Vec oc → Mat oc nCls → Vec nCls → Vec 1)
(g : Vec (N * nCls))
:
Head, every parameter node a loss derivative — the six nodes mnv2HeadTiedB ties, Φ
the loss as a function of (hW, hb, hγ, hβ, Wd, bd).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_head_lossTiedB
{N h w ic oc nCls : ℕ}
(xN cotN vN epsStr : String)
(Wh : Kernel4 oc ic 1 1)
(bh : Vec oc)
(εh : ℝ)
(hεh : 0 < εh)
(γh βh : Vec oc)
(Wd : Mat oc nCls)
(bd : Vec nCls)
(bf16 : Bool)
(cd : Option (Vec (N * oc)))
(v : Vec (N * (ic * h * w)))
(hs : MNV2HeadSmoothAtB N h w Wh bh εh γh βh v)
{L : Vec (N * nCls) → Vec 1}
{g : Vec (N * nCls)}
(hL : HasGradAt L (mnv2HeadBDoOpt N h w Wh bh εh γh βh Wd bd cd v) g)
{Φ : Kernel4 oc ic 1 1 → Vec oc → Vec oc → Vec oc → Mat oc nCls → Vec nCls → Vec 1}
(hΦ :
∀ (W : Kernel4 oc ic 1 1) (b γ β : Vec oc) (Wd' : Mat oc nCls) (bd' : Vec nCls),
Φ W b γ β Wd' bd' = L (mnv2HeadBDoOpt N h w W b εh γ β Wd' bd' cd v))
:
mnv2HeadLossTiedB xN cotN vN epsStr Wh bh εh γh βh Wd bd bf16 cd v Φ g
theorem
Proofs.MobileNetV2TieB.mnv2NoExpB_hasGradAt_comp
{N h w ic oc : ℕ}
(p : IVWNoExp ic oc)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVNoExpSmoothAtB N h w p v)
{G : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hG : HasGradAt G (mnv2NoExpB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (ic * h * w))) => G (mnv2NoExpB N h w p y)) v (mnv2NoExpCotIn N h w p v dy)
Pull the loss gradient back through the t = 1 block (mnv2NoExpCotIn_eq_vjp).
theorem
Proofs.MobileNetV2TieB.mnv2ExpOnlyB_hasGradAt_comp
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{G : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hG : HasGradAt G (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (ic * h * w))) => G (mnv2ExpOnlyB N h w p y)) v (mnv2CotInBody N h w p v dy)
…through a widening block (mnv2ExpOnlyCotIn_eq_vjp).
theorem
Proofs.MobileNetV2TieB.mnv2ResidB_hasGradAt_comp
{N h w c mid : ℕ}
(p : IVW c mid c)
(hq : IVPos p)
(v : Vec (N * (c * h * w)))
(hs : IVSmoothAtB N h w p v)
{G : Vec (N * (c * h * w)) → Vec 1}
{dy : Vec (N * (c * h * w))}
(hG : HasGradAt G (mnv2ResidB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (c * h * w))) => G (mnv2ResidB N h w p y)) v (mnv2ResidCotIn N h w p v dy)
…through a skip block (mnv2ResidCotIn_eq_vjp).
theorem
Proofs.MobileNetV2TieB.mnv2StridedB_hasGradAt_comp
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{G : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hG : HasGradAt G (mnv2StridedB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (ic * (2 * h) * (2 * w)))) => G (mnv2StridedB N h w p y)) v (mnv2StridedCotIn N h w p v dy)
…and through a stride-2 block (mnv2StridedCotIn_eq_vjp).
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB17
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b17 — the head.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB17 N w cd = Proofs.MobileNetV2TieB.mnv2HeadBDoOpt N 7 7 w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb cd
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB16
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b16: block b17, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB16 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB17 N w cd (Proofs.mnv2ExpOnlyB N 7 7 w.b17 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB15
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b15: block b16, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB15 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB16 N w cd (Proofs.mnv2ResidB N 7 7 w.b16 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB14
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b14: block b15, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB14 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB15 N w cd (Proofs.mnv2ResidB N 7 7 w.b15 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB13
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b13: block b14, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB13 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB14 N w cd (Proofs.mnv2StridedB N 7 7 w.b14 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB12
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b12: block b13, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB12 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB13 N w cd (Proofs.mnv2ResidB N 14 14 w.b13 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB11
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b11: block b12, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB11 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB12 N w cd (Proofs.mnv2ResidB N 14 14 w.b12 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB10
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b10: block b11, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB10 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB11 N w cd (Proofs.mnv2ExpOnlyB N 14 14 w.b11 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB9
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b9: block b10, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB9 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB10 N w cd (Proofs.mnv2ResidB N 14 14 w.b10 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB8
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b8: block b9, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB8 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB9 N w cd (Proofs.mnv2ResidB N 14 14 w.b9 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB7
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b7: block b8, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB7 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB8 N w cd (Proofs.mnv2ResidB N 14 14 w.b8 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB6
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b6: block b7, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB6 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB7 N w cd (Proofs.mnv2StridedB N 14 14 w.b7 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB5
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b5: block b6, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB5 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB6 N w cd (Proofs.mnv2ResidB N 28 28 w.b6 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB4
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b4: block b5, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB4 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB5 N w cd (Proofs.mnv2ResidB N 28 28 w.b5 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB3
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b3: block b4, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB3 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB4 N w cd (Proofs.mnv2StridedB N 28 28 w.b4 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB2
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b2: block b3, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB2 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB3 N w cd (Proofs.mnv2ResidB N 56 56 w.b3 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufB1
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after block b1: block b2, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB1 N w cd y = Proofs.MobileNetV2TieB.mnv2SufB2 N w cd (Proofs.mnv2StridedB N 56 56 w.b2 y)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SufStem
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(cd : Option (Vec (N * 1280)))
:
The net after the stem: block b1, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufStem N w cd y = Proofs.MobileNetV2TieB.mnv2SufB1 N w cd (Proofs.mnv2NoExpB N 112 112 w.b1 y)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_factor_stem
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(W : Kernel4 32 3 3 3)
(b γ β : Vec 32)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufStem N w cd (mnv2StemB N 112 112 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.MobileNetV2TieB.mnv2_factor_b1
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVWNoExp 32 16)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB1 N w cd (mnv2NoExpB N 112 112 p (mnv2PreB0 N w x))
The net with block b1's weights varied is the suffix after b1 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b2
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 16 96 24)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB2 N w cd (mnv2StridedB N 56 56 p (mnv2PreB1 N w x))
The net with block b2's weights varied is the suffix after b2 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b3
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 24 144 24)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB3 N w cd (mnv2ResidB N 56 56 p (mnv2PreB2 N w x))
The net with block b3's weights varied is the suffix after b3 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b4
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 24 144 32)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB4 N w cd (mnv2StridedB N 28 28 p (mnv2PreB3 N w x))
The net with block b4's weights varied is the suffix after b4 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b5
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 32 192 32)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB5 N w cd (mnv2ResidB N 28 28 p (mnv2PreB4 N w x))
The net with block b5's weights varied is the suffix after b5 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b6
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 32 192 32)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB6 N w cd (mnv2ResidB N 28 28 p (mnv2PreB5 N w x))
The net with block b6's weights varied is the suffix after b6 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b7
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 32 192 64)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB7 N w cd (mnv2StridedB N 14 14 p (mnv2PreB6 N w x))
The net with block b7's weights varied is the suffix after b7 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b8
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 64 384 64)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB8 N w cd (mnv2ResidB N 14 14 p (mnv2PreB7 N w x))
The net with block b8's weights varied is the suffix after b8 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b9
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 64 384 64)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB9 N w cd (mnv2ResidB N 14 14 p (mnv2PreB8 N w x))
The net with block b9's weights varied is the suffix after b9 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b10
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 64 384 64)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB10 N w cd (mnv2ResidB N 14 14 p (mnv2PreB9 N w x))
The net with block b10's weights varied is the suffix after b10 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b11
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 64 384 96)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB11 N w cd (mnv2ExpOnlyB N 14 14 p (mnv2PreB10 N w x))
The net with block b11's weights varied is the suffix after b11 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b12
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 96 576 96)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB12 N w cd (mnv2ResidB N 14 14 p (mnv2PreB11 N w x))
The net with block b12's weights varied is the suffix after b12 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b13
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 96 576 96)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB13 N w cd (mnv2ResidB N 14 14 p (mnv2PreB12 N w x))
The net with block b13's weights varied is the suffix after b13 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b14
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 96 576 160)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB14 N w cd (mnv2StridedB N 7 7 p (mnv2PreB13 N w x))
The net with block b14's weights varied is the suffix after b14 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b15
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 160 960 160)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB15 N w cd (mnv2ResidB N 7 7 p (mnv2PreB14 N w x))
The net with block b15's weights varied is the suffix after b15 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b16
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 160 960 160)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB16 N w cd (mnv2ResidB N 7 7 p (mnv2PreB15 N w x))
The net with block b16's weights varied is the suffix after b16 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b17
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(p : IVW 160 960 320)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := p, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x = mnv2SufB17 N w cd (mnv2ExpOnlyB N 7 7 p (mnv2PreB16 N w x))
The net with block b17's weights varied is the suffix after b17 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_head
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(cd : Option (Vec (N * 1280)))
(W : Kernel4 1280 320 1 1)
(b γ β : Vec 1280)
(Wd : Mat 1280 nCls)
(bd : Vec nCls)
:
mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := W, hb := b, hε := w.hε, hγ := γ,
hβ := β, fcW := Wd, fcb := bd }
cd x = mnv2HeadBDoOpt N 7 7 W b w.hε γ β Wd bd cd (mnv2PreB17 N w x)
The net with the head varied is the head at the varied parameters.
def
Proofs.MobileNetV2TieB.MNV2NetLossTiedB
(N : ℕ)
{nCls : ℕ}
(xN cotN vN epsStr : String)
(w : MNV2BWeights nCls)
(bf16 : Bool)
(cd : Option (Vec (N * 1280)))
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(L : Vec (N * nCls) → Vec 1)
(g : Vec (N * nCls))
:
Every MobileNetV2 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 210 slots
mnv2_net_tiedB ties, each at the cotangent the emitted chain threads to it, stated against L
of mobilenetv2ForwardBFull with that one parameter varied.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_net_lossGrad
(N : ℕ)
{nCls : ℕ}
(xN cotN vN epsStr : String)
(w : MNV2BWeights nCls)
(hq : MNV2PosB w)
(bf16 : Bool)
(cd : Option (Vec (N * 1280)))
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(hx : MNV2SmoothAtB N w x)
{L : Vec (N * nCls) → Vec 1}
{g : Vec (N * nCls)}
(hL : HasGradAt L (mobilenetv2ForwardBFullDoOpt N w cd x) g)
:
MNV2NetLossTiedB N xN cotN vN epsStr w bf16 cd x L g
Every MobileNetV2 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
210 slots mnv2_net_tiedB ties — at the same cotangent — is ∂L/∂θ of the WHOLE net,
mobilenetv2ForwardBFull with that one parameter varied (a stem field, a block's weight record
w.bk := p with one slot changed, or a head field).
Hypotheses: every BN ε positive (MNV2PosB) and all 35 relu6 sites off both kinks at the real
activations (MNV2SmoothAtB). The loss enters only through hL;
mnv2_net_lossGrad_smoothedCE discharges it for the loss the artifacts ship.
One replica; bf16 selects the conv and depthwise weight nodes' kind (the module's Scope).
theorem
Proofs.MobileNetV2TieB.mnv2_net_lossGrad_smoothedCE
(N : ℕ)
{nCls : ℕ}
(hK : 0 < nCls)
(xN cotN vN epsStr aStr negAK bStr logN ohN : String)
(α B : ℝ)
(w : MNV2BWeights nCls)
(hq : MNV2PosB w)
(bf16 : Bool)
(cd : Option (Vec (N * 1280)))
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(hx : MNV2SmoothAtB N w x)
(t : Vec (N * (1 * nCls)))
(ht : ∀ (n : Fin N), ∑ k : Fin nCls, targetRow N nCls t n k = 1)
:
MNV2NetLossTiedB N xN cotN vN epsStr w bf16 cd 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 (mobilenetv2ForwardBFullDoOpt N w cd 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.
theorem
Proofs.MobileNetV2TieB.mnv2_net_tied_lossGrad
(N : ℕ)
{nCls : ℕ}
(xN cotN vN epsStr : String)
(w : MNV2BWeights nCls)
(bf16 : Bool)
(cd : Option (Vec (N * 1280)))
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(g : Vec (N * nCls))
(hq : MNV2PosB w)
(hx : MNV2SmoothAtB N w x)
{L : Vec (N * nCls) → Vec 1}
(hL : HasGradAt L (mobilenetv2ForwardBFullDoOpt N w cd x) g)
:
have dy17 := mnv2HeadCotBlk N 7 7 w.hW w.hb w.hε w.hγ w.hβ w.fcW cd (mnv2PreB17 N w x) g;
have dy16 := mnv2CotInBody N 7 7 w.b17 (mnv2PreB16 N w x) dy17;
have dy15 := mnv2ResidCotIn N 7 7 w.b16 (mnv2PreB15 N w x) dy16;
have dy14 := mnv2ResidCotIn N 7 7 w.b15 (mnv2PreB14 N w x) dy15;
have dy13 := mnv2StridedCotIn N 7 7 w.b14 (mnv2PreB13 N w x) dy14;
have dy12 := mnv2ResidCotIn N 14 14 w.b13 (mnv2PreB12 N w x) dy13;
have dy11 := mnv2ResidCotIn N 14 14 w.b12 (mnv2PreB11 N w x) dy12;
have dy10 := mnv2CotInBody N 14 14 w.b11 (mnv2PreB10 N w x) dy11;
have dy9 := mnv2ResidCotIn N 14 14 w.b10 (mnv2PreB9 N w x) dy10;
have dy8 := mnv2ResidCotIn N 14 14 w.b9 (mnv2PreB8 N w x) dy9;
have dy7 := mnv2ResidCotIn N 14 14 w.b8 (mnv2PreB7 N w x) dy8;
have dy6 := mnv2StridedCotIn N 14 14 w.b7 (mnv2PreB6 N w x) dy7;
have dy5 := mnv2ResidCotIn N 28 28 w.b6 (mnv2PreB5 N w x) dy6;
have dy4 := mnv2ResidCotIn N 28 28 w.b5 (mnv2PreB4 N w x) dy5;
have dy3 := mnv2StridedCotIn N 28 28 w.b4 (mnv2PreB3 N w x) dy4;
have dy2 := mnv2ResidCotIn N 56 56 w.b3 (mnv2PreB2 N w x) dy3;
have dy1 := mnv2StridedCotIn N 56 56 w.b2 (mnv2PreB1 N w x) dy2;
have cotStem := mnv2NoExpCotIn N 112 112 w.b1 (mnv2PreB0 N w x) dy1;
(mnv2StemTiedB N 112 112 xN cotN vN epsStr w.sW w.sb w.sε w.sγ w.sβ bf16 x cotStem ∧ mnv2StemLossTiedB xN cotN vN epsStr w.sW w.sb w.sε w.sγ w.sβ bf16 x
(fun (W : Kernel4 32 3 3 3) (b γ β : Vec 32) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
cotStem) ∧ (mnv2NoExpTiedB N 112 112 xN cotN vN epsStr w.b1 bf16 (mnv2PreB0 N w x) dy1 ∧ mnv2NoExpLossTiedB xN cotN vN epsStr w.b1 bf16 (mnv2PreB0 N w x)
(fun (p : IVWNoExp 32 16) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb,
hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy1) ∧ (mnv2Stride2TiedB N 56 56 xN cotN vN epsStr w.b2 bf16 (mnv2PreB1 N w x) dy2 ∧ mnv2Stride2LossTiedB xN cotN vN epsStr w.b2 bf16 (mnv2PreB1 N w x)
(fun (p : IVW 16 96 24) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW,
hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy2) ∧ (mnv2Stride1TiedB N 56 56 xN cotN vN epsStr w.b3 bf16 (mnv2PreB2 N w x) dy3 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b3 bf16 (mnv2PreB2 N w x)
(fun (p : IVW 24 144 24) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW,
hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy3) ∧ (mnv2Stride2TiedB N 28 28 xN cotN vN epsStr w.b4 bf16 (mnv2PreB3 N w x) dy4 ∧ mnv2Stride2LossTiedB xN cotN vN epsStr w.b4 bf16 (mnv2PreB3 N w x)
(fun (p : IVW 24 144 32) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW,
hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy4) ∧ (mnv2Stride1TiedB N 28 28 xN cotN vN epsStr w.b5 bf16 (mnv2PreB4 N w x) dy5 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b5 bf16 (mnv2PreB4 N w x)
(fun (p : IVW 32 192 32) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW,
hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy5) ∧ (mnv2Stride1TiedB N 28 28 xN cotN vN epsStr w.b6 bf16 (mnv2PreB5 N w x) dy6 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b6 bf16 (mnv2PreB5 N w x)
(fun (p : IVW 32 192 32) =>
L
(mobilenetv2ForwardBFullDoOpt 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,
b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW,
fcb := w.fcb }
cd x))
dy6) ∧ (mnv2Stride2TiedB N 14 14 xN cotN vN epsStr w.b7 bf16 (mnv2PreB6 N w x) dy7 ∧ mnv2Stride2LossTiedB xN cotN vN epsStr w.b7 bf16 (mnv2PreB6 N w x)
(fun (p : IVW 32 192 64) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ,
fcW := w.fcW, fcb := w.fcb }
cd x))
dy7) ∧ (mnv2Stride1TiedB N 14 14 xN cotN vN epsStr w.b8 bf16 (mnv2PreB7 N w x) dy8 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b8 bf16 (mnv2PreB7 N w x)
(fun (p : IVW 64 384 64) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ,
fcW := w.fcW, fcb := w.fcb }
cd x))
dy8) ∧ (mnv2Stride1TiedB N 14 14 xN cotN vN epsStr w.b9 bf16 (mnv2PreB8 N w x) dy9 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b9 bf16 (mnv2PreB8 N w x)
(fun (p : IVW 64 384 64) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ,
fcW := w.fcW, fcb := w.fcb }
cd x))
dy9) ∧ (mnv2Stride1TiedB N 14 14 xN cotN vN epsStr w.b10 bf16 (mnv2PreB9 N w x) dy10 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b10 bf16 (mnv2PreB9 N w x)
(fun (p : IVW 64 384 64) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy10) ∧ (mnv2Stride1TiedB N 14 14 xN cotN vN epsStr w.b11 bf16 (mnv2PreB10 N w x) dy11 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b11 bf16 (mnv2PreB10 N w x)
(fun (p : IVW 64 384 96) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy11) ∧ (mnv2Stride1TiedB N 14 14 xN cotN vN epsStr w.b12 bf16 (mnv2PreB11 N w x) dy12 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b12 bf16 (mnv2PreB11 N w x)
(fun (p : IVW 96 576 96) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb,
hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy12) ∧ (mnv2Stride1TiedB N 14 14 xN cotN vN epsStr w.b13 bf16 (mnv2PreB12 N w x) dy13 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b13 bf16 (mnv2PreB12 N w x)
(fun (p : IVW 96 576 96) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW, hb := w.hb,
hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy13) ∧ (mnv2Stride2TiedB N 7 7 xN cotN vN epsStr w.b14 bf16 (mnv2PreB13 N w x) dy14 ∧ mnv2Stride2LossTiedB xN cotN vN epsStr w.b14 bf16 (mnv2PreB13 N w x)
(fun (p : IVW 96 576 160) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17, hW := w.hW,
hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
cd x))
dy14) ∧ (mnv2Stride1TiedB N 7 7 xN cotN vN epsStr w.b15 bf16 (mnv2PreB14 N w x) dy15 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b15 bf16 (mnv2PreB14 N w x)
(fun (p : IVW 160 960 160) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17,
hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW,
fcb := w.fcb }
cd x))
dy15) ∧ (mnv2Stride1TiedB N 7 7 xN cotN vN epsStr w.b16 bf16 (mnv2PreB15 N w x) dy16 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b16 bf16 (mnv2PreB15 N w x)
(fun (p : IVW 160 960 160) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17,
hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ, fcW := w.fcW,
fcb := w.fcb }
cd x))
dy16) ∧ (mnv2Stride1TiedB N 7 7 xN cotN vN epsStr w.b17 bf16 (mnv2PreB16 N w x) dy17 ∧ mnv2Stride1LossTiedB xN cotN vN epsStr w.b17 bf16 (mnv2PreB16 N w x)
(fun (p : IVW 160 960 320) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := p,
hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ, hβ := w.hβ,
fcW := w.fcW, fcb := w.fcb }
cd x))
dy17) ∧ mnv2HeadTiedB N 7 7 xN cotN vN epsStr w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb bf16 cd
(mnv2PreB17 N w x) g ∧ mnv2HeadLossTiedB xN cotN vN epsStr w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb bf16 cd
(mnv2PreB17 N w x)
(fun (W : Kernel4 1280 320 1 1) (b γ β : Vec 1280) (Wd : Mat 1280 nCls)
(bd : Vec nCls) =>
L
(mobilenetv2ForwardBFullDoOpt 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, b17 := w.b17,
hW := W, hb := b, hε := w.hε, hγ := γ, hβ := β, fcW := Wd, fcb := bd }
cd x))
g
The emitted MobileNetV2 step's gradient nodes ARE the loss's gradient, at one chain. For
each of the 210 parameter slots, at ONE cotangent chain (the tie's own, from g): the node
denotes its layer's Jacobian against the chain cotangent (mnv2_net_tiedB), and any loss L of
the logits with gradient g at the network's output of mobilenetv2ForwardBFull with that one
slot varied is differentiable there with the node as its gradient (mnv2_net_lossGrad). The two
theorems each state the chain; this one states it once, so an edit to either chain breaks its
proof.