Documentation

LeanMlir.Proofs.Architectures.ConvIndex

Conv and max-pool index facts — the flat ↔ tensor index vocabulary #

The flat-index plumbing every conv-net proof reads tensors through (t3Idx, the window-tiling sums, sum_s2), and the 2×2 max-pool's window facts: the window max is Lipschitz in its cells, the pool is 1-Lipschitz per entry and ℓ1-contractive, and a selection margin beyond 2δ freezes the argmax (MaxPool2MarginQ). The ℝ conv as a dense layer with weight sharing and its float forward are in ConvFloat.

source
theorem Proofs.max4_sub_abs_le {a b c d a' b' c' d' δ : ℝ} (h1 : |a - a'| ≤ δ) (h2 : |b - b'| ≤ δ) (h3 : |c - c'| ≤ δ) (h4 : |d - d'| ≤ δ) :
|max (max a b) (max c d) - max (max a' b') (max c' d')| ≤ δ

A four-way max moves by at most the largest cell movement (ℓ∞).

source
theorem Proofs.max4_sub_abs_le_sum {a b c d a' b' c' d' : ℝ} :
|max (max a b) (max c d) - max (max a' b') (max c' d')| ≤ |a - a'| + |b - b'| + |c - c'| + |d - d'|

A four-way max moves by at most the sum of the cell movements (ℓ1) — the per-window step of the pool's ℓ1 contraction.

source
@[reducible]
def Proofs.t3Idx {c h w : ℕ} (ci : Fin c) (hi : Fin h) (wi : Fin w) :
Fin (c * h * w)

Flat index of a Tensor3 coordinate (the suite's row-major layout).

⚠ @[reducible] is load-bearing on Lean ≥ 4.33 (see planning/archive/lean_434_and_cleanup.md): t3Idx_def folds the raw encoding into the ite CONDITION below, but simp does not rewrite inside the Decidable INSTANCE argument, so the goal carries a folded condition over an unfolded instance and every ite_eq_left/ite_eq_right here fails to match. basisVec, which produces that ite, is @[reducible] for the same reason.

Equations
Instances For
    source
    theorem Proofs.unflatten_t3Idx {c h w : ℕ} (v : Vec (c * h * w)) (ci : Fin c) (hi : Fin h) (wi : Fin w) :
    Tensor3.unflatten v ci hi wi = v (t3Idx ci hi wi)

    t3Idx reads back through Tensor3.unflatten.

    source
    theorem Proofs.flatten_t3Idx {c h w : ℕ} (T : Tensor3 c h w) (ci : Fin c) (hi : Fin h) (wi : Fin w) :
    T.flatten (t3Idx ci hi wi) = T ci hi wi

    Tensor3.flatten reads off at a t3Idx.

    source
    theorem Proofs.sum_t3 {c h w : ℕ} (f : Fin (c * h * w) → ℝ) :
    ∑ k : Fin (c * h * w), f k = ∑ ci : Fin c, ∑ hi : Fin h, ∑ wi : Fin w, f (t3Idx ci hi wi)

    A flat sum is the triple tensor sum.

    source
    theorem Proofs.t3Idx_surj {c h w : ℕ} (k : Fin (c * h * w)) :
    ∃ (ci : Fin c) (hi : Fin h) (wi : Fin w), k = t3Idx ci hi wi

    Every flat spatial index is a t3Idx — lets a per-cell bound be lifted to the whole flattened conv-output vector (∀ k), the form relu_close / maxPoolFlat_close / dense_close consume.

    source
    def Proofs.winRowEquiv (h : ℕ) :
    Fin h × Fin 2 ≃ Fin (2 * h)

    The window-cell parameterization (out-row, sub-row) ↦ in-row is a bijection — pooled windows tile the rows.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Proofs.winColEquiv (w : ℕ) :
      Fin w × Fin 2 ≃ Fin (2 * w)

      Column version of winRowEquiv.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Proofs.sum_window_cells {h w : ℕ} (g : Fin (2 * h) → Fin (2 * w) → ℝ) :
        ∑ ho : Fin h, ∑ wo : Fin w, ∑ ab : Fin 2 × Fin 2, g (winRowInv ho ab.1) (winColInv wo ab.2) = ∑ hi : Fin (2 * h), ∑ wi : Fin (2 * w), g hi wi

        Summing a function over all window cells of all windows is summing it over the whole spatial grid — the 2×2 stride-2 windows partition the input.

        source
        theorem Proofs.maxPoolFlat_apply {c h w : ℕ} (u : Vec (c * (2 * h) * (2 * w))) (ci : Fin c) (ho : Fin h) (wo : Fin w) :
        maxPoolFlat c h w u (t3Idx ci ho wo) = max (max (u (t3Idx ci (winRowInv ho 0) (winColInv wo 0))) (u (t3Idx ci (winRowInv ho 1) (winColInv wo 0)))) (max (u (t3Idx ci (winRowInv ho 0) (winColInv wo 1))) (u (t3Idx ci (winRowInv ho 1) (winColInv wo 1))))

        The pooled entry at (ci, ho, wo) is the four-way max of its window cells, in flat coordinates.

        source
        theorem Proofs.maxPoolFlat_l1_contract {c h w : ℕ} (u v : Vec (c * (2 * h) * (2 * w))) :
        ∑ q : Fin (c * h * w), |maxPoolFlat c h w u q - maxPoolFlat c h w v q| ≤ ∑ k : Fin (c * (2 * h) * (2 * w)), |u k - v k|

        ℓ1 contraction: the pooled drift, summed over all pooled entries, is at most the input drift summed over all input entries (windows are disjoint, max is 1-Lipschitz). The pool passes ℓ1 budgets through unamplified.

        source
        theorem Proofs.ne_of_gap_of_close {xa xb ya yb δ : ℝ} (hgap : 2 * δ < |xa - xb|) (ha : |ya - xa| ≤ δ) (hb : |yb - xb| ≤ δ) :
        ya ≠ yb

        Two values farther apart than 2δ cannot be equalized by δ-perturbations.

        source
        theorem Proofs.lt_of_lt_gap_of_close {xa xb ya yb δ : ℝ} (hlt : 2 * δ < xb - xa) (ha : |ya - xa| ≤ δ) (hb : |yb - xb| ≤ δ) :
        ya < yb

        Strict order survives δ-perturbations across a 2δ gap.

        source
        def Proofs.MaxPool2MarginQ {c h w : ℕ} (δ : ℝ) (x : Tensor3 c (2 * h) (2 * w)) :
        Prop

        Quantitative pool-selection margin: every two cells of every 2×2 window differ by more than 2δ. The quantitative form of MaxPool2Smooth — a perturbation of at most δ per entry can neither create a tie nor reorder a window, so the pool's argmax routing freezes. The pool peer of the ReLU margin a·D < |zⱼ|.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Proofs.MaxPool2MarginQ.smooth_of_close {c h w : ℕ} {δ : ℝ} {x y : Tensor3 c (2 * h) (2 * w)} (hm : MaxPool2MarginQ δ x) (hclose : ∀ (ci : Fin c) (hi : Fin (2 * h)) (wi : Fin (2 * w)), |y ci hi wi - x ci hi wi| ≤ δ) :
          MaxPool2Smooth y

          Every point within δ of a margined point is smooth (no window ties).

          source
          theorem Proofs.MaxPool2MarginQ.smooth {c h w : ℕ} {δ : ℝ} (hδ0 : 0 ≤ δ) {x : Tensor3 c (2 * h) (2 * w)} (hm : MaxPool2MarginQ δ x) :
          MaxPool2Smooth x

          A margined point is itself smooth.

          source
          theorem Proofs.MaxPool2MarginQ.isArgmax_iff {c h w : ℕ} {δ : ℝ} {x y : Tensor3 c (2 * h) (2 * w)} (hm : MaxPool2MarginQ δ x) (hclose : ∀ (ci : Fin c) (hi : Fin (2 * h)) (wi : Fin (2 * w)), |y ci hi wi - x ci hi wi| ≤ δ) (ci : Fin c) (hi : Fin (2 * h)) (wi : Fin (2 * w)) :
          MaxPool2IsArgmax y ci hi wi ↔ MaxPool2IsArgmax x ci hi wi

          The argmax freezes: within δ of a margined point, every window's argmax cell is the same as at the margined point.

          source
          theorem Proofs.sum_s2 {h w : ℕ} (g : Fin (h * w) → ℝ) :
          ∑ s : Fin (h * w), g s = ∑ hi : Fin h, ∑ wi : Fin w, g (finProdFinEquiv (hi, wi))

          The spatial (hi, wi) sum collapses to one flat sum over Fin (h·w).

          source
          noncomputable def Proofs.convPad {ic h w : ℕ} (kH kW : ℕ) (x : Tensor3 ic h w) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hi : Fin h) (wi : Fin w) :
          ℝ

          The padded input read that multiplies kernel entry (·, c, kh, kw) at output position (hi, wi) — names the dite inside conv2d so the affine-in-the-kernel structure can be stated. Depends on the input only, never the kernel.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For