The dense Euclidean engine — dense and ReLU layers on EuclideanSpace, and their L2 bounds #
The layers every Lipschitz / interval certificate in Certificates/ is stated about: denseE W
(bias-free dense, (Wx)ᵢ) and reluE, with the L2 Lipschitz bounds the product certificate
multiplies — Frobenius (denseE_lipschitzL2), the Gram / Schatten-4 bound
(denseE_lipschitzL2_gram), Schatten-8 (denseE_lipschitzL2_gram2), and the lower bound a
witness vector gives (lipschitzL2_lower_euclid). The upper bounds share one tail
(denseE_lipschitzL2_of_sq) and the Gram ones one Cauchy–Schwarz step (sq_le_of_gram_quad,
quad_le_of_frob). certified_at_eps specialises the
Tsuzuku certificate to a rational radius check. The trained instances are in
LipschitzCertInstance; the namespace is theirs, kept so every citation keeps its name.
A bias-free dense (linear) layer on Euclidean space:
(denseE W x)ᵢ = Σⱼ Wᵢⱼ xⱼ.
Equations
- Proofs.LipschitzCertDemo.denseE W x = WithLp.toLp 2 fun (i : Fin k) => ∑ j : Fin n, W i j * x.ofLp j
Instances For
The common tail of every dense bound: a raw-sum bound ‖Wd‖² ≤ B²·‖d‖² for every d
makes the dense layer B-Lipschitz in L2. The Frobenius and Gram bounds below differ only in
how they prove hW.
Frobenius bound, proved. If the entrywise square sum of W is at
most C², the dense layer is C-Lipschitz in L2. This is the certified
replacement for the power-iteration estimate specNormW: ‖W‖₂ ≤ ‖W‖_F,
so any rational C ≥ ‖W‖_F is a sound Lipschitz constant.
Coordinatewise ReLU on Euclidean space.
Equations
- Proofs.LipschitzCertDemo.reluE x = WithLp.toLp 2 fun (i : Fin n) => max (x.ofLp i) 0
Instances For
A one-hidden-layer net's logits from its hidden pre-activations. Given the exact
pre-activations pre of x, each logit of denseE W2 ∘ reluE ∘ denseE W1 is the finite sum
the per-image margin and argmax proofs expand; every generated scorecard reads its logits
through this.
√2 ≤ 14143/10000 — the rational majorant the per-image radius checks use.
Specialize the Tsuzuku certificate to a FIXED radius ε: if the margin
clears the rational check (14143/10000)·L·ε ≤ m (kernel-checkable —
no √2), every ‖δ‖ < ε leaves class i the strict argmax.
ReLU is 1-Lipschitz in L2 — coordinatewise |max(a,0) − max(b,0)| ≤ |a − b|
summed. The activation contributes factor 1 to the product certificate.
The Gram step: with G = W·Wᵀ and y = Wd, a bound ⟨y, Gy⟩ ≤ c·‖y‖² gives
‖y‖² ≤ c·‖d‖² — because ‖y‖² = ⟨d, Wᵀy⟩ ≤ ‖d‖·‖Wᵀy‖ and ‖Wᵀy‖² = ⟨y, Gy⟩.
Gram (Schatten-4) bound, proved. If G = W·Wᵀ (supplied as data, verified
entrywise) and ‖G‖_F² ≤ B⁴, then the dense layer is B-Lipschitz in L2.
Since ‖G‖_F = (Σᵢσᵢ⁴)^½, this is ‖W‖₂ ≤ (Σσᵢ⁴)^¼ — strictly tighter than
Frobenius (Σσᵢ²)^½ whenever the spectrum has any spread. The Gram matrix is
only k×k (output-side), so the kernel arithmetic stays small even for wide
layers.
Iterated Gram (Schatten-8) bound, proved. One more squaring:
with G = W·Wᵀ and H = Gᵀ·G (= G² for the symmetric G) supplied as
data, ‖H‖_F² ≤ B⁸ gives LipschitzL2 B (denseE W) — i.e.
‖W‖₂ ≤ ‖G²‖_F^(1/4) = (Σσᵢ⁸)^(1/8), one Cauchy–Schwarz level tighter
than the Schatten-4 bound.
Certified lower bound on any L2 Lipschitz constant (the power-iteration
direction): if ‖f u − f w‖ ≥ ℓ·‖u − w‖ at one concrete pair (verified as a
squared-sum inequality in-kernel), then every valid L satisfies ℓ ≤ L.
With u the (rationalized) power-iteration singular vector and w = 0,
this certifies how close a proven upper bound sits to the true ‖W‖₂.
f is certified at radius ε on input x with class i: every perturbation of L2 norm
< ε leaves i the strict argmax. The (undecidable — it quantifies over real δ)
per-image certificate every scorecard's certifiedC<i> / certifiedU<i> theorems prove.