Documentation

LeanMlir.Proofs.Architectures.PerChannelBNGrad

Per-channel BN parameter-gradient bridges (dγ, dβ certified) #

The non-BN closes (cnn_render_conv{W,b}_certified + the dense bridges IR.weight_grad_bridge / IR.bias_grad_bridge) and the BN input-grad (bnPerChannelGradInput_correct, under 0<ε) already cover every parameter of a per-channel-BN train step except the BN scale/shift γ, β. This file supplies their bridges — the BN analogue of IR.bias_grad_bridge / conv_bias_grad_bridge.

γ and β enter BN affinely: per channel c, y_(c,s) = γ_c · x̂_(c,s) + β_c, and x̂ does not depend on γ or β. So as a function of γ (resp. β), per-channel BN is x̂ ⊙ gather_channel(γ) + const (resp. const + gather_channel(β)) — a constant scaled by a channel-gather, plus a constant. pdiv_of_affine therefore reads its Jacobian off the basis vector as the sparse indicator ∂y_j/∂γ_idx = x̂_j·[chan j = idx] (resp. [chan j = idx]), and contracting with the cotangent dy gives exactly the rendered per-channel reduces dγ_c = Σ_s dy·x̂, dβ_c = Σ_s dy (the bnGammaSgd / bnBetaSgd ops). Unlike the BN input grad these need no 0<ε (affine in the params; ε only enters the constant x̂).

source
theorem Proofs.bnPerChannelGradGamma_correct (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (idx : Fin oc) :
bnPerChannelGradGamma oc m ε v dy idx = ∑ j : Fin (oc * m), pdiv (fun (γ' : Vec oc) => bnPerChannelFlat oc m ε γ' β v) γ idx j * dy j

BN γ-gradient bridge. The rendered per-channel dγ_idx = Σ_s dy·x̂ equals the certified Jacobian of per-channel BN (as a function of γ) contracted with the cotangent dy. The BN analogue of the conv/dense weight bridges; affine in γ, so no 0<ε.

source
theorem Proofs.bnPerChannelGradBeta_correct (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (idx : Fin oc) :
bnPerChannelGradBeta oc m dy idx = ∑ j : Fin (oc * m), pdiv (fun (β' : Vec oc) => bnPerChannelFlat oc m ε γ β' v) β idx j * dy j

BN β-gradient bridge. The rendered per-channel dβ_idx = Σ_s dy equals the certified Jacobian of per-channel BN (as a function of β) contracted with dy. The BN analogue of bias_grad_bridge; affine in β, so no 0<ε.

source
theorem Proofs.bnPerChannel_gamma_sgd_certified (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (lr : ℝ) (idx : Fin oc) :
γ idx - lr * bnPerChannelGradGamma oc m ε v dy idx = γ idx - lr * ∑ j : Fin (oc * m), pdiv (fun (γ' : Vec oc) => bnPerChannelFlat oc m ε γ' β v) γ idx j * dy j

BN γ output certified. γ_c − lr·(rendered dγ_c) denotes γ_c − lr·(certified ∂(per-channel BN)/∂γ_c · cotangent). The γ peer of conv_bias_sgd_certified.

source
theorem Proofs.bnPerChannel_beta_sgd_certified (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (lr : ℝ) (idx : Fin oc) :
β idx - lr * bnPerChannelGradBeta oc m dy idx = β idx - lr * ∑ j : Fin (oc * m), pdiv (fun (β' : Vec oc) => bnPerChannelFlat oc m ε γ β' v) β idx j * dy j

BN β output certified. β_c − lr·(rendered dβ_c) denotes the certified BN ∂/∂β contraction. The β peer.