Documentation

LeanMlir.Proofs.Float.ResNet34FloatBridge

ℝ→Float32 bridge: global average pooling #

The float global-average-pool gapFlatF and its budget gapFlat_close: GAP is a per-channel mean (globalAvgPoolFlat_eq_bnMean), so gapFlat_close reduces to bnMean_close on the channel slice (sum_finProdFinEquiv flattens the spatial double sum). The other ResNet-34 ops' float lemmas are elsewhere: the residual add is add_close (FloatBridge), the conv is flatConvF_close (ConvFloat), per-channel BN is bnForward_close_of (BnFloatBridge), and the FloatClose instances are in FloatComposeBridge.

source
noncomputable def Proofs.FloatModel.gapFlatF {c h w : ℕ} (M : FloatModel) (v : Vec (c * h * w)) :
Vec c

The float global-average-pool: per channel, the float mean of the channel's h·w spatial slice (rounded sum, rounded /(h·w)). The float peer of globalAvgPoolFlat.

Equations
Instances For
    source
    theorem Proofs.FloatModel.gapFlat_close {c h w : ℕ} (M : FloatModel) (v : Vec (c * h * w)) {A : ℝ} (hhw : 0 < h * w) (hA : ∀ (ci : Fin c) (hi : Fin h) (wi : Fin w), |Tensor3.unflatten v ci hi wi| ≤ A) (ci : Fin c) :
    |M.gapFlatF v ci - globalAvgPoolFlat c h w v ci| ≤ M.u * ((1 + M.u) ^ (h * w + 1) * A) + ((1 + M.u) ^ (h * w + 1) - 1) * A

    Global-average-pool closeness. GAP is the per-channel spatial mean, so the float GAP is within the bnMean_close budget of globalAvgPoolFlat per channel (sum_finProdFinEquiv flattens the spatial double sum to the Fin (h·w) slice the mean rounds).

    source
    theorem Proofs.globalAvgPoolFlat_eq_bnMean {c h w : ℕ} (v : Vec (c * h * w)) (ci : Fin c) :
    globalAvgPoolFlat c h w v ci = bnMean (h * w) fun (s : Fin (h * w)) => Tensor3.unflatten v ci (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2

    GAP as a per-channel bnMean. globalAvgPoolFlat c h w v ci is the mean of channel ci's spatial slice — bnMean (h·w) of the Fin (h·w)-indexed gather. The reduction gapFlat_close performs inline, exposed so the float-bridge magnitude/input-shift bounds (bnMean_abs_le / bnMean_input_close) apply.