The per-channel-BN MobileNetV2 stage vocabulary #

Per-channel-BN mirrors (bnPerChannelTensor3: reduce over spatial [2,3], γ/β : Vec c) of the global-BN stage abbreviations ivExpand / … / ivProject: ivExpandPC / ivDepthwisePC / ivDepthwiseStridedPC / ivProjectPC, and the two inverted-residual bodies composed from them (invresBodyPC, invresBodyStridedPC). MobileNetV2StagesPCEval gives their frozen-statistics twins.

source

@[reducible]

noncomputable def Proofs.ivExpandPC {ic mid h w kHe kWe : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) :

Vec (ic * h * w) → Vec (mid * h * w)

Expand stage, per-channel BN: relu6 ∘ bnPC ∘ conv(1×1).

Equations

Proofs.ivExpandPC We be εe γe βe = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelTensor3 mid h w εe γe βe ∘ Proofs.flatConv We be

Instances For

source

@[reducible]

noncomputable def Proofs.ivDepthwisePC {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) :

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

Depthwise stage (stride-1), per-channel BN: relu6 ∘ bnPC ∘ depthwise.

Equations

Proofs.ivDepthwisePC Wd bd εd γd βd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelTensor3 mid h w εd γd βd ∘ Proofs.depthwiseFlat Wd bd

Instances For

source

@[reducible]

noncomputable def Proofs.ivDepthwiseStridedPC {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) :

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

Depthwise stage (stride-2 downsample), per-channel BN: relu6 ∘ bnPC ∘ depthwiseStrided.

Equations

Proofs.ivDepthwiseStridedPC Wd bd εd γd βd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelTensor3 mid h w εd γd βd ∘ Proofs.depthwiseStride2FlatXla Wd bd

Instances For

source

@[reducible]

noncomputable def Proofs.ivProjectPC {mid oc h w kHp kWp : ℕ} (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) :

Vec (mid * h * w) → Vec (oc * h * w)

Project (linear bottleneck) stage, per-channel BN: bnPC ∘ conv(1×1) (no relu6).

Equations

Proofs.ivProjectPC Wp bp εp γp βp = Proofs.bnPerChannelTensor3 oc h w εp γp βp ∘ Proofs.flatConv Wp bp

Instances For

source

@[reducible]

noncomputable def Proofs.invresBodyPC {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) :

Vec (ic * h * w) → Vec (oc * h * w)

Inverted-residual body (stride-1), per-channel BN: project ∘ depthwise ∘ expand.

Equations

Proofs.invresBodyPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp = Proofs.ivProjectPC Wp bp εp γp βp ∘ Proofs.ivDepthwisePC Wd bd εd γd βd ∘ Proofs.ivExpandPC We be εe γe βe

Instances For

source

@[reducible]

noncomputable def Proofs.invresBodyStridedPC {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) :

Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Inverted-residual body (stride-2 downsample), per-channel BN: expand SAME (at 2h×2w) → depthwise-strided → project.

Equations

Proofs.invresBodyStridedPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp = Proofs.ivProjectPC Wp bp εp γp βp ∘ Proofs.ivDepthwiseStridedPC Wd bd εd γd βd ∘ Proofs.ivExpandPC We be εe γe βe

Instances For

Documentation

LeanMlir.Proofs.Nets.MobileNet.MobileNetV2StagesPC

The per-channel-BN MobileNetV2 stage vocabulary #