TorchLean API

Docs HomeGuideExamplesGraphs

NN.Proofs.RuntimeApprox.NF.ConvBackward.Input

NeuralFloat Conv2D Input-Gradient Bounds #

This file completes the pointwise approximation argument for Conv2D backward by handling the input gradient. Each input coordinate collects exactly the output/kernel positions that contribute to it under the stride and padding relation, then bounds the resulting NeuralFloat accumulation.

source
noncomputable def Proofs.RuntimeApprox.NFBackend.conv2dInputPointBound {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {inC outC kH kW stride padding inH inW : ℕ} (kernelR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))) (δR : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) (TorchLean.Floats.NF β fexp rnd)) (epsK epsδ : ℝ) (in_ch : Fin inC) (i : Fin inH) (j : Fin inW) :
ℝ

Pointwise error bound for the Conv2D input gradient (NF runtime vs spec).

The input-gradient entry accumulates contributions from all output channels and spatial positions that “hit” the given input coordinate under the stride/padding relation. The bound is a replay of that accumulation with per-term errors derived from epsK and epsδ.

Instances For
    source
    noncomputable def Proofs.RuntimeApprox.NFBackend.conv2dInputBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {inC outC kH kW stride padding inH inW : ℕ} (kernelR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))) (δR : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) (TorchLean.Floats.NF β fexp rnd)) (epsK epsδ : ℝ) :
    Spec.MultiChannelImage inC inH inW ℝ

    Tensor-shaped input-gradient bound.

    This packages conv2dInputPointBound into the full input image shape so later approxT lemmas can use a single global bound via linfNorm.

    Instances For
      source
      theorem Proofs.RuntimeApprox.NFBackend.approx_conv2d_input_point {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} {kernelS : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))} {kernelR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))} {biasS : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar)} {biasR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC Spec.Shape.scalar)} {inputS : Spec.MultiChannelImage inC inH inW ℝ} {inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)} {δS : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ} {δR : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) (TorchLean.Floats.NF β fexp rnd)} {epsK epsδ : ℝ} (hK : approxT toSpec kernelS kernelR epsK) (hδ : approxT toSpec δS δR epsδ) (in_ch : Fin inC) (i : Fin inH) (j : Fin inW) :
      have layerS := { kernel := kernelS, bias := biasS }; have layerR := { kernel := kernelR, bias := biasR }; |toSpec (Spec.getAtOrZero (Spec.conv2dInputDerivSpec layerR inputR δR) [↑in_ch, ↑i, ↑j]) - Spec.getAtOrZero (Spec.conv2dInputDerivSpec layerS inputS δS) [↑in_ch, ↑i, ↑j]| ≤ conv2dInputPointBound kernelR δR epsK epsδ in_ch i j

      Soundness of the Conv2D input-gradient pointwise bound.

      Given approxT hypotheses for the kernel and upstream gradient (grad_output), this shows the spec input-gradient entry is approximated by the NF runtime entry within conv2dInputPointBound.

      source
      theorem Proofs.RuntimeApprox.NFBackend.approxT_conv2d_input_deriv_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} {kernelS : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))} {kernelR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))} {biasS : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar)} {biasR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC Spec.Shape.scalar)} {inputS : Spec.MultiChannelImage inC inH inW ℝ} {inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)} {δS : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ} {δR : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) (TorchLean.Floats.NF β fexp rnd)} {epsK epsδ : ℝ} (hK : approxT toSpec kernelS kernelR epsK) (hδ : approxT toSpec δS δR epsδ) :
      have layerS := { kernel := kernelS, bias := biasS }; have layerR := { kernel := kernelR, bias := biasR }; have outS := Spec.conv2dInputDerivSpec layerS inputS δS; have outR := Spec.conv2dInputDerivSpec layerR inputR δR; have bT := conv2dInputBoundTensor kernelR δR epsK epsδ; approxT toSpec outS outR (linfNorm bT)

      Tensor-level approxT bound for the Conv2D input gradient.

      This lifts approx_conv2d_input_point entrywise and packages the error into linfNorm (conv2dInputBoundTensor ...).

      source
      theorem Proofs.RuntimeApprox.NFBackend.idx_i_ne_of_shape_ne {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} (a : Idx Γ s₁) (b : Idx Γ s₂) (hs : s₁ ≠ s₂) :
      a.i ≠ b.i