Documentation

LeanMlir.Proofs.Certificates.DenseEuclid

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, and certified_at_eps_close widens that check by a per-logit evaluation budget (the float tier's composition step). The trained instances are in LipschitzCert.Instance. The namespace Proofs.Robustness holds these engines, the IBP / CROWN / pair-SDP ones beside them, and every scorecard that instantiates them.

noncomputable def Proofs.Robustness.denseE {n k : ℕ} (W : Fin k → Fin n → ℝ) :

EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)

A bias-free dense (linear) layer on Euclidean space: (denseE W x)ᵢ = Σⱼ Wᵢⱼ xⱼ.

Equations

Proofs.Robustness.denseE W x = WithLp.toLp 2 fun (i : Fin k) => ∑ j : Fin n, W i j * x.ofLp j

Instances For

@[simp]

theorem Proofs.Robustness.denseE_apply {n k : ℕ} (W : Fin k → Fin n → ℝ) (x : EuclideanSpace ℝ (Fin n)) (i : Fin k) :

(denseE W x).ofLp i = ∑ j : Fin n, W i j * x.ofLp j

theorem Proofs.Robustness.sum_sq_matvec_le {k n : ℕ} (M : Fin k → Fin n → ℝ) (y : Fin n → ℝ) :

∑ a : Fin k, (∑ b : Fin n, M a b * y b) ^ 2 ≤ (∑ a : Fin k, ∑ b : Fin n, M a b ^ 2) * ∑ b : Fin n, y b ^ 2

Row-wise Cauchy–Schwarz summed: ‖Mv‖² ≤ ‖M‖_F²·‖v‖² at the raw-sum level.

theorem Proofs.Robustness.denseE_lipschitzL2 {n k : ℕ} (W : Fin k → Fin n → ℝ) {C : ℝ} (hC : 0 ≤ C) (hW : ∑ i : Fin k, ∑ j : Fin n, W i j ^ 2 ≤ C ^ 2) :

LipschitzL2 C (denseE W)

Frobenius bound, proved. If the entrywise square sum of W is at most C², the dense layer is C-Lipschitz in L2. Power iteration only estimates ‖W‖₂ from below; ‖W‖₂ ≤ ‖W‖_F makes any rational C ≥ ‖W‖_F a sound Lipschitz constant.

noncomputable def Proofs.Robustness.reluE {n : ℕ} :

EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)

Coordinatewise ReLU on Euclidean space.

Equations

Proofs.Robustness.reluE x = WithLp.toLp 2 fun (i : Fin n) => max (x.ofLp i) 0

Instances For

@[simp]

theorem Proofs.Robustness.reluE_apply {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) :

(reluE x).ofLp i = max (x.ofLp i) 0

theorem Proofs.Robustness.mlp_out_eq {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) {x : EuclideanSpace ℝ (Fin n)} {pre : Fin h → ℝ} (hpre : ∀ (t : Fin h), (denseE W1 x).ofLp t = pre t) (j : Fin k) :

((denseE W2 ∘ reluE ∘ denseE W1) x).ofLp j = ∑ t : Fin h, W2 j t * max (pre t) 0

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.

theorem Proofs.Robustness.sqrt_two_le_rat :

√2 ≤ 14143 / 10000

√2 ≤ 14143/10000 — the rational majorant the per-image radius checks use.

theorem Proofs.Robustness.certified_at_eps {n k : ℕ} {L m ε : ℝ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} (hf : LipschitzL2 L f) (hL : 0 < L) {x : EuclideanSpace ℝ (Fin n)} {i : Fin k} (hmargin : ∀ (j : Fin k), j ≠ i → m ≤ (f x).ofLp i - (f x).ofLp j) (hε : 14143 / 10000 * L * ε ≤ m) (hε0 : 0 ≤ ε) (δ : EuclideanSpace ℝ (Fin n)) (hδ : ‖δ‖ < ε) (j : Fin k) :

j ≠ i → (f (x + δ)).ofLp j < (f (x + δ)).ofLp i

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.

theorem Proofs.Robustness.certified_at_eps_close {n k : ℕ} {L m ε B : ℝ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} (hf : LipschitzL2 L f) (hL : 0 < L) {x : EuclideanSpace ℝ (Fin n)} {i : Fin k} (hmargin : ∀ (j : Fin k), j ≠ i → m ≤ (f x).ofLp i - (f x).ofLp j) (hclear : 14143 / 10000 * L * ε + 2 * B < m) (hε0 : 0 ≤ ε) (_hB0 : 0 ≤ B) (δ : EuclideanSpace ℝ (Fin n)) (hδ : ‖δ‖ < ε) (z' : Fin k → ℝ) (hz' : ∀ (j : Fin k), |z' j - (f (x + δ)).ofLp j| ≤ B) (j : Fin k) :

j ≠ i → z' j < z' i

The certificate composed with a per-logit evaluation budget. If the ℝ logit map is L-Lipschitz with margin m at x, and the margin clears the float-widened threshold (14143/10000)·L·ε + 2·B, then ANY evaluation z' within B of the ℝ logits at x + δ keeps class i the strict argmax — for every ‖δ‖ < ε. Pure margin arithmetic; z' is the deployed (rounded) forward.

theorem Proofs.Robustness.reluE_lipschitzL2 {n : ℕ} :

LipschitzL2 1 reluE

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.

theorem Proofs.Robustness.sum_sq_matTvec_eq {p q : ℕ} (A : Fin p → Fin q → ℝ) (y : Fin p → ℝ) (K : Fin p → Fin p → ℝ) (hK : ∀ (a b : Fin p), K a b = ∑ j : Fin q, A a j * A b j) :

∑ j : Fin q, (∑ i : Fin p, A i j * y i) ^ 2 = ∑ a : Fin p, y a * ∑ b : Fin p, K a b * y b

Sum-shuffle: ‖Aᵀy‖² = ⟨y, K y⟩ for K = A·Aᵀ supplied as data. The rearrangement engine both Gram bounds share.

theorem Proofs.Robustness.denseE_lipschitzL2_gram {n k : ℕ} (W : Fin k → Fin n → ℝ) (G : Fin k → Fin k → ℝ) {B : ℝ} (hB : 0 ≤ B) (hG : ∀ (a b : Fin k), G a b = ∑ j : Fin n, W a j * W b j) (hGF : ∑ a : Fin k, ∑ b : Fin k, G a b ^ 2 ≤ B ^ 4) :

LipschitzL2 B (denseE W)

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 W has rank ≥ 2. The Gram matrix is only k×k (output-side), so the kernel arithmetic stays small even for wide layers.

theorem Proofs.Robustness.denseE_lipschitzL2_gram2 {n k : ℕ} (W : Fin k → Fin n → ℝ) (G H : Fin k → Fin k → ℝ) {B : ℝ} (hB : 0 ≤ B) (hG : ∀ (a b : Fin k), G a b = ∑ j : Fin n, W a j * W b j) (hH : ∀ (a b : Fin k), H a b = ∑ c : Fin k, G c a * G c b) (hHF : ∑ a : Fin k, ∑ b : Fin k, H a b ^ 2 ≤ B ^ 8) :

LipschitzL2 B (denseE W)

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.

theorem Proofs.Robustness.lipschitzL2_lower_euclid {n k : ℕ} {L ℓ : ℝ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} (hf : LipschitzL2 L f) (hℓ : 0 ≤ ℓ) (u w : EuclideanSpace ℝ (Fin n)) (hpos : 0 < ∑ j : Fin n, (u - w).ofLp j ^ 2) (hray : ℓ ^ 2 * ∑ j : Fin n, (u - w).ofLp j ^ 2 ≤ ∑ i : Fin k, (f u - f w).ofLp i ^ 2) :

ℓ ≤ L

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‖₂.

def Proofs.Robustness.CertifiedAt {n k : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)) (ε : ℝ) (x : EuclideanSpace ℝ (Fin n)) (i : Fin k) :

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.

Equations

Proofs.Robustness.CertifiedAt f ε x i = ∀ (δ : EuclideanSpace ℝ (Fin n)), ‖δ‖ < ε → ∀ (j : Fin k), j ≠ i → (f (x + δ)).ofLp j < (f (x + δ)).ofLp i

Instances For

theorem Proofs.Robustness.CertifiedAt.mono {n k : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} {ε ε' : ℝ} {x : EuclideanSpace ℝ (Fin n)} {i : Fin k} (hc : CertifiedAt f ε x i) (hle : ε' ≤ ε) :

CertifiedAt f ε' x i

Certification is monotone in the radius — CertifiedAtLinf.mono's L2 peer.

theorem Proofs.Robustness.CertifiedAt.of_margin {n k : ℕ} {L m ε : ℝ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} (hf : LipschitzL2 L f) (hL : 0 < L) {x : EuclideanSpace ℝ (Fin n)} {i : Fin k} (hmargin : ∀ (j : Fin k), j ≠ i → m ≤ (f x).ofLp i - (f x).ofLp j) (hε : 14143 / 10000 * L * ε ≤ m) (hε0 : 0 ≤ ε) :

CertifiedAt f ε x i

certified_at_eps, concluding the certificate itself: an L-Lipschitz map whose margin at x clears (14143/10000)·L·ε is CertifiedAt radius ε.